Abstract
Qualitative spatial reasoning is concerned with the qualitative aspects of representation and reasoning about spatial entities as opposed to one-dimensional situations. It aims to express non-numerical relationships among spatial regions. The basic concepts in most of these theories are ‘part of’ and ‘connection’ relations which are the typical examples of a more general notion of a ‘contact’ relation.
Access provided by Autonomous University of Puebla. Download chapter PDF
Similar content being viewed by others
1 Introduction
Qualitative spatial reasoning is concerned with the qualitative aspects of representation and reasoning about spatial entities as opposed to one-dimensional situations. It aims to express non-numerical relationships among spatial regions. The basic concepts in most of these theories are ‘part of’ and ‘connection’ relations which are the typical examples of a more general notion of a ‘contact’ relation.
The formalization of ‘part of’ relationship goes back to the mereological systems of Stanisław Leśniewski developed from 1916 onwards [Leś16, Leś29, Leś31]. Next, based on an earlier work of de Laguna [dL22], Whitehead [Whi29] introduced a kind of connection relation as a basic relation between regions. His system includes Leśniewski’s mereology. Later, Grzegorczyk [Grz60] and Clarke [Cla81] presented an axiomatization of Whitehead’s relation.
One of the more recent spatial theories is the Region Connection Calculus, RCC, introduced in [RCC92]. The primitive concept of this theory is a binary relation of ‘connection’ between regions. Intuitively, in terms of points incident in regions, two regions are connected whenever they share a common point. With the connection relation a set of the other spatial relations is defined. These relations describe different connections between regions such as being externally connected, partially overlapping, being a tangential part of, and so on. In the theory RCC all meaningful degrees of connection are formally defined. The fundamental structure considered in the theory is a Boolean algebra endowed with a contact relation satisfying certain axioms.
Spatial theories having as a basic concept a proximity relation, first considered in [Efr52], are investigated in [NW70, DV07, VDDB02, VDB01], among others. The proximity relation is a binary relation between subsets of a non-empty set, which holds between the two sets whenever, intuitively, they are near in some sense. The proximity relation satisfies axioms which are among the typical axioms of the connection relation. The spatial intuition of proximity is also formalized in terms of nearness spaces as presented in [BdRV01]. A natural counterpart to the proximity and nearness spaces are the apartness spaces introduced in [BD03]. In [DO08] the apartness algebras and apartness frames are defined which lead to an intuitionistic logic with a sufficiency operation. Consequently, a dual tableau for such a logic can be developed based on the dual tableau for intuitionistic logic presented in Sect. 8.2 and on the developments of Sect. 11.5 where the rules for a sufficiency operation are discussed.
Qualitative spatial reasoning from a philosophical perspective is discussed in [Sim87] and from a relation algebraic perspective in [Dün05].
In this chapter we consider four types of spatial theories: theories based on a plain contact relation, theories based on Boolean algebras additionally equipped with a contact relation, theories of region connection calculus, and theories based on a proximity relation. All of these theories, except for those from the first group that are based on logic RL(1, 1′), are presented as first-order theories of appropriate classes of relations, following the developments in [Dün01b, DWM99, DOW01, DWM01, Ste00, VDDB02]. This enables us to construct their proof systems in a uniform way.
2 Dual Tableaux for Spatial Theories Based on a Plain Contact Relation
Typically, the most basic notion of theories for spatial reasoning is that of a contact relation [Cla81, Dün01b]. In this section we consider theories of the class of relation algebras generated by a binary relation C interpreted as a contact relation. This class is denoted by CRA. Each of these theories has some specific axioms that characterize relation C. One of them has the following axioms (see [DO00b]):
(C1) C is reflexive;
(C2) C is symmetric;
(C3) If C(a) = C(b), then a = b, where C(x) = { y : xCy}.
Axiom (C3) is referred to as the extensionality axiom.
In terms of a contact relation, several mereological relations can be defined. In Table 18.1 we list some typical relations of that kind.
The language of the relational logic RL CRA , adequate for reasoning in relation algebras generated by a contact relation, is RL(1, 1′)-language with:
-
\({\mathbb{R}\mathbb{V}}_{{\mathsf{RL}}_{\mathsf{CRA}}} = \varnothing \);
-
\({\mathbb{R}\mathbb{C}}_{{\mathsf{RL}}_{\mathsf{CRA}}} =\{ 1,1^{\prime},C\}\).
An RL CRA -model is a structure \(\mathcal{M} = (\mathcal{U},\mathcal{C},\Updownarrow )\) such that (U, m) is an RL(1, 1′)-model, C is a reflexive and symmetric relation on U such that m(C) = C and, in addition:
(ext C) If {z ∈ U : (x, z) ∈ C} = { z ∈ U : (y, z) ∈ C}, then (x, y) ∈ m(1′).
Note that the above condition is a counterpart to the extensionality axiom (C3) although the meaning of 1′ may not be the identity. RL CRA -models in which 1′ is interpreted as the identity relation are referred to as standard models.
An RL CRA -dual tableau consists of the rules and the axiomatic sets of the logic RL(1, 1′) and the following specific rules reflecting the axioms of contact relation C.
For any object symbols x and y,
We can prove soundness and completeness of RL CRA following the method developed for RL(1, 1′)-logic. As usual, RL CRA -sets of formulas are defined as in Sect. 2.4, i.e., the first-order disjunction of their members is valid. Correctness of a rule is defined as in Sect. 2.4.
Proposition 18.2.1.
The rules (ref C), (sym C), and (ext C) are RL CRA -correct.
Proof.
The rules (ref C) and (sym C) reflect reflexivity and symmetry of the relation C, respectively, as it is shown in Theorem 6.6.1. Now, we prove correctness of the rule (ext C). Let X be a finite set of RL CRA -formulas. Let x, y be any object symbols and let z be an object variable that does not occur in X and such that z≠x, y. Clearly, if X is an RL CRA -set, then so are X ∪{ x − Cz, yCz}, X ∪{ y − Cz, xCz}, and X ∪{ x − 1′y}. Now, assume that X ∪{ x − Cz, yCz}, X ∪{ y − Cz, xCz}, and X ∪{ x − 1′y} are RL CRA -sets. Suppose X is not an RL CRA -set, that is there exist an RL CRA -model \(\mathcal{M} = (\mathcal{U},\mathcal{C},\Updownarrow )\) and a valuation v in \(\mathcal{M}\) such that \(\mathcal{M},\sqsubseteq \nvDash \varphi \), for every φ ∈ X. It follows from the assumption that model \(\mathcal{M}\) and valuation v satisfy:\(\mathcal{M},\sqsubseteq \models \S -\mathcal{C}\ddag \ \text{ or}\ \mathcal{M},\sqsubseteq \models \dag \mathcal{C}\ddag ;\) \(\mathcal{M},\sqsubseteq \models \dag -\mathcal{C}\ddag \ \text{ or}\ \mathcal{M},\sqsubseteq \models \S \mathcal{C}\ddag ;\) \(\mathcal{M},\sqsubseteq \models \S -\infty ^{\prime}\dag .\)
By the assumption on variable z, for every a ∈ U the following hold:
If (v(x), a) ∈ C, then (v(y), a) ∈ C;If (v(y), a) ∈ C, then (v(x), a) ∈ C;(v(x), v(y)) ∉ m(1′).
Thus {z ∈ U : (v(x), z) ∈ C} = { z ∈ U : (v(y), z) ∈ C} and (v(x), v(y)) ∉ m(1′). However, the condition (ext C) implies (v(x), v(y)) ∈ m(1′), a contradiction.
By the above proposition and since correctness of all the remaining rules can be proved as in RL(1, 1′)-logic (see Sects. 2.5 and 2.7), we get:
Proposition 18.2.2.
-
1.
The RL CRA -rules are RL CRA -correct;
-
2.
The RL CRA -axiomatic sets are RL CRA -sets.
The notions of an RL CRA -proof tree, a closed branch of such a tree, a closed RL CRA -proof tree, and RL CRA -provability are defined as in Sect. 2.4.
A branch b of an RL CRA -proof tree is complete whenever it is closed or it satisfies the completion conditions of RL(1, 1′)-dual tableau and the following conditions specific for the RL CRA -dual tableau:
For any object symbols x and y,
Cpl(ref C) If xCy ∈ b, then x1′y ∈ b, obtained by an application of the rule (ref C);Cpl(sym C) If xCy ∈ b, then yCx ∈ b, obtained by an application of the rule (sym C);Cpl(ext C) Either x − 1′y ∈ b or there exists an object variable z such that either (x − Cz ∈ b and yCz ∈ b) or (y − Cz ∈ b and xCz ∈ b), obtained by an application of the rule (ext C).
The notions of a complete RL CRA -proof tree and an open branch of an RL CRA -proof tree are defined as in RL-logic (see Sect. 2.5). Observe that the rules of RL CRA -dual tableau, in particular the specific rules (ref C), (sym C), and (ext C), guarantee that whenever a branch of an RL CRA -proof tree contains formulas xRy and x − Ry, for an atomic term R, then the branch can be closed. Thus, the closed branch property can be proved as in Proposition 2.8.1.
The branch structure \({\mathcal{M}}^{\lfloor } = ({\mathcal{U}}^{\lfloor },{\mathcal{C}}^{\lfloor },{\Updownarrow }^{\lfloor })\) is defined in the standard way (see Sect. 2.6, p. 44), in particular m b(C) = C b = { (x, y) ∈ U b ×U b : xCy ∉ b}.
Proposition 18.2.3 (Branch Model Property).
Let b be an open branch of an RL CRA -proof tree. Then, the branch structure \({\mathcal{M}}^{\lfloor } = ({\mathcal{U}}^{\lfloor },{\mathcal{C}}^{\lfloor },{\Updownarrow }^{\lfloor })\) is an RL CRA -model.
Proof.
It suffices to show that C b is reflexive, symmetric, and it satisfies the condition (ext C). By the completion conditions Cpl(ref C) and Cpl(sym C), it easily follows that C b is reflexive and symmetric. To prove the extensionality property of C b, let x, y ∈ U b be such that {z ∈ U b : (x, z) ∈ C b} = { z ∈ U b : (y, z) ∈ C b}. By the completion condition Cpl(ext C), either x − 1′y ∈ b or there exists an object variable z, such that either (x − Cz ∈ b and yCz ∈ b) or (y − Cz ∈ b and xCz ∈ b). If x − 1′y ∈ b, then x1′y ∉ b, since otherwise, by the closed branch property, b would be closed. Hence, (x, y) ∈ m b(1′). If for some z ∈ U b, x − Cz ∈ b and yCz ∈ b, then (x, z) ∈ C b and (y, z) ∉ C b. Thus, {z ∈ U b : (x, z) ∈ C b}≠{z ∈ U b : (y, z) ∈ C b}, a contradiction. If there is z ∈ U b such that y − Cz ∈ b and xCz ∈ b, then (y, z) ∈ C b and (x, z) ∉ C b, which also contradicts the assumption.
Since m b(C) is defined in a standard way, the satisfaction in branch model property can be proved as in RL(1, 1′)-logic (see Sects. 2.5 and 2.7). Hence, completeness of RL CRA -dual tableau follows.
Theorem 18.2.1 (Soundness and Completeness of RL CRA ).
For every RL CRA -formula φ, the following conditions are equivalent:
-
1.
φ is RL CRA -valid;
-
2.
φ is true in all standard RL CRA -models;
-
3.
φ is RL CRA -provable.
In order to reason directly about the mereological relations definable from the contact relation C, we can develop the relational logic RL Mer which is obtained from RL CRA by adding to its language the set of relational constants Mer = { P, PP, O, PO, EC, TPP, NTPP, DC, DR}. An RL Mer -structure is a system \(\mathcal{M} = (\mathcal{U},\mathcal{C},\{\# : \# \in \mathsf{Mer}\},\Updownarrow )\), where (U, C, m) is an RL CRA -model and m(#) = # ⊆ U ×U, for every relational constant # ∈ Mer. An RL Mer -model is an RL Mer -structure \(\mathcal{M} = (\mathcal{U},\mathcal{C},\{\# : \# \in \mathsf{Mer}\},\Updownarrow )\) such that relations from Mer are defined by conditions given in Table 18.1. We slightly abuse the notation here by identifying symbols of the language with the corresponding entities in the models.
A dual tableau for RL Mer consists of the rules and the axiomatic sets of RL CRA -dual tableau, and the following specific rules that reflect the definitions of mereological relations in terms of the contact relation C:
For all object symbols x and y,
The alternative forms of the rules above are discussed in Sect. 25.9.
Let \(\mathcal{K}\) be a class of RL Mer -structures. The notion of a \(\mathcal{K}\)-set and the notion of \(\mathcal{K}\)-correctness of a rule are defined as in Sect. 2.4.
Theorem 18.2.2 (Correspondence).
Let \(\mathcal{K}\) be a class of RL Mer -structures and let # ∈ Mer ={ P,O, PO,PP, EC, TPP, NTPP, DC, DR}. Then, the following conditions are equivalent:
-
1.
\(\mathcal{K}\) is the class of RL Mer -models;
-
2.
For every # ∈ Mer, the rules (#) and (−#) are \(\mathcal{K}\)-correct.
Proof.
(1. → 2. ) Assume that \(\mathcal{K}\) is the class of RL Mer -models. By way of example, we prove correctness of the rules (P) and ( − P).
(P) Let X be a finite set of RL Mer -formulas and let z be a variable that does not occur in X and z≠x, y. Assume X ∪{ xPy} is an RL Mer -set and suppose that X ∪{ x − Cz, zCy} is not an RL Mer -set. It follows that there is an RL Mer -model \(\mathcal{M}\) and a valuation v in \(\mathcal{M}\) such that for every φ ∈ X, \(\mathcal{M},\sqsubseteq \nvDash \varphi \) and, moreover, (v(x), v(z)) ∈ C and (v(z), v(y)) ∉ C, that is (v(x), v(y)) ∈ (C ; − C). However, by the assumption, (v(x), v(y)) ∈ P, which by the condition P ⊆ − (C ; − C) implies (v(x), v(y)) ∉ (C ; − C), a contradiction. Now, assume that X ∪{ x − Cz, zCy} is an RL Mer -set. Then, by the assumption on variable z, for every RL Mer -model \(\mathcal{M}\) and for every valuation v in \(\mathcal{M}\), either there exists φ ∈ X such that \(\mathcal{M},\sqsubseteq \models \varphi \) or for every z ∈ U, (v(x), z) ∉ C or (z, v(y)) ∈ C, that is (v(x), v(y)) ∉ (C ; − C). Suppose X ∪{ xPy} is not an RL Mer -set. Then, there exist an RL Mer -model \(\mathcal{M}\) and a valuation v such that (v(x), v(y)) ∉ P. Thus, by the condition − P ⊆ (C ; − C), (v(x), v(y)) ∈ (C ; − C), a contradiction. Therefore, the rule (P) is RL Mer -correct.
( − P) Let X be a finite set of RL Mer -formulas. Clearly, if X ∪{ x − Py} is an RL Mer -set, then so are X ∪{ xCz, x − Py} and X ∪{ z − Cy, x − Py}. Now, assume that X ∪{ xCz, x − Py} and X ∪{ z − Cy, x − Py} are RL Mer -sets. Suppose X ∪{ x − Py} is not an RL Mer -set. Then, there exist an RL Mer -model \(\mathcal{M}\) and a valuation v in \(\mathcal{M}\) such that for every φ ∈ X, \(\mathcal{M},\sqsubseteq \nvDash \varphi \) and (v(x), v(y)) ∈ P. It follows that for every w ∈ U, either (v(x), w) ∉ C or (w, v(y)) ∈ C. However, by the assumption there exists w ∈ U such that (v(x), w) ∈ C and (w, v(y)) ∉ C, a contradiction. Therefore, the rule ( − P) is RL Mer -correct.
(2. → 1. ) Assume that for every # ∈ Mer, the rules (#) and ( − #) are \(\mathcal{K}\)-correct. We need to show that relations from Mer satisfy equations given in Table 18.1. By way of example, we show that P = − (C ; − C).
( ⊆ ) By correctness of the rule ( − P), for every finite set X of RL Mer -formulas, X ∪{ x − Py} is a \(\mathcal{K}\)-set iff X ∪{ xCz, x − Py} and X ∪{ z − Cy, x − Py} are \(\mathcal{K}\)-sets. Let \(X{ \mathrm{df} \atop =} \{x-Cz,zCy\}\). By the assumption, {x − Py, x − Cz, zCy} is a \(\mathcal{K}\)-set. Thus, for every \(\mathcal{K}\)-structure \(\mathcal{M}\) and for every valuation v in \(\mathcal{M}\), if (v(x), v(z)) ∈ C and (v(z), v(y)) ∉ C, then (v(x), v(y)) ∉ P. Thus, if (v(x), v(y)) ∈ (C ; − C), then (v(x), v(y)) ∉ P, and hence P ⊆ − (C ; − C).
( ⊇ ) By correctness of the rule (P), for every finite set X of RL Mer -formulas and for every variable z that does not occur in X and such that z≠x, y, X ∪{ xPy} is a \(\mathcal{K}\)-set iff X ∪{ x − Cz, zCy} is a \(\mathcal{K}\)-set. Let \(X{ \mathrm{df} \atop =} \{x(C\,;\,-C)y\}\). Then, by the assumption on variable z, X ∪{ x − Cz, zCy} is a \(\mathcal{K}\)-set. Thus, by \(\mathcal{K}\)-correctness of the rule ( − P), {xPy, x(C ; − C)y} is a \(\mathcal{K}\)-set. Hence, − (C ; − C) ⊆ P.
The above theorem implies:
Proposition 18.2.4.
-
1.
The RL Mer -rules are RL Mer -correct;
-
2.
The RL Mer -axiomatic sets are RL Mer -sets.
In order to prove completeness, we need to define the completion conditions corresponding to the rules specific for RL Mer -dual tableau, i.e., the rules (P), ( − P), (O), ( − O), (PP), ( − PP), (EC), ( − EC), (DR), and ( − DR).
For all object symbols x and y,
Cpl(P) If xPy ∈ b, then for some object variable z, both x − Cz ∈ b and zCy ∈ b, obtained by an application of the rule (P);Cpl( − P) If x − Py ∈ b, then for every object symbol z, either xCz ∈ b or z − Cy ∈ b, obtained by an application of the rule ( − P);Cpl(PP) If xPPy ∈ b, then either xPy ∈ b or x − 1′y ∈ b, obtained by an application of the rule (PP);Cpl( − PP) If x − PPy ∈ b, then both x − Py ∈ b and x1′y ∈ b, obtained by an application of the rule ( − PP);Cpl(O) If xOy ∈ b, then for every object symbol z, either zPx ∈ b or zPy ∈ b, obtained by an application of the rule (O);Cpl( − O) If x − Oy ∈ b, then for some object variable z, both z − Px ∈ b and z − Py ∈ b, obtained by an application of the rule ( − O);Cpl(PO) If xPOy ∈ b, then either xOy ∈ b or x − Py ∈ b or y − Px ∈ b, obtained by an application of the rule (PO);Cpl( − PO) If x − POy ∈ b, then x − Oy ∈ b and xPy ∈ b and yPx ∈ b, obtained by an application of the rule ( − PO);Cpl(EC) If xECy ∈ b, then either xCy ∈ b or x − Oy ∈ b, obtained by an application of the rule (EC);Cpl( − EC) If x − ECy ∈ b, then both x − Cy ∈ b and xOy ∈ b, obtained by an application of the rule ( − EC);Cpl(TPP) If xTPPy ∈ b, then either xPPy ∈ b or for every object symbol z, xECz ∈ b or zECy ∈ b, obtained by an application of the rule (TPP);Cpl( − TPP) If x − TPPy ∈ b, then xPPy ∈ b and for some object variable z, both x − ECz ∈ b and z − ECy ∈ b, obtained by an application of the rule ( − TPP);Cpl(NTPP) If xNTPPy ∈ b, then either xPPy ∈ b or x − TPPy ∈ b, obtained by an application of the rule (NTPP);Cpl( − NTPP) If x − NTPPy ∈ b, then both x − PPy ∈ b and xTPPy ∈ b, obtained by an application of the rule ( − NTPP)Cpl(DC) If xDCy ∈ b, then x − Cy ∈ b, obtained by an application of the rule (DC);Cpl( − DC) If x − DCy ∈ b, then xCy ∈ b, obtained by an application of the rule ( − DC);Cpl(DR) If xDRy ∈ b, then x − Oy ∈ b, obtained by an application of the rule (DR);Cpl( − DR) If x − DRy ∈ b, then xOy ∈ b, obtained by an application of the rule ( − DR).
The notions of a complete RL Mer -proof tree and an open branch of an RL Mer -proof tree are defined as in RL-logic (see Sect. 2.5).
The following form of the closed branch property holds:
Fact 18.2.1
(Closed Branch Property). For every branch of an RL Mer -proof tree, if xRy and x−Ry, for an atomic \(R \in \mathsf{Mer} \setminus \{ P,-O,-TPP\}\), belong to the branch, then the branch is closed.
Although it does not concern the relational constants P, − O, and − TPP, it is sufficient for proving satisfaction in branch model property, see Proposition 18.2.5. The reason is that the rules for these constants reflect their corresponding definitions in logic RL Mer .
Let b be an open branch of an RL Mer -proof tree. The branch structure \({\mathcal{M}}^{\lfloor }\,=\) (U b, C b, {# b : # ∈ Mer}, m b) is defined as in the completeness proof of RL CRA -dual tableau with the following additional clauses:
-
For every # ∈ Mer, # b is defined according to Table 18.1; for example, \({O}^{b}{ \mathrm{df} \atop =} {({P}^{-1})}^{b}\,;\,{P}^{b}\).
-
m b(#) = # b.
By the above definition, \({\mathcal{M}}^{\lfloor }\) is an RL Mer -model, hence the branch model property holds. Now, we prove the satisfaction in branch model property.
Proposition 18.2.5 (Satisfaction in Branch Model Property).
Let b be an open branch of an RL Mer -proof tree. Then, for every RL Mer -formula φ, if \({\mathcal{M}}^{\lfloor },{\sqsubseteq }^{\lfloor }\models \varphi \) , then φ∉b.
Proof.
We need to show that the proposition holds for every relational constant # and its complement, for # ∈ Mer. By way of example, we prove the required condition for the relational constant O and for − EC.
( − O) Assume that \({\mathcal{M}}^{\lfloor }\) and v b satisfy a formula x − Oy, that is (x, y) ∉ O b. By the definition of O b, for every z ∈ U b, either (z, x) ∉ P b or (z, y) ∉ P b. Suppose x − Oy ∈ b. By the completion condition Cpl( − O), there exists z ∈ U b such that z − Px ∈ b and z − Py ∈ b. By the completion condition Cpl( − P), there exists z ∈ U b such that for every u ∈ U b, either zCu ∈ b or u − Cx ∈ b, and for every t ∈ U b, either zCt ∈ b or t − Cy ∈ b. Thus, by the induction hypothesis, there exists z ∈ U b such that for every u ∈ U b, either (z, u) ∉ C b or (u, x) ∈ C b, and for every t ∈ U b, either (z, t) ∉ C b or (t, y) ∈ C b. Therefore, there exists z ∈ U b such that (z, x) ∉ (C b ; − C b) and (z, y) ∉ (C b ; − C b). Hence, (z, x) ∈ P b and (z, y) ∈ P b, a contradiction.
( − EC) Assume \({\mathcal{M}}^{\lfloor },{\sqsubseteq }^{\lfloor }\models \S -\mathcal{E}\mathcal{C}\dag \), that is (x, y) ∉ EC b. Then, either (x, y) ∉ C b or (x, y) ∈ O b. Suppose x − ECy ∈ b. By the completion condition Cpl( − EC), x − Cy ∈ b and xOy ∈ b. By the induction hypothesis, (x, y) ∈ C b and (x, y) ∉ O b, a contradiction.
The proofs of the remaining cases are similar.
Finally, we obtain:
Theorem 18.2.3 (Soundness and Completeness of RL { Mer} ).
For every RL Mer -formula φ, the following conditions are equivalent:
-
1.
φ is RL Mer -valid;
-
2.
φ is true in all standard RL Mer -models;
-
3.
φ is RL Mer -provable.
An RL Mer -proof of \(P \cap DC = \varnothing \)
An RL Mer -proof of PP ; PP ⊆ PP
Example.
In Figs. 18.1–18.3 we present examples of RL Mer -proofs of some properties of mereological relations. We show that \(P \cap DC = \varnothing \) by showing that − P ∪ − DC is the universal relation (Fig. 18.1). Then we show that (PP ; PP) ⊆ PP by constructing an RL Mer -proof of the formula x( − (PP ; PP) ∪PP)y (Fig. 18.2). Finally, we prove that P is antisymmetric, i.e., P ∩ P − 1 ⊆ 1′, by constructing an RL Mer -proof of the formula x( − (P ∩ P − 1) ∪1′)y (Fig. 18.3).
3 Dual Tableaux for Spatial Theories Based on a Contact Relation on a Boolean Algebra
In this section we present a first-order theory of Boolean algebras with a contact relation. Such structures are considered, for example, in [Ste00, DW08].
An RL Mer -proof of antisymmetry of the ‘part of’ relation P
The language of the first-order theory of Boolean algebras, F BA fun , is a first-order language with the identity and function symbols (cf. Sect. 1.2) representing the Boolean operations from fun = { − , ∨ , ∧ } and the Boolean constants 0 and 1. The language of the first-order theory of Boolean algebras with a contact relation, F BAC fun , is an F BA fun -language endowed with the relational constant C. F BAC fun -models are Boolean algebras with a contact relation C satisfying some of the following conditions.
Let (U, − , ∨ , ∧ , 0, 1) be a Boolean algebra, let C be a binary relation on U, let a, b, c ∈ U, and let ≤ be the Boolean ordering on U.
(C0) If aCb, then a, b≠0;
(C1) If a≠0, then aCa.
Sometimes, a stronger axiom is postulated instead of (C1):
(C2) If a ∧ b≠0, then aCb.
Further axioms include:
(C3) C is symmetric;
(C4) C is reflexive;
(C5) If aCb and b ≤ c, then aCc;
(C6) If aC(b ∨ c), then aCb or aCc;
(C7) If C(a) ⊆ C(b), then a ≤ b.
Observe that (C7) follows from (C3) and (C5). The other typical axioms are:
- (C8):
-
If not aCb, then there is c such that not aCc and not ( − c)Cb;
- (C9):
-
If a, b≠0 and a ∨ b = 1, then aCb;
- (C10):
-
If a≠1, then there exists b≠0 such that not bCa.
In the presence of the axioms (C0), …, (C6) axiom (C9) is equivalent to:
(C11) If a≠0, 1, then aC( − a).
The primitive notions of F BA fun and F BAC fun can be equivalently presented in purely relational terms by elimination of function symbols. The binary Boolean operations ∨ and ∧ are represented as ternary relations R ∨ and R ∧, respectively, and the Boolean complement − as a binary relation R −. Relations R −, R ∨, R ∧ are intended to reflect the following intuitions:
Then the formalism appropriate for reasoning in the spatial theories involving these relations is a first-order theory of binary relations C and R −, and ternary relations R ∨ and R ∧. It will be denoted by F BAC . Similarly, F BA denotes a first-order language, without function symbols, of the theory of Boolean algebras.
An F BA -model is a structure \(\mathcal{M} = (\mathcal{U},{\mathcal{R}}_{-},{\mathcal{R}}_{\vee },{\mathcal{R}}_{\wedge },{\prime},\infty ,\Updownarrow )\) such that (U, m) is an F-model defined in Sect. 1.2, R − is a binary relation on U interpreting the relational constant R −, R ∨ and R ∧ are ternary relations on U interpreting the relational constants R ∨ and R ∧, respectively, and 0, 1 are distinguished elements of U interpreting object constants from the language. An F BA -model is standard whenever the interpretation of = is the identity. As usual, we slightly abuse the notation using the same symbols for the relational constants in the language and for the corresponding relations in the models.
A valuation in a model \(\mathcal{M} = (\mathcal{U},{\mathcal{R}}_{-},{\mathcal{R}}_{\vee },{\mathcal{R}}_{\wedge },{\prime},\infty ,\Updownarrow )\) is a function \(v:{ \mathbb{O}\mathbb{V}}_{{\mathsf{F}}_{\mathsf{BA}}} \cup \{ 0,1\} \rightarrow U \cup \{ 0,1\}\) such that v(1) = 1 and v(0) = 0. The satisfaction relation, truth in a model, and validity are defined as in F-logic in Sect. 1.2.
F BA -models are assumed to satisfy the following semantic conditions reflecting the role of the axioms of Boolean algebras:
For # ∈ { ∨ , ∧ } and for all x, y, z,
- (ReBA0):
-
There is z such that R −(x, z);
- (ReBA1):
-
R −(z, x) and R −(z, y) imply x = y;
- (ReBA2#):
-
There is z such that R # (x, y, z);
- (ReBA3#):
-
R # (z, t, x) and R # (z, t, y) imply x = y.
The above conditions encode the fact that R − and R # , for # ∈ { ∨ , ∧ }, are functions.
- (ReBA4#):
-
R # (x, y, z) iff R # (y, x, z);
- (ReBA5#):
-
There are t, u such that R # (x, y, t) and R # (t, z, u) iff there are t′, u′ such that R # (y, z, t′) and R # (x, t′, u′);
- (ReBA6):
-
There are t, u such that R ∨(x, y, t) and R ∧(t, z, u) iff there are t′, u′ such that R ∧(x, z, t′) and R ∧(y, z, u′) and R ∨(t′, u′, u);
- (ReBA7):
-
There are t, u such that R ∧(x, y, t) and R ∨(t, z, u) iff there are t′, u′ such that R ∨(x, z, t′) and R ∨(y, z, u′) and R ∧(t′, u′, u).
These conditions encode the properties of join and meet, namely commutativity (ReBA4), associativity (ReBA5), and distributivity ((ReBA6) and (ReBA7)).
Boolean constants 0 and 1 are characterized with the conditions:
- (ReBA8):
-
R ∨(x, 0, x);
- (ReBA9):
-
R ∧(x, 1, x);
- (ReBA10):
-
There is y such that R −(x, y), R ∨(x, y, 1), and R ∧(x, y, 0).
F BAC -models are the structures \(\mathcal{M} = (\mathcal{U},{\mathcal{R}}_{-},{\mathcal{R}}_{\vee },{\mathcal{R}}_{\wedge },\mathcal{C},{\prime},\infty ,\Updownarrow )\) such that (U, R −, R ∨, R ∧, 0, 1, m) is an F BA -model and C is a binary relation on U. The relation C may satisfy some of the conditions (ReC0), …, (ReC11) which correspond to the conditions (C0), …, (C11), respectively.
Let x, y, z, t ∈ U. Then:
-
If C(x, y), then x≠0 and y≠0;
-
If x≠0, then C(x, x);
-
If R ∧(x, y, 0), then C(x, y);
-
If C(x, y), then C(y, x);
-
If x = y, then C(x, y);
-
If C(x, z) and R ∨(z, y, y), then C(x, y);
-
If C(x, t) and R ∨(y, z, t), then C(x, y) or C(x, z);
-
If for all z ∈ U, C(x, z) implies C(y, z), then R ∨(x, y, y);
-
If C(x, y), then there are z, t such that not C(x, z) and R −(z, t) and not C(t, y);
-
If x≠0, y≠0, and R ∨(x, y, 1), then C(x, y);
-
If x≠1, then there exists z such that z≠0 and ¬C(z, x);
-
If x≠0 and x≠1, then there exists z such that C(x, z) and R −(x, z).
Observe that R ∨(x, y, y) iff x ≤ y.
Theorem 18.3.1.
For every F BAC fun -formula φ, there is an F BAC -formula φ′ such that φ is true in all F BAC fun -models satisfying some of the axioms from {(C0), …, (C11)} iff φ′ is true in all F BAC -models satisfying the corresponding conditions from {(ReC0), …, (ReC11)}.
In order to prove the above theorem, it suffices to show: (1) for every F BAC fun -model \(\mathcal{M}\) there exists an F BAC -model \(\mathcal{M}^{\prime}\) such that ( ∗ ) φ is true in \(\mathcal{M}\) iff φ′ is true in \(\mathcal{M}^{\prime}\), and (2) for every standard F BAC -model \(\mathcal{M}^{\prime}\) there exists an F BAC fun -model \(\mathcal{M}\) such that ( ∗ ) holds. We construct the models \(\mathcal{M}\) and \(\mathcal{M}^{\prime}\) so that they satisfy: (Ci) is true in \(\mathcal{M}\) iff (ReCi) is true in \(\mathcal{M}^{\prime}\), for i ∈ { 0, …, 11}, and the same holds for the axioms of Boolean algebras and the conditions (ReBA0), (ReBA1), (ReBA2#), (ReBA3#), (ReBA4#), (ReBA5#), for # ∈ { ∨ , ∧ }, and (ReBA7), …, (ReBA10).
F BAC -dual tableau contains the axiomatic sets and the rules of F-dual tableau adjusted to F BAC -language (see Sect. 1.3). In the rules ( ∃) and ( ¬ ∀), z is any object variable or constant, and in the rules ( ∀) and ( ¬ ∃), z is a new variable. Furthermore, we admit specific rules that reflect properties of relational constants that are specific for F BAC .
The rules and the axiomatic sets reflecting the properties of relations presented above have the following forms:
For # ∈ { ∨ , ∧ } and for all object symbols x and y,
The rule corresponding to the implication from left to right of the condition (ReBA5#) has the following form:
(rReBA5#( → )) \(\frac{} {{R}_{\#}(x,y,t)\,\vert \,{R}_{\#}(t,z,u)\,\vert \,\neg {R}_{\#}(y,z,t^{\prime}),\neg {R}_{\#}(x,t^{\prime},u^{\prime})}\)
x, y, z, t, u are any object symbols, t′, u′ are new object variables such that t′≠u′ and {t′, u′} ∩ { x, y, z, t, u} = ∅
The implication from right to left is reflected by the rule of the form:
(rReBA5#( ← )) \(\frac{} {{R}_{\#}(y,z,t^{\prime})\,\vert \,{R}_{\#}(x,t^{\prime},u^{\prime})\,\vert \,\neg {R}_{\#}(x,y,t),\neg {R}_{\#}(t,z,u)}\)
x, y, z, t′, u′ are any object symbols, t, u are new object variables such that t≠u and \(\{t,u\} \cap \{ x,y,z,t^{\prime},u^{\prime}\} = \varnothing \)
Similarly, the rules corresponding to the conditions (ReBA6) and (ReBA7) have the following forms:
(rReBA6( → )) \(\frac{} {{R}_{\vee }(x,y,t)\,\vert \,{R}_{\wedge }(t,z,u)\,\vert \,\neg {R}_{\wedge }(x,z,t^{\prime}),\neg {R}_{\wedge }(y,z,u^{\prime}),\neg {R}_{\vee }(t^{\prime},u^{\prime},u)}\)
x, y, z, t, u are any object symbols, t′, u′ are new object variables such that t′≠u′ and \(\{t^{\prime},u^{\prime}\} \cap \{ x,y,z,t,u\} = \varnothing \)
(rReBA6( ← )) \(\frac{} {{R}_{\wedge }(x,z,t^{\prime})\,\vert \,{R}_{\wedge }(y,z,u^{\prime})\,\vert \,{R}_{\vee }(t^{\prime},u^{\prime},u)\,\vert \,\neg {R}_{\vee }(x,y,t),\neg {R}_{\wedge }(t,z,u)}\)
x, y, z, t′, u′ are any object symbols, t, u are new object variables such that t≠u and \(\{t,u\} \cap \{ x,y,z,t^{\prime},u^{\prime}\} = \varnothing \)
(rReBA7( → )) \(\frac{} {{R}_{\wedge }(x,y,t)\,\vert \,{R}_{\vee }(t,z,u)\,\vert \,\neg {R}_{\vee }(x,z,t^{\prime}),\neg {R}_{\vee }(y,z,u^{\prime}),\neg {R}_{\wedge }(t^{\prime},u^{\prime},u)}\)
x, y, z, t, u are any object symbols, t′, u′ are new object variables such that t′≠u′ and \(\{t^{\prime},u^{\prime}\} \cap \{ x,y,z,t,u\} = \varnothing \)
(rReBA7( ← )) \(\frac{} {{R}_{\vee }(x,z,t^{\prime})\,\vert \,{R}_{\vee }(y,z,u^{\prime})\,\vert \,{R}_{\wedge }(t^{\prime},u^{\prime},u)\,\vert \,\neg {R}_{\wedge }(x,y,t),\neg {R}_{\vee }(t,z,u)}\)
x, y, z, t′, u′ are any object symbols, t, u are new object variables such that t≠u and \(\{t,u\} \cap \{ x,y,z,t^{\prime},u^{\prime}\} = \varnothing \).
The conditions (ReBA8) and (ReBA9) lead to the following axiomatic sets:
The condition (ReBA10) is reflected by the rule of the form:
The rules corresponding to the axioms characterizing the conditions (ReCi) have the following forms:
For all object symbols x and y,
F BAC -dual tableau includes specialized cut rules. As mentioned in Sect. 16.3, in the presence of the ordinary cut rule they could be replaced by the rules with a non-empty premise (see Sect. 25.9).
Let \(\mathcal{K}\) be a class of F BAC -models. The notions of a \(\mathcal{K}\)-set and \(\mathcal{K}\)-correctness of a rule are defined in a similar way as in the logic F (see Sect. 1.3). Recall, that a finite set X of F BAC -formulas is a \(\mathcal{K}\)-set whenever the disjunction of its formulas is \(\mathcal{K}\)-valid.
Theorem 18.3.2 (Correspondence).
Let \(\mathcal{K}\) be a class of F BAC -models. Then for every i ∈{ 0,…,11}, the following conditions are equivalent:
-
1.
(ReCi) is true in all models of \(\mathcal{K}\)
-
2.
The rule (rReCi) is \(\mathcal{K}\) -correct.
Proof.
By way of example, we prove the statement for the condition (ReC10).
Let \(\mathcal{K}\) be a class of F BAC -models satisfying the condition (ReC10). Let X be a finite set of F BAC -formulas. Let z be a variable that does not occur in X and such that z≠x. Assume that X ∪{ x≠1} and X ∪{ z = 0, C(z, x)} are \(\mathcal{K}\)-sets. Then, by the assumption on variable z, for every \(\mathcal{K}\)-model \(\mathcal{M}\) and for every valuation v in \(\mathcal{M}\), either there exists φ ∈ X such that \(\mathcal{M},\sqsubseteq \models \varphi \) or both v(x)≠1 and for every z ∈ U, either z = 0 or C(z, v(x)). Suppose X is not a \(\mathcal{K}\)-set. Then, by the assumption, there exist a \(\mathcal{K}\)-model \(\mathcal{M}\) and a valuation v in \(\mathcal{M}\) such that v(x)≠1 and for every z ∈ U, either z = 0 or C(z, v(x)). Since v(x)≠1, by the condition (ReC8), there exists z ∈ U such that z≠0 and ¬C(z, v(x)), a contradiction. Therefore, the rule (rReC10) is \(\mathcal{K}\)-correct.
Assume the rule (rReC10) is \(\mathcal{K}\)-correct. Let \(X{ \mathrm{df} \atop =} \{x = 1,\exists t(t\neq 0 \wedge C(t,x))\}\) and let z be a variable such that z≠x and z≠t. Then, X ∪{ x≠1} and X ∪{ z = 0, C(z, x)} are \(\mathcal{K}\)-sets. Thus, by the assumption, X is a \(\mathcal{K}\)-set, that is in every \(\mathcal{K}\)-model \(\mathcal{M}\), either x = 1 or there exists t ∈ U such that t≠0 and C(t, x), which means that the condition (ReC10) holds.
The proofs of the remaining cases are similar.
From now on, throughout this section, by an F BAC -model we mean a model (U, R −, R ∨, R ∧, C, 0, 1, m) satisfying all the conditions (ReBA0), (ReBA1), (ReBA2#), …, (ReBA5#), for # ∈ { ∨ , ∧ }, (ReBA6), …, (ReBA10), and all the conditions (ReC0), …, (ReC11). Theorem 18.3.2 implies:
Proposition 18.3.1.
-
1.
The F BAC -rules are F BAC -correct;
-
2.
The F BAC -axiomatic sets are F BAC -sets.
The notions of an F BAC -proof tree, a closed branch of such a tree, a closed F BAC -proof tree, and F BAC -provability are defined as in the logic F (see Sect. 1.3).
A branch b of an F BAC -proof tree is complete whenever it is closed or it satisfies the completion conditions of the dual tableau for the logic F (see Sect. 1.3) and the completion conditions corresponding to the specific rules of the F BAC -dual tableau:
For every # ∈ { ∨ , ∧ },
Cpl(rReBA0) For every object symbol x, there exists an object variable z such that ¬R −(x, z) ∈ b, obtained by an application of the rule (rReBA0);Cpl(rReBA1) For all object symbols x and y, if x = y ∈ b, then for every object symbol z, either R −(z, x) ∈ b or R −(z, y) ∈ b, obtained by an application of the rule (rReBA1);Cpl(rReBA2#) For all object symbols x and y, there exists an object variable z such that ¬R # (x, y, z) ∈ b, obtained by an application of the rule (rReBA2#);Cpl(rReBA3#) For all object symbols x and y, if x = y ∈ b, then for all object symbols z and t, either R # (z, t, x) ∈ b or R # (z, t, y) ∈ b, obtained by an application of the rule (rReBA3#);Cpl(rReBA4#) For all object symbols x, y, and z, if R # (x, y, z) ∈ b, then R # (y, x, z) ∈ b, obtained by an application of the rule (rReBA4#);
Cpl(rReBA5#( → )) For all object symbols x, y, z, t, u, either R # (x, y, t) ∈ b or R # (t, z, u) ∈ b or for some object variables t′ and u′ both ¬R # (y, z, t′) ∈ b and ¬R # (x, t′, u′) ∈ b, obtained by an application of the rule (rReBA5#( → ));Cpl(rReBA5#( ← )) For all object symbols x, y, z, t′, u′, either R # (y, z, t′) ∈ b or R # (x, t′, u′) ∈ b or for some object variables t and u both ¬R # (x, y, t) ∈ b and ¬R # (t, z, u) ∈ b, obtained by an application of the rule (rReBA5#( ← ));Cpl(rReBA6( → )) For all object symbols x, y, z, t, u, either R ∨(x, y, t) ∈ b or R ∧(t, z, u) ∈ b or there are object variables t′, u′ such that ¬R ∧(x, z, t′) ∈ b and ¬R ∧(y, z, u′) ∈ b and ¬R ∨(t′, u′, u), obtained by an application of the rule (rReBA6( → ));
Cpl(rReBA6( ← )) For all object symbols x, y, z, t′, u′, either R ∧(x, z, t′) ∈ b or R ∧(y, z, u′) ∈ b or R ∨(t′, u′, u) or there are object variables t and u such that both ¬R ∨(x, y, t) ∈ b and ¬R ∧(t, z, u) ∈ b, obtained by an application of the rule (rReBA6( ← ));Cpl(rReBA7( → )) For all object symbols x, y, z, t, u, either R ∧(x, y, t) ∈ b or R ∨(t, z, u) ∈ b or there are object variables t′, u′ such that ¬R ∨(x, z, t′) ∈ b and ¬R ∨(y, z, u′) ∈ b and ¬R ∧(t′, u′, u), obtained by an application of the rule (rReBA7( → ));Cpl(rReBA7( ← )) For all object symbols x, y, z, t′, u′, either R ∨(x, z, t′) ∈ b or R ∨(y, z, u′) ∈ b or R ∧(t′, u′, u) or there are object variables t and u such that both ¬R ∧(x, y, t) ∈ b and ¬R ∨(t, z, u) ∈ b, obtained by an application of the rule (rReBA7( ← ));Cpl(rReBA10) For every object symbol x, there exists an object variable y such that ¬R −(x, y) ∈ b and ¬R ∨(x, y, 1) ∈ b, and ¬R ∧(x, y, 0), obtained by an application of the rule (rReBA10);Cpl(rReC0) For all object symbols x and y, either C(x, y) ∈ b or both x = 0 ∈ b and y = 0 ∈ b, obtained by an application of the rule (rReC0);>Cpl(rReC1) For all object symbols x and y, if C(x, x) ∈ b, then x≠0 ∈ b, obtained by an application of the rule (rReC1);Cpl(rReC2) For all object symbols x, y, if C(x, y) ∈ b, then ¬R ∧(x, y, 0) ∈ b, obtained by an application of the rule (rReC2);Cpl(rReC3) For all object symbols x and y, if C(x, y) ∈ b, then C(y, x) ∈ b, obtained by an application of the rule (rReC3);Cpl(rReC4) For all object symbols x and y, if C(x, y) ∈ b, then x = y ∈ b, obtained by an application of the rule (rReC4);Cpl(rReC5) For all object symbols x and y, if C(x, y) ∈ b, then for every object symbol z, either C(x, z) ∈ b or R ∨(z, y, y) ∈ b, obtained by an application of the rule (rReC5);Cpl(rReC6) For all object symbols x, y, and z, if C(x, y) ∈ b and C(x, z) ∈ b, then for every object symbol t, either C(x, t) ∈ b or R ∨(y, z, t) ∈ b, obtained by an application of the rule (rReC6);Cpl(rReC7) For all object symbols x and y, if R ∨(x, y, y) ∈ b, then for some object variable z both ¬C(x, z) ∈ b and C(y, z) ∈ b, obtained by an application of the rule (rReC7);Cpl(rReC8) For all object symbols x and y either C(x, y) ∈ b or there are object variables z and t such that C(x, z) ∈ b and ¬R −(z, t) ∈ b, and C(t, y) ∈ b, obtained by an application of the rule (rReC8);Cpl(rReC9) For all object symbols x and y, if C(x, y) ∈ b, then either x≠0 ∈ b or y≠0 or R ∨(x, y, 1) ∈ b, obtained by an application of the rule (rReC9);Cpl(rReC10) For every object symbol x, either x≠1 ∈ b or for some object variable z, both z = 0 ∈ b and C(z, x) ∈ b, obtained by an application of the rule (rReC10);Cpl(rReC11) For every object symbol x, either x≠0 ∈ b or x≠1 ∈ b or for some object variable z, both ¬C(x, z) ∈ b and ¬R −(x, z) ∈ b, obtained by an application of the rule (rReC11).
The notions of a complete F BAC -proof tree and an open branch of an F BAC -proof tree are defined as in F-logic (see Sect. 1.3). Observe that all the rules considered in this section guarantee that whenever a branch of an F BAC -proof tree contains an atomic F BAC -formula φ and its negation, then the branch can be closed, which enables us to prove the closed branch property.
Let b be an open branch of an F BAC -proof tree. The branch structure \({\mathcal{M}}^{\lfloor }=({\mathcal{U}}^{\lfloor },{\mathcal{R}}_{-}^{\lfloor },{\mathcal{R}}_{\vee }^{\lfloor },{\mathcal{R}}_{\wedge }^{\lfloor },{\mathcal{C}}^{\lfloor },{{\prime}}^{\lfloor },{\infty }^{\lfloor },{\Updownarrow }^{\lfloor })\) is defined as follows:
-
\({U}^{b} ={ \mathbb{O}\mathbb{S}}_{{\mathsf{F}}_{\mathsf{BAC}}}\);
-
0b = m b(0) = 0 and 1b = m b(1) = 1;
-
R b = m b(R) = { (x, y) ∈ (U b)2 : R(x, y) ∉ b}, for R ∈ { R −, C, = };
-
Q b = m b(Q) = { (x, y, z) ∈ (U b)3 : Q(x, y, z) ∉ b}, for Q ∈ { R ∨, R ∧}.
Proposition 18.3.2 (Branch Model Property).
Let b be an open branch of an F BAC -proof tree. Then the branch structure \({\mathcal{M}}^{\lfloor }\,=\,({\mathcal{U}}^{\lfloor },{\mathcal{R}}_{-}^{\lfloor },{\mathcal{R}}_{\vee }^{\lfloor },{\mathcal{R}}_{\wedge }^{\lfloor },{\mathcal{C}}^{\lfloor },{{\prime}}^{\lfloor },{\infty }^{\lfloor },{\Updownarrow }^{\lfloor })\) is an F BAC -model.
Proof.
Let b be an open branch of an F BAC -proof tree. It suffices to show that \({\mathcal{M}}^{\lfloor }\) satisfies the conditions (ReBA0), (ReBA1), (ReBA2#), …, (ReBA5#), for # ∈ { ∨ , ∧ }, (ReBA6), …, (ReBA10), (ReC0), …, (ReC11). By way of example, we show that \({\mathcal{M}}^{\lfloor }\) satisfies the conditions (ReBA2#) and (ReC7).
(ReBA2#) Note that by the completion condition Cpl(rReBA2#), for all x, y ∈ U b there exists z ∈ U b such that ¬R # (x, y, z) ∈ b. Thus, R # (x, y, z) ∉ b. Hence, for all x, y ∈ U b there exists z ∈ U b such that R # b(x, y, z).
(ReC7) Let x, y ∈ U b. Assume that for all z ∈ U b, C b(x, z) implies C b(y, z), that is for all object symbols z, either C(x, z) ∈ b or C(y, z) ∉ b. Suppose \({R}_{\vee }^{b}(x,y,y)\) is not satisfied in \({\mathcal{M}}^{\lfloor }\). Then, R ∨(x, y, y) ∈ b, and by the completion condition Cpl(rReC7), there exists z ∈ U b such that both ¬C(x, z) ∈ b and C(y, z) ∈ b, a contradiction.
The proofs of the remaining conditions are similar. In each case we use the corresponding completion condition.
Since the interpretation of atomic formulas in the branch model is defined in the standard way, i.e., as in the completeness proof of F-dual tableau (see Sect. 1.3), the satisfaction in branch model property holds and the completeness of F BAC -dual tableau can be proved as in the logics F and RL(1, 1′).
Theorem 18.3.3 (Soundness and Completeness of F BAC ).
Let φ be an F BAC -formula. Then the following conditions are equivalent:
-
1.
φ is F BAC -valid;
-
2.
φ is true in all standard F BAC -models;
-
3.
φ is F BAC -provable.
4 Dual Tableau for Region Connection Calculus
The first-order theory of region connection calculus (see [RCC92]), F RCC fun , is obtained from F BA fun by endowing its language with a relational constant C representing a contact relation, relational constants DC, EC, PO, TPP, NTPP, TPP − 1, and NTPP − 1 representing the mereological relations defined in Sect. 18.2, and the relational constant EQ representing equality of regions. The mereological relations provide a partition of the universe of regions, that is they are pairwise disjoint and their union is the universal relation. Such a theory is, in fact, based on the contact relation (see Table 18.1). A relation algebra generated by these relations is investigated in [LM94]. In [DSW01] it is shown that the basic RCC relations cannot be the atoms of any relation algebra.
The models of F RCC fun satisfy the conditions (RCC1), (RCC2), and (RCC3) that coincide with (C3), (C4), and (C6), respectively, and the following:
-
aC1;
-
b≠1 implies: [aC( − b) iff a − NTPPb] and [aO( − b) iff a − Pb];
-
aC(b ∧ c) iff there exists d such that dPb, dPc, and aCd;
-
a ∧ b≠0 iff aOb;
-
syq(C, C) ⊆ 1′,
where syq is the operation of symmetric quotient defined as:
and operations ∖ and ∕ of the right and left residual of the composition of relations, respectively, are defined by the following conditions, for all relations P and R:
By F RCC we mean the theory obtained from F RCC fun by elimination of function symbols. F RCC -structures are F BA -models with binary relations C, DC, EC, PO, TPP, and NTPP that interpret the specific relational constants of the region connection calculus according to their definitions in Table 18.1.
F RCC -models are the F RCC -structures that satisfy the conditions which are function-free representations of the RCC-axioms. (ReRCC1), (ReRCC2), and (ReRCC3) coincide with (ReC3), (ReC4), and (ReC6), respectively.
(ReRCC4) C(x, 1);>(ReRCC5) y≠1 implies:
-
(1)
There exists z such that C(x, z) and R −(y, z) iff ¬NTTP(x, y),
-
(2)
There exists z such that O(x, z) and R −(y, z) iff ¬P(x, y);
(ReRCC6) There is t such that C(x, t) and R ∧(y, z, t) iff there is w such that P(w, y), P(w, z), and C(x, w);
(ReRCC7) There is z such that R ∧(x, y, z) and z≠0 iff O(x, y);
(ReRCC8) If for all zC(x, z) or not C(z, y) and for all w not C(x, w) or C(w, y), then x = y.
The following theorem states the relationship between the theory of region connection calculus and the F RCC -models.
Theorem 18.4.1.
For every F RCCfun -formula φ there exists an F RCC -formula φ′ such that φ is true in all algebras of RCC iff φ′ is true in all F RCC -models.
F RCC -dual tableau is obtained from the F-dual tableau by endowing it with the specific rules and the axiomatic sets reflecting the conditions (ReBA0), (ReBA1), (ReBA2#), …, (ReBA5#), for # ∈ { ∨ , ∧ }, (ReBA6), …, (ReBA10), and the rules (rReRCC1), (rReRCC2), (rReRCC3) which coincide with (rReC3), (rReC4), and (rReC6), respectively. All these rules and axiomatic sets are presented in the previous section. F RCC -dual tableau contains also the rules (#) and ( − #), for every # ∈ Mer, presented in Sect. 18.2 with a minor syntactic transformation which adapts the rules to their first-order presentation. Namely, instead of xRy and x − Ry we write R(x, y) and ¬R(x, y), respectively, and instead of 1′ we write = . Moreover, in the rules which introduce arbitrary variable, now we allow any object symbol, i.e., an object variable or 0 or 1. We also include the axiomatic sets and the specific rules that reflect conditions (ReRCC5), …, (ReRCC8).
Condition (ReRCC4) leads to the following axiomatic set:
The two implications of the first part of (ReRCC5) have the following rules:
The rules for the second part of (ReRCC5) are:
The remaining rules are:
The rules above are specialized cut rules. A discussion of the alternative deterministic forms of specialized cut rules can be found in Sect. 25.9.
Theorem 18.4.2 (Correspondence).
Let \(\mathcal{K}\) be a class of F RCC -structures. Then, the following hold:
-
1.
The condition (ReRCC4) is valid in \(\mathcal{K}\) iff the axiomatic sets (AxReRCC4) are \(\mathcal{K}\) -sets;
-
2.
The condition (ReRCC5) is valid in \(\mathcal{K}\) iff for every i ∈ {1,2}, the rules (riReRCC5( →)) and (riReRCC5( ←)) are \(\mathcal{K}\) -correct;
-
3.
For every \(\mathcal{C}\in \) (ReRCC6), (ReRCC7)}, the condition \(\mathcal{C}\) is valid in \(\mathcal{K}\) iff the rules (r \(\mathcal{C}\) ( →)) and (r \(\mathcal{C}\) ( ←)) are \(\mathcal{K}\) -correct;
-
4.
The condition (ReRCC8) is valid in \(\mathcal{K}\) iff the rule (rReRCC8) is \(\mathcal{K}\) -correct.
Proof.
By way of example, we prove the proposition for the condition (ReRCC8).
Assume (ReRCC8) is true in all \(\mathcal{K}\)-structures. We show that the rule (rReRCC8) is \(\mathcal{K}\)-correct. Let X be a finite set of F RCC -formulas, let x, y be object symbols, and let z and w be variables that do not occur in X and such that z≠w and \(\{z,w\} \cap \{ x,y\}\,=\,\varnothing \). Assume that X ∪{ C(x, z), ¬C(z, y), x = y} and X ∪ ¬C(x, w), C(w, y), x = y} are \(\mathcal{K}\)-sets. Suppose X ∪{ x = y} is not a \(\mathcal{K}\)-set. Then, there exist a \(\mathcal{K}\)-structure \(\mathcal{M}\) and a valuation v in \(\mathcal{M}\) such that v(x)≠v(y) and, due to the assumption on variables z and w, for all z ∈ U, either C(v(x), z) or not C(z, v(y)) and for all w ∈ U either not C(v(x), w) or C(w, v(y)). Thus, by the condition (ReRCC8), v(x) = v(y), a contradiction. Therefore, the rule (rReRCC8) is \(\mathcal{K}\)-correct.
Now, assume that the rule (rReRCC8) is \(\mathcal{K}\)-correct. Let \(X{ \mathrm{df} \atop =} \{\exists z^{\prime}(\neg C(x,z^{\prime}) \wedge C(z^{\prime}y)),\exists w^{\prime}(C(x,w^{\prime}) \wedge \neg C(w^{\prime},y))\}\). Let z, w be object variables such that z≠w and \(\{z,w\} \cap \{ x,y,z^{\prime},w^{\prime}\} = \varnothing \). Then, X ∪{C(x, z), ¬C(z, y), x = y} and X ∪ ¬C(x, w), C(w, y), x = y} are \(\mathcal{K}\)-sets. Thus, by the assumption, X ∪{ x = y} is also \(\mathcal{K}\)-set, which means that for every \(\mathcal{K}\)-structure \(\mathcal{M}\), if x≠y is true in \(\mathcal{M}\), then either there exists z′ ∈ U such that not C(x, z′) and C(z′, y) or there exists w′ ∈ U such that C(x, w′) and not C(w′, y). Hence, the condition (ReRCC8) holds.
The above theorem implies:
Proposition 18.4.1.
-
1.
The F RCC -rules are F RCC -correct;
-
2.
The F RCC -axiomatic sets are F RCC -sets.
The completion conditions determined by the rules specific for F RCC are:
Cpl(r1ReRCC5( → )) For all object symbols x, y, and z, either y≠1 ∈ b or NTTP(x, y) ∈ b or C(x, z) ∈ b or R −(y, z) ∈ b, obtained by an application of the rule (r1ReRCC5( → ));
Cpl(r1ReRCC5( ← )) For all object symbols x and y, either y≠1 ∈ b or ¬NTTP(x, y) ∈ b or for some object variable z both ¬C(x, z) ∈ b and ¬R −(y, z) ∈ b, obtained by an application of the rule (r1ReRCC5( ← ));
Cpl(r2ReRCC5( → )) For all object symbols x, y, and z, either y≠1 ∈ b or P(x, y) ∈ b or O(x, z) ∈ b or R −(y, z) ∈ b, obtained by an application of the rule (r2ReRCC5( → ));Cpl(r2ReRCC5( ← )) For all object symbols x and y, either y≠1 ∈ b or ¬P(x, y) ∈ b or there exists an object variable z such that both ¬O(x, z) ∈ b and ¬R −(y, z) ∈ b, obtained by an application of the rule (r2ReRCC5( ← ));
Cpl(rReRCC6( → )) For all object symbols x, y, z, and t, either C(x, t) ∈ b or R ∧(y, z, t) ∈ b or there exists an object variable w such that ¬P(w, y) ∈ b, ¬P(w, z) ∈ b, and ¬C(x, w) ∈ b, obtained by an application of the rule (rReRCC6( → ));
Cpl(rReRCC6( ← )) For all object symbols x, y, z, and w, either P(w, y) ∈ b or P(w, z) ∈ b or C(x, w) ∈ b, or for some object variable t both ¬C(x, t) ∈ b and ¬R ∧(y, z, t) ∈ b, obtained by an application of the rule (rReRCC6( ← ));
Cpl(rReRCC7( → )) For all object symbols x, y, and z, either ¬O(x, y) ∈ b or R ∧(x, y, z) ∈ b or z≠0, obtained by an application of the rule (rReRCC7( → ));
Cpl(rReRCC7( ← )) For all object symbols x and y, either O(x, y) ∈ b or for some object variable z, both ¬R ∧(x, y, z) ∈ b and z = 0 ∈ b, obtained by an application of the rule (rReRCC7( ← ));
Cpl(rReRCC8) For all object symbols x and y, if x = y ∈ b, then for some object variables z and w, either both C(x, z) ∈ b and ¬C(z, y) ∈ b or both ¬C(x, w) ∈ b and C(w, y) ∈ b, obtained The rules of F RCC -dual tableau guarantee that whenever a branch of an F RCC -proof tree contains an atomic F RCC -formula φ and its negation, then the branch can be closed. Thus, the closed branch property can be proved.
Let b be an open branch of an F RCC -proof tree. The branch structure \({\mathcal{M}}^{\lfloor } = ({\mathcal{U}}^{\lfloor },{\mathcal{R}}_{-}^{\lfloor },{\mathcal{R}}_{\vee }^{\lfloor },{\mathcal{R}}_{\wedge }^{\lfloor },{\mathcal{C}}^{\lfloor },\{{\#}^{\lfloor } : \# \in \mathsf{Mer}\},{{\prime}}^{\lfloor },{\infty }^{\lfloor },{\Updownarrow }^{\lfloor })\) is defined as follows:
-
\({U}^{b} ={ \mathbb{O}\mathbb{S}}_{{\mathsf{F}}_{\mathsf{RCC}}}\);
-
0b = m b(0) = 0 and 1b = m b(1) = 1;
-
R b = m b(R) = { (x, y) ∈ (U b)2 : R(x, y) ∉ b}, for R ∈ { R −, C, = };
-
Q b = m b(Q) = { (x, y, z) ∈ (U b)3 : Q(x, y, z) ∉ b}, for Q ∈ { R ∨, R ∧};
-
For every # ∈ Mer, # b is defined according to Table 18.1; for example, \({P}^{b}{ \mathrm{df} \atop =} -({C}^{b}\,;\,-{C}^{b})\);
-
m b(#) = # b.
Proposition 18.4.2 (Branch Model Property).
Let b be an open branch of an F RCC -proof tree. Then, the branch structure \({\mathcal{M}}^{\lfloor }\) is an F RCC -model.
Proof.
Let b be an open branch of an F RCC -proof tree. It suffices to show that \({\mathcal{M}}^{\lfloor }\) satisfies the conditions (ReRCC1), …, (ReRCC8). By way of example, we show that \({\mathcal{M}}^{\lfloor }\) satisfies the condition (ReRCC6).
( → ) By the completion condition Cpl(rReRCC6( → )), for all x, y, z, t ∈ U b, either C(x, t) ∈ b or R ∧(y, z, t) ∈ b or there exists an object variable w such that ¬P(w, y) ∈ b and ¬P(w, z) ∈ b, and ¬C(x, w) ∈ b. Thus, by the definition of \({\mathcal{M}}^{\lfloor }\) and the completion condition Cpl( ¬P) (see the proof of Proposition 18.2.5), either not C b(x, t) or not \({R}_{\wedge }^{b}(y,z,t)\) or there exists w ∈ U b such that P b(w, y) and P b(w, z), and C b(x, w). Hence, if C b(x, t) and \({R}_{\wedge }^{b}(y,z,t)\), then there exists w ∈ U b such that P b(w, y) and P b(w, z), and C b(x, w).
( ← ) By the completion condition Cpl(rReRCC6( ← )), for all x, y, z, w ∈ U b, either P(w, y) ∈ b or P(w, z) ∈ b or C(x, w) ∈ b or there exists an object variable t such that both ¬C(x, t) ∈ b and ¬R ∧(y, z, t) ∈ b. By the definition of \({\mathcal{M}}^{\lfloor }\) and the completion condition Cpl(P) (see Proposition 18.2.5), if P b(w, y), P b(w, z), and C b(x, w) hold, then there exists t ∈ U b such that C b(x, t) and \({R}_{\wedge }^{b}(y,z,t)\). Therefore, \({\mathcal{M}}^{\lfloor }\) satisfies the condition (ReRCC6).
The proofs of the remaining conditions are similar.
The satisfaction in branch model property for F RCC follows from Proposition 18.2.5. In this way, we get:
Theorem 18.4.3 (Soundness and Completeness of F RCC ).
Let φ be an F RCC -formula. Then, the following conditions are equivalent:
-
1.
φ is F RCC -valid;
-
2.
φ is true in all standard F RCC -models;
-
3.
φ is F RCC -provable.
Example.
Consider the following property holding in RCC:
This property is represented by the following F RCC -formula:
Figure 18.4 presents an F RCC -proof of φ which shows that the property in question holds in RCC.
5 Dual Tableaux for Spatial Theories of Proximity Relation
A proximity relation is a binary relation δ on a Boolean algebra satisfying the following axioms:
An F RCC -proof of ‘aOb implies 0 ≩ (a ∧ b)’
(δ1) aδb implies a, b≠0;(δ2) cδ(a ∨ b) iff cδa or cδb;(δ3) (a ∨ b)δc iff aδc or bδc.
Development of a dual tableau for the theory of proximity follows the lines of Sect. 18.3. We consider the first-order theory F BAδ of binary relations δ and R −, and ternary relations R ∨ and R ∧.
F BAδ-models are structures \(\mathcal{M} = (\mathcal{U},{\mathcal{R}}_{-},{\mathcal{R}}_{\vee },{\mathcal{R}}_{\wedge },\delta ,{\prime},\infty ,\Updownarrow )\) satisfying conditions (ReBA0), (ReBA1), (ReBA2#), …, (ReBA5#), for # ∈ { ∨ , ∧ }, (ReBA6), …, (ReBA10) presented in Sect. 18.3, and for all x, y, t ∈ U:
(Reδ1) δ(x, y) implies x≠0 and y≠0;
(Reδ2) There exists z such that R ∨(x, y, z) and δ(t, z) iff δ(t, x) or δ(t, y);
(Reδ3) There exists z such that R ∨(x, y, z) and δ(z, t) iff δ(x, t) or δ(y, t).
F BAδ-dual tableau is the F-dual tableau endowed with the specific rules and axiomatic sets corresponding to the conditions (ReBA0), (ReBA1), (ReBA2#), …, (ReBA5#), for # ∈ { ∨ , ∧ }, (ReBA6), …, (ReBA10) presented in Sect. 18.3, and the specific rules corresponding to the conditions (Reδ1), (Reδ2), (Reδ3). The latter rules have the following forms:
For all object symbols x, y, and t,
Alternative forms of rules (rReδ1), (rReδ2( ← )), and (rReδ3( ← )) are discussed in Sect. 25.9.
The following can be proved:
Proposition 18.5.1.
-
1.
The F BAδ-rules are F BAδ-correct;
-
2.
The F BAδ-axiomatic sets are F BAδ -sets.
The completion conditions determined by the rules (rReδ1), (rReδ2( → )), (rReδ2( ← )), (rReδ3( → )), and (rReδ3( ← )) are:
For all object symbols x, y, and t,
Cpl(rReδ1) Either δ(x, y) ∈ b or both x = 0 ∈ b and y = 0 ∈ b, obtained by an application of the rule (rReδ1);
Cpl(rReδ2( → )) If δ(t, x) ∈ b and δ(t, y) ∈ b, then for every object symbol z, either R ∨(x, y, z) ∈ b or δ(t, z) ∈ b, obtained by an application of the rule (rReδ2( → ));
Cpl(rReδ2( ← )) Either both δ(t, x) ∈ b and δ(t, y) ∈ b or for some object variable z both ¬R ∨(x, y, z) ∈ b and ¬δ(t, z) ∈ b, obtained by an application of the rule (rReδ2( ← ));
Cpl(rReδ3( → )) If δ(x, t) ∈ b and δ(y, t) ∈ b, then for every object symbol z, either R ∨(x, y, z) ∈ b or δ(z, t) ∈ b, obtained by an application of the rule (rReδ3( → ));
Cpl(rReδ3( ← )) Either both δ(x, t) ∈ b and δ(y, t) ∈ b or for some object variable z both ¬R ∨(x, y, z) ∈ b and ¬δ(z, t) ∈ b, obtained by an application of the rule (rReδ3( ← )).
The rules of F BAδ-dual tableau guarantee that whenever a branch of an F BAδ-proof tree contains an atomic F BAδ-formula φ and its negation, then the branch can be closed. Thus, the closed branch property can be proved.
The branch structure is defined as in the completeness proof of F BAC -dual tableau (see p. 55), where C is replaced by δ.
Proposition 18.5.2 (Branch Model Property).
Let b be an open branch of an F BAδ-proof tree. Then, the branch structure \({\mathcal{M}}^{\lfloor }\,=\,({\mathcal{U}}^{\lfloor },{\mathcal{R}}_{-}^{\lfloor },{\mathcal{R}}_{\vee }^{\lfloor },{\mathcal{R}}_{\wedge }^{\lfloor },{\delta }^{\lfloor },{{\prime}}^{\lfloor },{\infty }^{\lfloor },{\Updownarrow }^{\lfloor })\) is an F BAδ-model.
Proof.
It suffices to show that \({\mathcal{M}}^{\lfloor }\) satisfies the conditions (Reδ1), (Reδ2), (Reδ3). By way of example, we show that \({\mathcal{M}}^{\lfloor }\) satisfies the condition (Reδ2).
Assume that there exists z ∈ U b such that \({R}_{\vee }^{b}(x,y,z)\) and δb(t, z), that is R ∨(x, y, z) ∉ b and δ(t, z) ∉ b. Suppose δb(t, x) and δb(t, y) do not hold in \({\mathcal{M}}^{\lfloor }\). Then, δ(t, x) ∈ b and δ(t, y) ∈ b. By the completion condition Cpl(rReδ2( → )), for every z ∈ U b, either R ∨(x, y, z) ∈ b or δ(t, z) ∈ b, a contradiction.
On the other hand, by the completion condition Cpl(rReδ2( ← )), either δ(t, x) ∈ b or δ(t, y) ∈ b or for some z ∈ U b both ¬R ∨(x, y, z) ∈ b and ¬δ(t, z) ∈ b. Thus, if δb(t, x) and δb(t, y), then there exists z ∈ U b such that \({R}_{\vee }^{b}(x,y,z)\) and δb(t, z) ∈ b. Therefore, the condition (Reδ2) is true in \({\mathcal{M}}^{\lfloor }\).
Since the interpretation of atomic formulas in the branch model is defined in the standard way, the satisfaction in branch model property can be proved as for F BAC -dual tableau. Thus, we obtain:
Theorem 18.5.1 (Soundness and Completeness of F BAδ).
For every F BAδ-formula φ, the following conditions are equivalent:
-
1.
φ is F BAδ-valid;
-
2.
φ is true in all standard F BAδ-models;
-
3.
φ is F BAδ-provable.
Various types of proximity relations, defined by adding specific axioms to the basic axioms (δ1), (δ2), and (δ3), are considered in the literature. Some of these axioms are among the following:
-
aδb implies a = b (separated proximity);
-
If not aδb, then there exists c such that not aδc and not ( − c)δb (Efremovic proximity);
-
δ is symmetric;
-
a ∧ b≠0 implies aδb.
In order to reason about a proximity relation δ satisfying additional conditions (δ4), …, (δ7), we develop logics F BA(δi), i ∈ { 4, …, 7}, based on the logic F BAδ. F BA(δi)-models are F BAδ-models that satisfy the condition (Reδi), for all x, y ∈ U:
-
δ(x, y) implies x = y;
-
If not δ(x, y), then there are z, t ∈ U such that not δ(x, z) and R −(z, t) and not δ(t, y);
-
δ(x, y) implies δ(y, x);
-
If there exists z ∈ U such that R ∧(x, y, z) and z≠0, then δ(x, y).
A dual tableau for logic F BA(δi) is F BAδ-dual tableau endowed with the specific rule corresponding to the condition (Reδi), for i ∈ { 4, …, 7}. The rules have the following forms:
For all object symbols x and y,
Theorem 18.5.2 (Correspondence).
Let \(\mathcal{K}\) be a class of F BAδ-models. Then for every i ∈{ 4,…,7}, the following conditions are equivalent:
-
1.
The condition (Reδi) is true in all \(\mathcal{K}\) -models;
-
2.
The rule (rReδi) is \(\mathcal{K}\) -correct.
Proof.
By way of example, we prove the theorem for (Reδ5).
Assume that the condition (Reδ5) is true in all \(\mathcal{K}\)-models. Let X be a finite set of F BAδ-formulas. Let x, y be object symbols and let z, t be object variables that do not occur in X and such that z≠t, \(\{z,t\} \cap \{ x,y\} = \varnothing \). Assume X ∪{ δ(x, z), ¬R −(z, t), δ(t, y), δ(x, y)} is a \(\mathcal{K}\)-set and suppose X ∪{ δ(x, y)}is not a \(\mathcal{K}\)-set. Then, there exist a \(\mathcal{K}\)-model \(\mathcal{M}\) and a valuation v in \(\mathcal{M}\) such that \(\mathcal{M},\sqsubseteq \nvDash \delta (\S ,\dag )\). By the assumption on variables z and t, for all z, t ∈ U, either δ(v(x), z) or not R −(z, t) or δ(t, v(y)). Then, by the condition (Reδ5), \(\mathcal{M},\sqsubseteq \models \delta (\S ,\dag )\), a contradiction. Therefore, the rule (rReδ5) is \(\mathcal{K}\)-correct.
Assume that the rule (rReδ5) is \(\mathcal{K}\)-correct. Let \(X{ \mathrm{df} \atop =} \{\exists z^{\prime}\exists t^{\prime}(\neg \delta (x,z^{\prime}) \wedge {R}_{-}(z^{\prime},t^{\prime}) \wedge \neg \delta (t^{\prime},y))\}\). Let z, t be object variables such that z≠t and \(\{z,t\} \cap \{ x,y,z^{\prime},t^{\prime}\} = \varnothing \). Then, X ∪{ δ(x, z), ¬R −(z, t), δ(t, y), δ(x, y)} is a \(\mathcal{K}\)-set, so by the assumption X ∪{ δ(x, y)} is also a \(\mathcal{K}\)-set. Therefore, the following is true in every \(\mathcal{K}\)-model: if not δ(x, y), then there exist z′ and t′ such that not δ(x, z′) and R −(z′, t′) and not δ(t′, y). Hence, the condition (Reδ5) is true in all \(\mathcal{K}\)-models.
The above theorem implies:
Proposition 18.5.3.
Let i ∈{ 4,…,7}. Then:
-
1.
The F BA(δi)-rules are F BA(δi) -correct;
-
2.
The F BA(δi)-axiomatic sets are F BA(δi) -sets.
The completion conditions determined by the rules (rReδ4), …, (rReδ7) are:
For all object symbols x and y,
Cpl(rReδ4) If x = y ∈ b, then δ(x, y) ∈ b, obtained by an application of the rule (rReδ4);
Cpl(rReδ5) If δ(x, y) ∈ b, then there are object variables z and t such that δ(x, z) ∈ b and ¬R −(z, t) ∈ b, and δ(t, y) ∈ b, obtained by an application of the rule (rReδ5);
Cpl(rReδ6) If δ(x, y) ∈ b, then δ(y, x) ∈ b, obtained by an application of the rule (rReδ6);
Cpl(rReδ7) If δ(x, y) ∈ b, then for every object symbol z, either R ∧(x, y, z) ∈ b or z≠0 ∈ b, obtained by an application of the rule (rReδ1).
The closed branch property, the branch model property and the satisfaction in branch model property can be proved as for F BAδ-dual tableau. Hence, we get:
Theorem 18.5.3 (Soundness and Completeness of F BA(δi)).
Let i ∈{ 4,…,7}. For every F BAδ-formula φ, the following conditions are equivalent:
-
1.
φ is F BA(δi)-valid;
-
2.
φ is true in all standard F BA(δi)-models;
-
3.
φ is F BA(δi)-provable.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2011 Springer Science+Business Media B.V.
About this chapter
Cite this chapter
Orłowska, E., Golińska-Pilarek, J. (2011). Dual Tableaux for Spatial Reasoning. In: Dual Tableaux: Foundations, Methodology, Case Studies. Trends in Logic, vol 33. Springer, Dordrecht. https://doi.org/10.1007/978-94-007-0005-5_18
Download citation
DOI: https://doi.org/10.1007/978-94-007-0005-5_18
Published:
Publisher Name: Springer, Dordrecht
Print ISBN: 978-94-007-0004-8
Online ISBN: 978-94-007-0005-5
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)