A Tableau System for Quasi-Hybrid Logic

Abstract

Hybrid logic is a valuable tool for specifying relational structures, at the same time that allows defining accessibility relations between states, it provides a way to nominate and make mention to what happens at each specific state. However, due to the many sources nowadays available, we may need to deal with contradictory information. This is the reason why we came with the idea of Quasi-hybrid logic, which is a paraconsistent version of hybrid logic capable of dealing with inconsistencies in the information, written as hybrid formulas.

In [5] we have already developed a semantics for this paraconsistent logic. In this paper we go a step forward, namely we study its proof-theoretical aspects. We present a complete tableau system for Quasi-hybrid logic, by combining both tableaux for Quasi-classical and Hybrid logics.

1 Introduction

Hybrid logic [1] is the simplest tool for the description of relational structures: it allows establishing accessibility relations between states and furthermore, nominating and making mention to what happens at specific states.

Unfortunately, we may collect contradictory information due to the many sources nowadays available. This is the reason why we came with the idea of Quasi-hybrid logic [5], which is a paraconsistent version of hybrid logic, thus capable of dealing with the inconsistencies in the information, written as formulas in hybrid logic. This kind of logic is useful for comparing the amount of inconsistency among databases, and has proved to be applicable in a wide range of real-life applications, namely we have studied how can inconsistencies relate to the health care flow of a patient [4], and we are currently working in robotics in order to create a robot which uses a paraconsistent reasoning to determine its movements and actions.

This work proposes to introduce proof-theoretical aspects of QH logic. We aimed to combine both tableaux for quasi-classical and hybrid logics, [3, 8] respectively, which resulted in a new tableau system as desired.

Classically, tableau systems rely on a backwards reasoning where we start with a formula whose validity we want to prove. A tableau, i.e., a tree, is created using some predefined rules, and whose starting point is the negation of the formula we are investigating. If we come to a point where each branch of the tree contains both a formula of the form $\varphi$ and a formula of the form $\lnot \varphi$, we say that the tableau is closed and verify that there are no counter-models for the original formula, thus it is proved that the formula is valid.

In our paraconsistent setting, we will consider a database $\varDelta$, and a query $\psi$ whose satisfiability will be verified in the bistructures (introduced in Sect. 3) that satisfy the formulas in the database. Analogously to the classical case, we start with $\varDelta$ and $\psi ^*$, where $\psi ^*$ will be defined later (in particular it will be a satisfaction statement). Our tableau is constructed using strong rules (which yield disjunctive syllogism) for formulas in $\varDelta$ and a weaker version (which rejects DS) for $\psi ^*$. If we end up with a tableau which is closed, i.e., in which every branch has a formula of the form $\varphi$ and $\varphi ^*$, we can conclude that $\varphi$ is true in every bistructure that satisfies $\varDelta$.

2 The Basic Hybrid Language

We start by presenting the simplest form of hybrid logic: the basic hybrid language, $\mathcal {H}(@)$. The basic hybrid language introduces nominals and the satisfaction operator into the propositional modal logic. Although being a simple extension, it carries great power in terms of expressivity.

Definition 1

Let $L=\langle \mathrm {Prop}, \mathrm {Nom}\rangle$ be a hybrid similarity type where $\mathrm {Prop}$ is a set of propositional symbols and $\mathrm {Nom}$ is a set disjoint from $\mathrm {Prop}$. We use p, q, r, etc. to refer to the elements in $\mathrm {Prop}$. The elements in $\mathrm {Nom}$ are called nominals and we typically write them as i, j, k, etc.. The set of well-formed formulas over L, $\mathrm {Form}_@(L)$, is defined by the following grammar:

$$WFF:= i\ |\ p\ |\ \lnot \varphi \ |\ \varphi \vee \psi \ | \varphi \wedge \psi \ |\ \Diamond \varphi \ |\ \Box \varphi \ |\ @_i\varphi $$

For any nominal i, $@_i$ is called a satisfaction operator, and for a formula $\varphi$, $@_i \varphi$ is called a satisfaction statement.

Given a hybrid similarity type $L=\langle \mathrm {Prop}, \mathrm {Nom}\rangle$, a hybrid structure $\mathcal {H}$ over L is a tuple (W, R, N, V) such that:

• W is a non-empty set called domain, whose elements are called states or worlds.

• R is a binary relation on W and is called the accessibility relation.

• $N:\mathrm {Nom}\rightarrow W$ is a function called hybrid nomination that assigns nominals to elements in W. For any nominal i, N(i) is the element of W named by i.

• V is a hybrid valuation, which means that V is a function with domain $\mathrm {Prop}$ and range Pow(W) such that V(p) tells us at which states (if any) each propositional symbol is true.

The pair (W, R) is called the frame underlying $\mathcal {H}$ and $\mathcal {H}$ is said to be a structure based on this frame.

The satisfaction relation, which is defined as follows, is a generalization of Kripke-style satisfaction.

Definition 2

(Satisfaction). The relation of local satisfaction $\models$ between a hybrid structure $\mathcal {H}=(W, R, N, V)$, a state $w\in W$ and a hybrid formula is recursively defined by:

• 1. $\mathcal {H}, w\models i$ iff $w=N(i)$;

• 2. $\mathcal {H}, w\models p$ iff $w\in V(p)$;

• 3. $\mathcal {H}, w\models \lnot \varphi$ iff it is false that $\mathcal {H}, w \models \varphi$;

• 4. $\mathcal {H}, w\models \varphi \wedge \psi$ iff $\mathcal {H}, w \models \varphi$ and $\mathcal {H}, w \models \psi$;

• 5. $\mathcal {H}, w\models \varphi \vee \psi$ iff $\mathcal {H}, w \models \varphi$ or $\mathcal {H}, w \models \psi$;

• 6. $\mathcal {H}, w\models \Diamond \varphi$ iff $\exists w'\in W(w R w'$ and $\mathcal {H}, w'\models \varphi )$;

• 7. $\mathcal {H}, w\models \Box \varphi$ iff $\forall w'\in W(w R w' \Rightarrow \mathcal {H}, w'\models \varphi )$;

• 8. $\mathcal {H}, w\models @_i \varphi$ iff $\mathcal {H}, w'\models \varphi$, where $w'=N(i)$;

If $\mathcal {H}, w\models \varphi$ we say that $\varphi$ is satisfied in $\mathcal {H}$ at w. If $\varphi$ is satisfied at all states in a structure $\mathcal {H}$, we write $\mathcal {H}\models \varphi$. If $\varphi$ is satisfied at all states in all structures based on a frame $\mathcal {F}$, then we say that $\varphi$ is valid on $\mathcal {F}$ and we write $\mathcal {F}\models \varphi$. If $\varphi$ is valid on all frames, then we simply say that $\varphi$ is valid and we write $\models \varphi$. For $\varDelta \subseteq \mathrm {Form}_@(L)$, we say that $\mathcal {H}$ is a model of $\varDelta$ iff for all $\theta \in \varDelta , \mathcal {H}\models \theta$.

Definition 3

A formula $\bar{\varphi }\in \mathrm {Form}_@(L)$ is said to be (logically) equivalent to $\varphi \in \mathrm {Form}_@(L)$ iff for every hybrid structure $\mathcal {H}=(W, R, N, V)$, for all $w\in W$,

$$\mathcal {H}, w\models \varphi \Leftrightarrow \mathcal {H}, w\models \bar{\varphi }.$$

It is easy to see that boolean connectives have the usual properties, and that $\Box \varphi$ is equivalent to $\lnot \Diamond \lnot \varphi$.

We define the notion of negation normal form of a formula (i.e., formulas in which the negation symbol occurs immediately before propositional symbols and/or nominals) for hybrid logic and we establish an analogous result to the one in [2] for classical propositional logic that states that any modal formula is logically equivalent to one in the negation normal form.

Definition 4

Let $L=\langle \mathrm {Prop},\mathrm {Nom}\rangle$ be a hybrid similarity type. A formula is said to be in negation normal form, for short $\mathrm {NNF}$, if negation only appears directly before propositional variables and/or nominals. The set of $\mathrm {NNF}$ formulas over L, $\mathrm {Form}_{\mathrm {NNF}(@)}(L)$, is recursively defined as follows:

For $p\in \mathrm {Prop},\ i\in \mathrm {Nom}$,

• 1. $p,\ i,\ \lnot p,\ \lnot i$ are in $\mathrm {NNF}$;

• 2. If $\varphi ,\ \psi$ are formulas in $\mathrm {NNF}$, then $\varphi \vee \psi ,\ \varphi \wedge \psi$ are in $\mathrm {NNF}$;

• 3. If $\varphi$ is in $\mathrm {NNF}$, then $\Box \varphi ,\ \Diamond \varphi$ are in $\mathrm {NNF}$;

• 4. If $\varphi$ is in $\mathrm {NNF}$, then $@_i\varphi$ is in $\mathrm {NNF}$.

The next proposition shows that we do not lose generality by considering just formulas in negation normal form.

Proposition 1

[5]. Every formula $\varphi \in \mathrm {Form}_@(L)$ is logically equivalent to a formula $\bar{\varphi }\in \mathrm {Form}_{\mathrm {NNF}(@)}(L)$.

The negation normal form of a formula is defined just as in classical propositional logic. A recursive procedure that puts formulas in negation normal form $nnf: \mathrm {Form}_@(L)\rightarrow \mathrm {Form}_{\mathrm {NNF}(@)}(L)$, is set as usual. For example:

$$\begin{aligned}&nnf(l)\mathop {=}\limits ^{def} l, \text {if } l\ \text {is a literal}, \\&nnf(\lnot (\psi _1\wedge \psi _2))\mathop {=}\limits ^{def} nnf(\lnot \psi _1)\vee nnf(\lnot \psi _2) \quad \text {and} \quad nnf(\lnot \Box \psi )\mathop {=}\limits ^{def}\Diamond nnf(\lnot \psi ) \end{aligned}$$

3 Paraconsistency in Hybrid Logic

In this section we study paraconsistency in Hybrid logic following an approach inspired by the work of Grant and Hunter ([6, 7]).

First of all, we define a Quasi-hybrid ( $\mathrm {QH}$ ) Basic Logic. The assumption in [6] is that all formulas are in Prenex Conjunctive Normal Form; in $\mathrm {QH}$ logic we will assume henceforth that all formulas are in Negation Normal Form. This assumption does not lead to loss of generality since any hybrid formula is equivalent to a formula in negation normal form (cf. Proposition 1).

Next, concepts of bistructure, decoupled and strong satisfaction and $\mathrm {QH}$ model will be presented. We define the paraconsistent diagram of a bistructure.

3.1 Quasi-Hybrid Basic Logic

As already mentioned, we will assume that all formulas are in negation normal form, i.e., given a hybrid similarity type $L=\langle \mathrm {Prop}, \mathrm {Nom}\rangle$, the set of formulas is $\mathrm {Form}_{\mathrm {NNF}(@)} (L)$.

Definition 5

Let $\theta$ be a formula in $\mathrm {NNF}$. We define the complementation operation $\sim$ from $\sim \theta :=nnf(\lnot \theta )$.

The $\sim$ operator is not part of the object hybrid similarity type but it makes some definitions clearer.

Recall that a hybrid structure for a hybrid similarity type L is a tuple (W, R, N, V). However, in order to accommodate contradictions in a model, we will use two valuations for propositions: $V^+$ and $V^-$.

Definition 6

A hybrid bistructure is a tuple $(W, R, N, V^+, V^-)$, where $(W, R, N, V^+)$ and $(W, R, N, V^-)$ are hybrid structures.

The map $V^+$ is interpreted as the acceptance of a propositional symbol, and $V^-$ as the rejection. This is formalized in the definition for decoupled satisfaction.

Definition 7

For a hybrid bistructure $E=(W, R, N, V^+, V^-)$ we define a satisfiability relation $\models _d$ called decoupled satisfaction at $w\in W$ for propositional symbols and nominals as follows:

• 1. $E,w\models _d p \text { iff } w \in V^+(p)$;

• 2. $E, w\models _d i\text { iff } w=N(i)$;

• 3. $E, w\models _d \lnot p \text { iff } w \in V^-(p)$;

• 4. $E, w\models _d \lnot i \text { iff } w \ne N(i)$;

Since we allow both a propositional symbol and its negation to be simultaneously satisfied and also allow both to be non-satisfied, we have decoupled, at the level of the structure, the link between a formula and its complement. In contrast, if a classical hybrid structure satisfies a propositional symbol at some world, it is forced to not satisfy its complement at that world.

This decoupling gives us the basis for a semantics for paraconsistent reasoning. Paraconsistency involves a tradeoff; in order to allow contradictions, one of the following three principles must be abandoned: disjunction introduction, disjunctive syllogism, and transitivity. In this approach, we chose to keep the disjunctive syllogism and transitivity and discard disjunction introduction.

In Quasi-hybrid logic, “or" statements involve an intensional disjunction. Such a disjunction is one whose satisfaction entails not merely that at least one of the disjuncts is the case, but also that if one of the disjuncts were not the case, then the other one would be the case.

Definition 8

A satisfiability relation $\models _s$ called strong satisfaction, is defined as follows:

• 1. $E, w \models _s p\text { iff } E, w \models _d p$;

• 2. $E, w \models _s \lnot p\text { iff } E, w \models _d \lnot p$;

• 3. $E, w \models _s i\text { iff } E, w \models _d i$;

• 4. $E, w \models _s \lnot i\text { iff } E, w \models _d \lnot i$;

• 5. $E, w \models _s \theta _1\vee \theta _2\text { iff } [E, w \models _s \theta _1\ or\ E, w \models _s \theta _2]\ and\ [E, w \models _s \sim \theta _1\Rightarrow$

  $E, w \models _s \theta _2]\ and\ [E, w \models _s \sim \theta _2\Rightarrow E, w \models _s \theta _1]$;

• 6. $E, w \models _s \theta _1\wedge \theta _2\text { iff } E, w \models _s \theta _1\ and\ E, w \models _s \theta _2$;

• 7. $E, w \models _s \Diamond \theta \text { iff } \exists w'(wRw'\ \& \ E, w'\models _s \theta )$;

• 8. $E, w \models _s \Box \theta \text { iff } \forall w'(wRw'\Rightarrow E, w' \models _s \theta )$;

• 9. $E, w \models _s @_i \theta \text { iff } E, w' \models _s \theta \ where\ w'=N(i)$;

We define strong validity as follows: $E\models _s\theta \text { iff for all } w\in W,\ E, w \models _s \theta .$

We say that E is a quasi-hybrid model of $\varDelta$ iff for all $\theta \in \varDelta , E\models _s\theta$ and we write $E\models _s \varDelta$.

4 A Tableau for Quasi-Hybrid Logic

In this section we discuss a decision procedure for Quasi-hybrid logic, based on a tableau system. This new tableau system is a fusion between the tableau system for Quasi-classical logic introduced in [8], and the tableau system for Hybrid logic proposed in [3].

We will consider a database $\varDelta$ of hybrid formulas that express real situations where inconsistencies may appear at some states, and we will check if a query $\varphi$ is a consequence of the database, i.e., we will want to check if every bistructure that strongly validates all formulas in $\varDelta$ also validates $\varphi$ weakly.

We will restrict our attention to formulas which are satisfaction statements.

4.1 Tableau Rules for $\mathrm {QH}$ Logic

We will start by introducing some definitions that will be useful later when we explain the construction of the tableau. We present the rules and a theorem for checking soundness.

Definition 9

We define weak satisfaction $\models _\mathrm{w}$ as strong satisfaction $(\models _s)$, except for the case of disjunction, which we will consider as a classical disjunction:

$$\begin{aligned} E, w \models _\mathrm{w} \theta _1\vee \theta _2\,\text {iff}\,E, w \models _\mathrm{w} \theta _1\ or\ E, w \models _\mathrm{w} \theta _2 \end{aligned}$$

The reader may observe that for any $\theta \in \mathrm {Form}_{\mathrm {NNF}(@)}(L)$, $E,w\models _s \theta$ implies $E,w\models _\mathrm{w} \theta$. And that, by contraposition, $\not \models _\mathrm{w}\ \subseteq \ \not \models _s$.

Similarly to the definition of strong validity, we define weak validity as follows: $E\models _\mathrm{w}\theta \text { iff for all } w\in W,\ E, w \models _\mathrm{w} \theta .$

From now on, we will restrict our attention to satisfaction statements.

Definition 10

(Quasi-Hybrid Consequence Relation). Let $\varDelta$ be a set of satisfaction statements called database, and $\varphi$ be a satisfaction statement, called query. We say that $\varphi$ is a consequence of $\varDelta$ in quasi-hybrid logic if and only if, for all bistructures E which are quasi-hybrid models of $\varDelta$, $\varphi$ is weakly valid.

Formally,

$$\varDelta \models _{\mathrm {QH}} \varphi \text { iff } \forall E \left( E \models _s \varDelta \Rightarrow E \models _\mathrm{w} \varphi \right) $$

Before introducing the tableau-based proof procedure, some definitions are required, namely:

Definition 11

Given a hybrid similarity type $L=\langle \mathrm {Prop}, \mathrm {Nom}\rangle$, we denote the set of satisfaction statements over L as $L_@$.

We duplicate the set of satisfaction statements by considering starred copies. The extended set is denoted by $L^*_@$ and is defined as: $L^*_@=L_@\cup \{\varphi ^*\ |\ \varphi \in L_@\}$.

The satisfaction of the new formulas $\varphi ^*$ is in some sense the complementary of the satisfaction of $\varphi$.

Definition 12

We extend both weak and strong satisfaction relations to starred formulas as follows:

$\begin{array}{rcl} E,w \models _s \varphi ^* &{} \text {iff} &{} E, w\not \models _s \varphi \\ E,w \models _\mathrm{w} \varphi ^* &{} \text {iff} &{} E, w\not \models _\mathrm{w} \varphi \end{array}$

Weak and strong validity of starred formulas are defined in the natural way.

We can now introduce two types of decomposition rules to be used in our $\mathrm {QH}$ semantic tableau: strong rules and weak rules, strong rules are applied to non-starred formulas, and weak rules are applied to starred formulas. The tableau system will be denoted $T_{\mathrm {QH}}$.

Tableau Rules:

Strong rules (S-rules)

$\bullet$ For connectives and operators:

$$\begin{aligned} \displaystyle \frac{@_i (\alpha \vee \beta )}{(@_i (\sim \alpha ))^*\ |\ @_i \beta }\;(\vee _1) \displaystyle \frac{@_i (\alpha \vee \beta )}{(@_i (\sim \beta ))^*\ |\ @_i\alpha }\;(\vee _2) \displaystyle \frac{@_i (\alpha \vee \beta )}{@_i \alpha \ |\ @_i \beta }\;(\vee _3) \end{aligned}$$

$$\begin{aligned} \displaystyle \frac{@_i (\alpha \wedge \beta )}{@_i \alpha , @_i \beta }\;(\wedge ) \displaystyle \frac{@_i @_j \alpha }{@_j \alpha }\;(@) \displaystyle \frac{@_i \Box \alpha , @_i \Diamond t}{@_t \alpha }\;(\Box ) \end{aligned}$$

$$\begin{aligned} \displaystyle \frac{@_i \Diamond \alpha }{@_i \Diamond t, @_t \alpha }\;(\Diamond )(\text {i}) \end{aligned}$$

$\bullet$ For nominals:

$$\begin{aligned} \displaystyle \frac{}{@_i i}\;(Ref)(\text {ii}) \displaystyle \frac{@_a c, @_a\varphi }{@_c \varphi }\;(Nom_1)(\text {iii}) \displaystyle \frac{@_a c, @_a \Diamond b}{@_c \Diamond b}\;(Nom_2) \end{aligned}$$

Weak rules (W-rules)

$\bullet$ For connectives and operators:

$$\begin{aligned} \displaystyle \frac{(@_i (\alpha \vee \beta ))^*}{(@_i \alpha )^*, (@_i \beta )^*}\;(\vee ^*) \displaystyle \frac{(@_i (\alpha \wedge \beta ))^*}{(@_i \alpha )^*| (@_i \beta )^*}\;(\wedge ^*) \end{aligned}$$

$$\begin{aligned} \displaystyle \frac{(@_i @_j \alpha )^*}{(@_j \alpha )^*}\;(@^*) \displaystyle \frac{(@_i \Box \alpha )^*}{@_i \Diamond t, (@_t \alpha )^*}\;(\Box ^*)(\text {iv}) \displaystyle \frac{(@_i \Diamond \alpha )^*, @_i \Diamond t}{(@_t \alpha )^*}\;(\Diamond ^*) \end{aligned}$$

$$\begin{aligned} \displaystyle \frac{(@_i \Box \lnot t)^*}{@_i \Diamond t}\;(\Box ^*_{\lnot i}) \end{aligned}$$

$\bullet$ For nominals:

$$\begin{aligned} \displaystyle \frac{@_a c, (@_a\varphi )^*}{(@_c \varphi )^*}\;(Nom_1^*)(\text {iii}) \displaystyle \frac{@_a c, (@_a \Box b)^*}{(@_c \Box b)^*}\;(Nom_2^*) \end{aligned}$$

• (i) t is a new nominal, $\alpha$ is not a nominal.

• (ii) for i in the branch.

• (iii) for $\varphi$ a propositional variable/nominal.

• (iv) t is a new nominal, $\alpha$ is not of the form $\lnot j$, for j a nominal.

The strong and weak rules for nominals, together with $(\vee _1), (\vee _2), (\Box )$ and $(\Diamond ^*)$ are called non-destructive rules. The remaining are called destructive.

The star in the formulas can be seen as a kind of meta-negation; the weak rules, which involve starred formulas, can thus be viewed as duals of the strong ones, except for the case where we obtain the classical disjunction.

Next theorem states that $T_{\mathrm {QH}}$ is sound:

Theorem 1

(Soundness). The tableau rules are sound in the following sense:

• for any r-rule $\displaystyle \frac{\varLambda }{\varSigma }$, any bistructure E and any state $w\in W$, $E, w\models _r\varLambda$ implies $E, w\models _r\varSigma$.

• for any r-rule $\displaystyle \frac{\varLambda }{\varSigma \ |\ \varGamma }$, any bistructure E and any state $w\in W$, $E, w\models _r\varLambda$ implies $E, w\models _r\varSigma$ or $E, w\models _r\varGamma$,

for $\varLambda$; $\varSigma$ and $\varGamma$ lists of formulas in $L_@^*$ and $r\in \{s, \mathrm {w}\}$.

Proof

The proof can be obtained by checking each rule.

4.2 Properties of the Tableau System and its Construction

The idea of a tableau is that we apply the rules previously introduced to root formulas and to formulas which occur in the tableau after the application of a rule. This indiscriminate way of applying rules leads to infinite tableaux, where there may be repeated formulas and loops, thus we must find a systematic construction that terminates a tableau and allows us to take some conclusions from it.

Definition 13

We say that a formula $\chi \in L_@^*$ is a strong occurrence/s-occurs if it is the result of applying a strong rule. Analogously we say that $\chi$ is a weak occurrence/w-occurs if it is the result of applying a weak rule. A formula occurs if it s-occurs or w-occurs.

Definition 14

The notion of a subformula is defined by the following conditions:

• $\varphi$ is a subformula of $\varphi$;

• if $\psi \wedge \theta$ or $\psi \vee \theta$ is a subformula of $\varphi$, then so are $\psi$ and $\theta$;

• if $@_a\psi$, $\Box \psi$, or $\Diamond \psi$ is a subformula of $\varphi$, then so is $\psi$.

The tableau system $T_{\mathrm {QH}}$ satisfies the following quasi-subformula property:

Theorem 2

(Quasi-Subformula Property). If a formula $@_a\varphi$ s-occurs in a tableau where $\varphi$ is not a nominal and $\varphi$ is not of the form $\Diamond b$, then $\varphi$ is a subformula of a root formula. If a formula $(@_a\varphi )^*$ w-occurs in a tableau, then $\varphi$ is a subformula of the premise in the applied rule.

Proof

The proof can be obtained by checking each rule.

Definition 15

Let $\varTheta$ be a branch of a tableau and let $\mathrm {Nom}^\varTheta$ be the set of nominals occurring in the formulas of $\varTheta$. Define a binary relation $\sim _\varTheta$ on $\mathrm {Nom}^\varTheta$ by $a \sim _\varTheta b$ if and only if the formula $@_a b$ occurs on $\varTheta$.

Definition 16

Let b and a be nominals occurring on a branch $\varTheta$ of a tableau in $T_{\mathrm {QH}}$. The nominal a is said to be included in the nominal b with respect to $\varTheta$ if the following holds:

• for any subformula $\varphi$ of a root formula, if the $@_a \varphi$ s-occurs on $\varTheta$, then $@_b \varphi$ also s-occurs on $\varTheta$; and

• if $(@_a \varphi )^*$ w-occurs on $\varTheta$, then $(@_b \varphi )^*$ also w-occurs on $\varTheta$.

If a is included in b with respect to $\varTheta$, and the first occurrence of b on $\varTheta$ is before the first occurrence of a, then we write $a \subseteq _\varTheta b$.

Definition 17

(Tableau Construction). Given a database $\varDelta$ of satisfaction statements and a query $@_a \varphi$ of $\mathrm {QH}$, one wants to verify if $@_a \varphi$ is a consequence of $\varDelta$. In order to do so, we define by induction a sequence $\tau _0, \tau _1, \tau _2,\cdots$ of finite tableaux in $T_{\mathrm {QH}}$, each of which is embedded in its successor.

Let $\tau _0$ be the finite tableau constituted by the formulas in $\varDelta$ and $(@_a \varphi )^*$. $\tau _{n+1}$ is obtained from $\tau _n$ if it is possible to apply an arbitrary rule to $\tau _n$ with the following three restrictions:

• 1. If a formula to be added to a branch by applying a rule already occurs on the branch, then the addition of the formula is simply omitted.

• 2. After the application of a destructive rule to a formula occurrence $\varphi$ on a branch, it is recorded that the rule was applied to $\varphi$ with respect to the branch and the rule will not again be applied to $\varphi$ with respect to the branch or any extension of it.

• 3. The existential rules $(\Diamond , \Box ^*)$ are not applied to a formula occurrence $@_a\Diamond \varphi$ or $(@_a\Box \varphi )^*$ on a branch $\varTheta$ if there exists a nominal b such that $a\subseteq _\varTheta b.$

Note that due to the first restriction, a formula cannot occur more than once on a branch. Also note that no information is recorded about applications of nondestructive rules. The conditions on applications of the existential rules $(\Diamond , \Box ^*)$ in the third restriction are the loop-check conditions. The intuition behind loopchecks is that an existential rule is not applied in a world if the information in that world can be found already in an ancestor world. Hence, the introduction of a new world by the existential rule is blocked.

A branch is closed iff there is a formula $\psi$ for which $\psi$ and $\psi ^*$ are in that branch; we use the symbol $\times$ to mark a closed branch. A $T_{\mathrm {QH}}$ tableau is closed iff every branch is closed. A branch is open if it is not closed and there are no more rules to apply; we use the symbol $\odot$ to mark an open branch. A tableau is open if it has an open branch.

A terminal tableau is a tableau where the rules have been exhaustively used i.e., there are no more rules applicable to the tableau obeying the restrictions in Definition 17.

Henceforth, $\theta$ is a branch of a terminal tableau.

Definition 18

Let U be the subset of $\mathrm {Nom}^\varTheta$ containing any nominal a having the property that there is no nominal b such that $a \subseteq _\varTheta b$. Let $\approx$ be the restriction of $\sim _\varTheta$ to U.

Note that U contains all nominals present in the root formulas since they are the first formulas of the branch $\varTheta$. Observe that $\varTheta$ is closed under the rules (Ref) and (Nom1), so both $\sim _\varTheta$ and $\approx$ are equivalence relations.

Given a nominal a in U, we let $[a]_\approx$ denote the equivalence class of a with respect to $\approx$ and we let $U/\approx$ denote the set of equivalence classes.

Definition 19

Let R be the binary relation on U defined by aRc if and only if there exists a nominal $c'\approx c$ such that one of the following two conditions is satisfied:

• 1. The formula $@_a\Diamond c'$ occurs on $\varTheta$.

• 2. There exists a nominal d in $\mathrm {Nom}^\varTheta$ such that the formula $@_a\Diamond d$ occurs on $\varTheta$ and $d \subseteq _\varTheta c'$.

Note that the nominal d referred to in the second item in the definition is not an element of U. It follows from $\varTheta$ being closed under the rule (Nom2) that R is compatible with $\approx$ in the first argument and it is trivial that R is compatible with $\approx$ in the second argument. We let $\bar{R}$ be the binary relation on $U/\approx$ defined by $[a]_\approx \,\bar{R}\,[c]_\approx$ if and only if aRc.

Definition 20

Let $\bar{N}:U\rightarrow U/\approx$ be defined as $\bar{N}(a)=[a]_\approx$.

Definition 21

Let $V^+$ be the function that to each ordinary propositional symbol assigns the set of elements of U where that propositional variable occurs, i.e., $a\in V^+(p)$ iff $@_a p$ occurs on $\varTheta$. Analogously, let $V^-$ be the function that to each ordinary propositional symbol assigns the set of elements of U where the negation of that propositional variable occurs, i.e., $a\in V^-(p)$ iff $@_a \lnot p$ occurs on $\varTheta$.

We let $V_\approx ^+$ be defined by $V_\approx ^+(p)=\{[a]_\approx \ |\ a\in V^+(p)\}$. We define $V_\approx ^-$ analogously: $V_\approx ^-(p)=\{[a]_\approx \ |\ a\in V^-(p)\}$.

Given a branch $\varTheta$, let $M^\varTheta = \left( U/\approx ,\bar{R},\bar{N}, V_\approx ^+, V_\approx ^-\right)$. We will omit the reference to the branch in $M^\varTheta$ if it is clear from the context.

Theorem 3

(Model Existence). Assume that the branch $\varTheta$ is open. For any satisfaction statement $@_a\varphi$ which contains only nominals from U, the following conditions hold:

(i) If $@_a\varphi$ s-occurs on $\varTheta$, then $M, [a]_\approx \models _s \varphi$

(ii) If $@_a\varphi$ w-occurs on $\varTheta$, then $M, [a]_\approx \models _\mathrm{w} \varphi$

(iii) If $(@_a\varphi )^*$ s-occurs on $\varTheta$, then $M, [a]_\approx \not \models _s \varphi$.

(iv) If $(@_a\varphi )^*$ w-occurs on $\varTheta$, then $M, [a]_\approx \not \models _\mathrm{w} \varphi$.

Proof

The proof is by induction on the structure of $\varphi$.

• $\varphi =i$, i a nominal

  (i) $@_a i$ s-occurs on $\varTheta$, then $[a]_\approx =[i]_\approx$, hence $M,[a]_\approx \models _s i$.

  (ii) $@_a i$ never w-occurs.

  (iii) $(@_a i)^*$ s-occurs on $\varTheta$, then, since the branch is open, $@_a i$ does not occur on $\varTheta$, in particular, it does not s-occur. So, $[a]_\approx \ne [i]_\approx$, then $M, [a]_\approx \not \models _s i$.

  (iv) $(@_a i)^*$ w-occurs on $\varTheta$, then analogously to the previous case, $@_a i$ does not occur on $\varTheta$, in particular, it does not w-occur. So, $[a]_\approx \ne [i]_\approx$, then $M, [a]_\approx \not \models _\mathrm{w} i$.

• $\varphi =\lnot i$, i a nominal

  The proof is analogous to the case $\varphi =i$.

• $\varphi =p$, p a propositional variable

  (i) $@_a p$ s-occurs on $\varTheta$, then $a\in V_\approx ^+(p)$, thus $M, [a]_\approx \models _s p$.

  (ii) $@_a p$ never w-occurs.

  (iii) $(@_a p)^*$ s-occurs on $\varTheta$, then, since the branch is open, $@_a p$ does not occur on $\varTheta$, in particular, it does not s-occur. It also means that $a\notin V_\approx ^+(p)$ so, $M, [a]_\approx \not \models _s p$.

  (iv) $(@_a p)^*$ w-occurs on $\varTheta$; analogously to the previous case, considering that $@_a p$ does not w-occur we get that $M, [a]_\approx \not \models _\mathrm{w} p$.

• $\varphi =\lnot p$, p a propositional variable

  Each case will be analogous to the one in $\varphi =p$, only with the difference that we now consider $V_\approx ^-(p)$ instead of $V_\approx ^+(p)$.

• $\varphi =\phi \wedge \psi$, $\phi , \psi$ formulas

  (i) $@_a (\phi \wedge \psi )$ s-occurs on $\varTheta$, then, by applying the S-rule ($\wedge ),$ $@_a\phi$ and $@_a\psi$ s-occur on $\varTheta$. By the induction hypothesis, $M, [a]_\approx \models _s \phi$ and $M, [a]_\approx \models _s \psi$.

  Thus, $M, [a]_\approx \models _s \phi \wedge \psi$.

  (ii) $@_a (\phi \wedge \psi )$ never w-occurs.

  (iii) $(@_a (\phi \wedge \psi ))^*$ s-occurs on $\varTheta$, then, by applying the W-rule ($\wedge ^*$), $(@_a\phi )^*$ or $(@_a\psi )^*$ w-occur on $\varTheta$.Hence, by induction hypothesis, $M, [a]_\approx \not \models _\mathrm{w} \phi$ or $M, [a]_\approx \not \models _\mathrm{w} \psi$. Thus, $M, [a]_\approx \not \models _\mathrm{w} \phi \wedge \psi$. Therefore, $M, [a]_\approx \not \models _s \phi \wedge \psi$.

  (iv) $(@_a (\phi \wedge \psi ))^*$ w-occurs on $\varTheta$; follow an analogous approach to (iii).

• $\varphi =@_i\phi$, $\phi$ a formula

  (i) $@_a @_i\phi$ s-occurs on $\varTheta$, then, by applying the S-rule (@),  $@_i\phi$ s-occurs on $\varTheta$. By the induction hypothesis, $M, [i]_\approx \models _s \phi$; thus, by the definition of satisfiability, $M, [a]_\approx \models _s @_i\phi$.

  (ii) $@_a @_i\phi$ never w-occurs.

  (iii) $(@_a @_i\phi )^*$ s-occurs on $\varTheta$, then, by applying the W-rule ($@^*$), $(@_i\phi )^*$ w-occurs on $\varTheta$. By the induction hypothesis, $M, [i]_\approx \not \models _\mathrm{w} \phi$. Thus, $M, [i]_\approx \not \models _s \phi$ and it follows that $M, [a]_\approx \not \models _s @_i\phi$.

  (iv) $(@_a @_i\phi )^*$ w-occurs on $\varTheta$; follow an analogous approach to (iii).

• $\varphi =\phi \vee \psi$, $\phi ,\psi$ formulas

  (i) $@_a (\phi \vee \psi )$ s-occurs on $\varTheta$, then, since we can apply three S-rules, namely ($\vee _1, \vee _2, \vee _3$), one may obtain 8 new branches, represented as follows:

  

  Let us check what happens at each branch:

  • 1. $(@_a (\sim \phi ))^*$, $(@_a (\sim \psi ))^*$ and $@_a\phi$ s-occur.

    By induction hypothesis:

    $M,[a]_\approx \not \models _s\sim \phi$,

    $M,[a]_\approx \not \models _s\sim \psi$, and

    $M,[a]_\approx \models _s\phi$.

    Recall that $M,[a]_\approx \models _s\phi \vee \psi$

    $\Leftrightarrow \left( M,[a]_\approx \models _s\phi \text { or } M,[a]_\approx \models _s\psi \right)$

    $\text { and } \left( M,[a]_\approx \models _s\sim \phi \Rightarrow M,[a]_\approx \models _s\psi \right)$

    $\text { and }\left( M,[a]_\approx \models _s\sim \psi \Rightarrow M,[a]_\approx \models _s\phi \right)$

    Thus, under the conditions in branch number 1, it is verified that $M,[a]_\approx \models _s\phi \vee \psi$.

  • 2. $(@_a (\sim \phi ))^*$, $(@_a (\sim \psi ))^*$ and $@_a\psi$ s-occur.

    Thus,

    $M,[a]_\approx \not \models _s\sim \phi$,

    $M,[a]_\approx \not \models _s\sim \psi$, and

    $M,[a]_\approx \models _s\psi$.

    Using the same approach as before, one has that $M,[a]_\approx \models _s\phi \vee \psi$.

  • 3. $(@_a (\sim \phi ))^*$, and $@_a\phi$ s-occur.

    Thus,

    $M,[a]_\approx \not \models _s\sim \phi$, and

    $M,[a]_\approx \models _s\phi$.

    Then, $M,[a]_\approx \models _s\phi \vee \psi$.

  • 4. $(@_a (\sim \phi ))^*$, $@_a \phi$ and $@_a\psi$ s-occur.

    Thus,

    $M,[a]_\approx \not \models _s\sim \phi$,

    $M,[a]_\approx \models _s\phi$, and

    $M,[a]_\approx \models _s\psi$.

    So, $M,[a]_\approx \models _s\phi \vee \psi$.

  • 5. $@_a\psi$, $(@_a (\sim \psi ))^*$ and $@_a \phi$ s-occur.

    Analogously to branch number 4, $M,[a]_\approx \models _s\phi \vee \psi$.

  • 6. $@_a\psi$ and $(@_a (\sim \psi ))^*$ s-occur.

    Analogously to branch number 3, $M,[a]_\approx \models _s\phi \vee \psi$.

  • 7. and 8. $@_a\phi$ and $@_a\psi$ s-occur.

    Thus, $M,[a]_\approx \models _s\phi \vee \psi$.

  We can thus conclude that, if $@_a(\phi \vee \psi )$ s-occurs, then $M,[a]_\approx \models _s\phi \vee \psi$.

  (ii) $@_a(\phi \vee \psi )$ never w-occurs.

  (iii) $(@_a(\phi \vee \psi ))^*$ s-occurs on $\varTheta$, then by applying rule ($\vee ^*$), we obtain that $(@_a\phi )^*$ and $(@_a\psi )^*$ w-occur. By induction hypothesis, $M,[a]_\approx \not \models _\mathrm{w}\phi$ and $M,[a]_\approx \not \models _\mathrm{w}\psi$; thus, $M,[a]_\approx \not \models _\mathrm{w}\phi \vee \psi$. Therefore $M,[a]_\approx \not \models _s \phi \vee \psi$.

  (iv) $(@_a(\phi \vee \psi ))^*$ w-occurs on $\varTheta$, analogous to the previous case.

• $\varphi =\Diamond \psi$, where:

  • $\psi$ is a nominal t

    For the first two cases we have that:

    (i) $@_a\Diamond t$ s-occurs on $\varTheta$, then $[a]_\approx \bar{R}[t]_\approx$. By definition of satisfiability, $M,[a]_\approx \models _s\Diamond t$.

    (ii) $@_a\Diamond t$ w-occurs on $\varTheta$; it follows from the previous explanation that $M,[a]_\approx \models _\mathrm{w}\Diamond t$.

  • $\psi$ is not a nominal

    For the first two cases we have that:

    (i) $@_a\Diamond \psi$ s-occurs on $\varTheta$, then by the application of the S-rule ($\Diamond$), $@_a\Diamond t$ and $@_t\psi$ s-occur, for t a new nominal.

    • $*$ if $t\in U$, $[a]_\approx \bar{R}[t]_\approx$ and $M,[a]_\approx \models _s\Diamond \psi$.

    • $*$ if $t\notin U$, $\exists d$ such that $t\subseteq _\varTheta d$. Assume that there is no e such that $d\subseteq _\varTheta e$, i.e., $d\in U$. By Theorem 2, the formula $\psi$ is a subformula of a root formula, so $@_d\psi$ s-occurs on $\varTheta$. By induction hypothesis, $M,[d]_\approx \models _s \psi$ and $[a]_\approx \bar{R}[d]_\approx$. Thus yielding that $M,[a]_\approx \models _s\Diamond \psi$.

    (ii) $@_a\Diamond \psi$ never w-occurs.

  • The last two cases are applicable for either $\psi$ a nominal or not:

    (iii) $(@_a\Diamond \psi )^*$ s-occurs on $\varTheta$.

    We want to prove that $M, [a]_\approx \not \models _s\Diamond \psi$, i.e., that for all $[c]_\approx$ such that $[a]_\approx \bar{R}[c]_\approx$, $M, [c]_\approx \not \models _s \psi$.

    By definition, $[a]_\approx \bar{R}[c]_\approx$ implies that $\exists c':\ c'\approx c$ that satisfies one of the following two conditions:

    • $*$ $@_a\Diamond c'$ occurs.

      Then, by the W-rule ($\Diamond ^*$), $(@_{c'} \psi )^*$ w-occurs on $\varTheta$. By induction, $M, [c']_\approx \not \models _\mathrm{w} \psi$.

      Since $[c']_\approx =[c]_\approx$, then $[a]_\approx \bar{R}[c']_\approx$. Thus, $M, [a]_\approx \not \models _\mathrm{w} \Diamond \psi$, which implies that $M, [a]_\approx \not \models _s \Diamond \psi$.

    • $*$ $\exists d\in \mathrm {Nom}^\varTheta$ such that $@_a\Diamond d$ occurs and $d\subseteq _\varTheta c'$.

      By the application of the W-rule ($\Diamond ^*$), $(@_d \psi )^*$ occurs on $\varTheta$. By Theorem 2, $\psi$ is a subformula of the premise in the applied rule.

      Since $d\subseteq _\varTheta c'$, $(@_{c'}\psi )^*$ occurs on $\varTheta$.

      By induction we conclude that $M, [c']_\approx \not \models _\mathrm{w} \psi$, thus $M, [a]_\approx \not \models _\mathrm{w} \Diamond \psi$ and finally, $M, [a]_\approx \not \models _s \Diamond \psi$.

    (iv) $(@_a\Diamond \psi )^*$ w-occurs on $\varTheta$. The proof is the same as the previous one, stopping at the point where $M, [a]_\approx \not \models _\mathrm{w} \Diamond \psi$.

• $\varphi =\Box \psi$

  In order to prove the first two cases, consider $\psi$ an arbitrary formula.

  (i) $@_a\Box \psi$ s-occurs on $\varTheta$.

  We want to prove that $M, [a]_\approx \models _s\Box \psi$, i.e., that for all $[c]_\approx$ such that $[a]_\approx \bar{R}[c]_\approx$, $M, [c]_\approx \models _s\psi$.

  As you may verify, this is a similar proof to the one made for $(@_a\Diamond \psi )^*$:

  By definition, $[a]_\approx \bar{R}[c]_\approx$ implies that $\exists c':\ c'\approx c$ that satisfies one of the following two conditions:

  • $@_a\Diamond c'$ occurs.

    Then, by the S-rule ($\Box$), $@_{c'} \psi$ s-occurs on $\varTheta$. By induction, $M, [c']_\approx \models _s \psi$.

    Since $[c']_\approx =[c]_\approx$, then $[a]_\approx \bar{R}[c']_\approx$. Thus, $M, [a]_\approx \models _s \Box \psi$.

  • $\exists d\in \mathrm {Nom}^\varTheta$ such that $_a\Diamond d$ occurs and $d\subseteq _\varTheta c'$.

    By the application of the S-rule ($\Box$), $@_d \psi$ s-occurs on $\varTheta$. By Theorem 2, $\psi$ is a subformula.

    Since $d\subseteq _\varTheta c'$, $@_{c'}\psi$ occurs on $\varTheta$.

    By induction we conclude that $M, [c']_\approx \models _s \psi$, thus $M, [a]_\approx \models _s \Box \psi$.

  (ii) $@_a\Box \psi$ never w-occurs.

  The last two cases require a separation between $\psi$ of the form $\lnot i$, with i a nominal, and not of the form described.

  Let us consider:

  • $\psi$ of the form $\lnot i$, with i a nominal.

    (iii) $(@_a\Box \lnot i)^*$ s-occurs on $\varTheta$, thus, by the rule $(\Box ^*_{\lnot i})$ which implies that $(@_a\Diamond i)$ w-occurs.

    An occurrence of $(@_a\Diamond i)$ means that $[a]_\approx \bar{R}[i]_\approx$. So, by definition, $M,[a]_\approx \models _\mathrm{w} \Diamond i$, which entails that $M,[a]_\approx \not \models _\mathrm{w} \Box \lnot i$. Therefore, $M,[a]_\approx \not \models _s \Box \lnot i$.

    (iv) $(@_a\Box \lnot i)^*$ w-occurs on $\varTheta$ follows the same approach.

  • $\psi$ otherwise.

    (iii) $(@_a\Box \psi )^*$ s-occurs on $\varTheta$, thus by application of the W-rule ($\Box ^*$), $@_a\Diamond t$ and $(@_t\psi )^*$ w-occur, for t a new nominal.

    • $*$ if $t\in U$, $[a]_\approx \bar{R}[t]_\approx$. By induction hypothesis, $M, [t]_\approx \not \models _\mathrm{w}\psi$. Thus $M,[a]_\approx \not \models _\mathrm{w}\Box \psi$. To conclude, $M,[a]_\approx \not \models _s\Box \psi$.

    • $*$ if $t\notin U$, $\exists d$ such that $t\subseteq _\varTheta d$. Assume that there is no e such that $d\subseteq _\varTheta e$, i.e., $d\in U$. By Theorem 2, the formula $\psi$ is a subformula of a root formula, so $(@_d\psi )^*$ w-occurs on $\varTheta$. By induction hypothesis, $M,[d]_\approx \not \models _\mathrm{w} \psi$ and $[a]_\approx \bar{R}[d]_\approx$. Thus yielding that $M,[a]_\approx \not \models _\mathrm{w}\Box \psi$, which, in its turn, yields $M,[a]_\approx \not \models _s\Box \psi$.

    (iv) $(@_a\Box \psi )^*$ s-occurs on $\varTheta$; the proof is the same as before, stopping at $M,[a]_\approx \not \models _\mathrm{w}\Box \psi$, which already gives the desired result.

From this theorem together with the soundness theorem we have the following decision procedure:

Decision Procedure: Given a database $\varDelta$ and a query $@_a\varphi$ whose consequence from $\varDelta$ we want to decide, let $\tau _n$ be a terminal tableau generated by the tableau construction algorithm. If the tableau is closed, then $@_a\varphi$ is a consequence of $\varDelta$ . Analogously, if the tableau is open, then $@_a\varphi$ is not a consequence of $\varDelta$.

Example 1

Let $\varDelta =\{@_i(p\vee q), @_j\Diamond i, @_j q, @_j \lnot q \}$ be a database and consider a query $\varphi =@_j\Diamond p$. Let us decide if $\varphi$ is a consequence of $\varDelta$ using the tableau procedure described:

Since the tableau has some open branches, it means that the tableau is open, thus $\varphi$ is not a consequence of $\varDelta$. A counter-model is the bistructure with two worlds i and j where only $@_i q$, $@_j q$, $@_j\lnot q$ and $@_j\Diamond i, @_i\Box \lnot i$, $@_j\Box \lnot j$ are satisfied, which clearly is a bistructure that satisfies $\varDelta$, but where $\varphi$ is not true.

We can easily verify that the database has an inconsistency, as it contains both $@_j q$ and $@_j \lnot q$. If we were to evaluate $\varphi$ in hybrid logic (usual version, non-paraconsistent), then $\varphi$ would trivially follow.

Example 2

Let $\varDelta =\{@_t(p \wedge q\wedge r), @_i\Box \lnot p, @_i\Diamond t\}$ be a database and consider a query $\varphi =(@_t(p\wedge \lnot p))$. Let us decide if $\varphi$ is a consequence of $\varDelta$ using the tableau procedure described:

Note that the database has an inconsistency and the query itself is inconsistent. However, from the tableau procedure we verify that, since it is closed, $\varphi$ is a consequence of $\varDelta$.

These examples show the mechanism of the tableau construction in action. Both examples yield an inconsistency in the database, but it is possible to still reach sensible conclusions about the validity of the query, thanks to the paraconsistent aspect of the tableau system presented.

5 Conclusion

Paraconsistent logics have been around for some decades, and their importance is justified by the unavoidable occurrence of inconsistencies in data and knowledge management. Inconsistent information can appear everywhere, and for many reasons. Contradictory information may arise in systems which are safety critical, such as health systems, aviation systems and many others.

After introducing Quasi-hybrid logic [5], a paraconsistent version of hybrid logic capable of dealing with contradictory information under the form of hybrid formulas, the next step was the construction of a proof-theoretical system for this new logic and the study of properties such as completeness, decidability, etc.

The challenge here was the combination of two different tableau systems already existent in literature, one for Quasi-classical logic and another for Hybrid logic. We ended up with a tableau system for Quasi-hybrid logic, described in this work, which ends with some examples.

This is clearly a step forward in the study of $\mathrm {QH}$ logic, which we aim to continue exploring, namely by:

• investigating inconsistency at the level of nominals, by allowing two nominations: a positive one for nominals, and a negative one for the negation of nominals. This way, we are able to handle the possibility of receiving information of the form $@_i j$ and $@_i\lnot j$;

• accounting for inconsistency in modalities, for example by allowing both $@_i\Diamond j$ and $@_i\Box \lnot j$ to be true;

• studying paraconsistency in the context of strong Priorean logic;

• use a combination of all of the above to study reactive deontic logics and switch graphs, where the base accessibility relation changes when its edges are traversed, in the context of $\mathrm {QH}$ logic.

Paraconsistency has already been considered in the context of modal logic (e.g. [9, 10]). It will be interesting to compare our system with the hybrid systems obtained by adding nominals and the satisfaction operator to those systems.