Region Connection Calculus

In this exercise, we take a look at modelling qualitative spatial knowledge. Qualitative spatial knowledge is knowledge about the relative position of regions of space when we do not necessarily know the exact extend and location of each region. For instance, one may know that a river is flowing through a forest, but not know the exact route of the river and the extent of the forest. In domains like geography, geology, oil extraction, construction engineering, certain legal situations, it is important to know whether some geospatial entity is situated within, or overlaps, another geospatial entity.

Overview of the Region Connection Calculus

Region Connection Calculus (RCC) corresponds to a family of logics for qualitative spatial reasoning. There are variants like RCC-5, RCC-8, RCC-23 and others, but we will study the simplest one, RCC-5.

RCC-5 states that any two regions of space (say r₁ and r₂) are spatially related in exactly one of the following ways:

r₁ and r₂ cover the exact same region of space;
r₁ is strictly contained in r₂;
r₁ strictly contains r₂;
r₁ and r₂ partially overlap;
r₁ and r₂ are completely disconnected.

If we only know parts of the pairwise relations among a set of spatial entities, we can deduce some of the missing ones. For instance, if r₁ strictly contains r₂ and r₂ strictly contains r₃, we know that r₁ strictly contains r₃. We are going to formalise this kind of reasoning, following the same presentation of the RCC-5 logic as the other logics seen in class.

The logic L_RCC-5

Syntax

Let us consider an infinite set R whose elements will be called region names. The set of symbols of L_RCC-5 is R ∪ {EQ, PP, PPi, PO, DR}. The set {EQ, PP, PPi, PO, DR} is called the set of qualitative spatial relations and is denoted as Rel.

Given region names r₁ and r₂ in R, and a qualitative spatial relation rel, a formula in L_RCC-5 is:

r₁ rel r₂

There is no other kind of formula.

Semantics of RCC-5

An interpretation in L_RCC-5 is a pair I = (Δ^I, (·)^I) such that:

Δ^I is an arbitrary non-empty set called the spatial universe of the interpretation;
(·)^I : R ⟶ 2^{Δ^I} is a function that assigns a subset of the spatial universe to each region name (that is, for each r ∈ R, (r)^I ⊆ Δ^I). This is called the interpretation function.

Given an interpretation I = (Δ^I, (·)^I), the satisfaction relation in L_RCC-5 is defined as follows, for any regions r₁ and r₂:

I ⊨ r₁ EQ r₂ iff (r₁)^I = (r₂)^I;
I ⊨ r₁ PP r₂ iff (r₁)^I ⊆ (r₂)^I;
I ⊨ r₁ PPi r₂ iff (r₂)^I ⊆ (r₁)^I;
I ⊨ r₁ PO r₂ iff there exist x, y, z such that x ∈ (r₁)^I \ (r₂)^I, y ∈ (r₂)^I \ (r₁)^I, and z ∈ (r₁)^I ⋂ (r₂)^I;
I ⊨ r₁ DR r₂ iff (r₁)^I ⋂ (r₂)^I = ∅.

Note: There is a little mistake in this definition, but it does not affect the questions at all. In the real RCC-5 semantics, PP and PPi have to be interpreted as strict subset/superset. The character should have been ⊊ or ⊂.

If S is a set of formulas and I an interpretation in L_RCC-5, we write I ⊨ S iff I ⊨ f for all f ∈ S. In this case, we say that I is a model of S.

Questions on L_RCC-5

Question 1: What is the formal definition of entailment in L_RCC-5, i.e., when a formula f logically follows from a set of formulas S?
Answer 1: The formal definition of entailment is the same for all logics defined with a notion of interpretation and satisfaction: A set S of formulas L_RCC-5-entails a formula f iff all L_RCC-5-models of S L_RCC-5-satisfy f.
Question 2: What is the definition of consistency in L_RCC-5?
Answer 2: The formal definition of consistency is the same for all logics defined with a notion of interpretation and satisfaction: A set S of formulas is L_RCC-5-consistent iff there exists a L_RCC-5-model of S.
Question 3: Provide an example of a tautology in L_RCC-5.
Answer 3: For any region name r, r EQ r is a tautology.

What follows formalises knowledge about French administrative and geographic areas:

Europe DR SouthAmerica (Europe and South America are disconnected);
France PP Europe (France is in Europe);
Dpt75 EQ Paris (the city of Paris covers the same area as département 75);
IDF PPi Paris (Île de France is the region that contains the city of Paris);
IDF PP France (Île de France is a part of France);
FrenchGuiana PP France (French Guiana is a part of France);
FrenchGuiana PP SouthAmerica (French Guiana is in South America).

Question 4: Can you prove that this theory entails FrenchGuiana PP Paris? If you can, provide a formal proof.
Answer 4: To prove that this is the case, we will first prove that in any model of this theory, FrenchGuiana has to be interpreted as the empty set. Let I be an interpretation that satisfies all the formulas above. I ⊨ FrenchGuiana PP France implies that (FrenchGuiana)^I ⊆ (France)^I, I ⊨ France PP Europe implies that (France)^I ⊆ (Europe)^I, I ⊨ FrenchGuiana PP SouthAmerica implies that (FrenchGuiana)^I ⊆ (SouthAmerica)^I. So every element of (FrenchGuiana)^I is in both (Europe)^I and (SouthAmerica)^I. But I ⊨ Europe DR SouthAmerica implies that (Europe)^I and (SouthAmerica)^I are disjoint. So (FrenchGuiana)^I. It is clear that FrenchGuiana must therefore be contained in every other regions.
Question 5: Can you prove that this theory entails France PP SouthAmerica? If you can, provide a formal proof.
Answer 5: This cannot be proved because it does not follow from the given formulas. To show this, it suffices to find a model of the formulas that does not satisfy this one. Consider the spatial domain {1, 2, 3, 4} and an interpretation function that maps FrenchGuiana, Dpt75 and Paris to the empty set; that maps IDF to {1}, France to {1, 2}, Europe to {1, 2, 3} and SouthAmerica to {4}. It is easy to see that this is a model of the theory, but does not satisfy France PP SouthAmerica.
Question 6: If we add FrenchGuiana PO AmazonianForest, how does it affect Questions 4 and 5? A short answer shuld suffice.
Answer 6: If we add this formula, the theory becomes inconsistent. We have seen that any model must interpret FrenchGuiana as the empty set. But if a model I also satisfies FrenchGuiana PO AmazonianForest, then there must exist an element in (FrenchGuiana)^I. So, it woud still be the case that the theory entails FrenchGuiana PP Paris because an inconsistent theory entails everything, but it would also be the case that it entails France PP SouthAmerica.

Our formalisation of spatial relations is very simplistic and unnatural. It allows region names to be interpreted in a strange way. For instance, the spatial universe could be the set of real numbers, and a region name could be interpreted as the set of rational numbers. A region could have arbitrary topological shape, such as a Sierpiński's carpet.

For this reason, spatial universes are often restricted to topological spaces of dimension n (usually, n is 2 or 3), and region names are interpreted as non-empty closed sets.

Question 7: Assuming we make the restrictions explained immediately above, what can we say about Questions 4 and 5 (not including the formula given in Question 6)? Give a short answer.
Answer 7: The reasoning in Question 4 would still hold, so it is still the case that the interpretation of FrenchGuiana must belong to 2 disjoint sets. If the semantics constrains all regions to be non-empty, then this must be inconsistent. So every formulas are entailed.

Alternative semantics for L_RCC-5

In the previous section, named regions are interpreted as exactly the area they cover. Consequently, two region names that cover the same spatial extent identify the same thing. Thus, it would not be possible to extend the logic to describe differently the city of Paris and département 75, which have the same extent, but a different administration. Here, we keep the same syntax but revise the semantics.

An alt-interpretation in L_RCC-5 is a quadruple I^a = (U, Reg, (·)^{I^a}, ext) such that:

U is an arbitrary non-empty set called the universe of interpretation;
Reg ⊆ U is an arbitrary subset of the universe (the regions of the universe);
(·)^{I^a} : R ⟶ Reg is a function that assigns an element of the universe to each region name. This is called the alt-interpretation function.
ext : Reg ⟶ 2^U is a function that assigns a subset of the universe to each region of the universe (that is, for each r ∈ Reg, ext(r) ⊆ U). This is called the spatial extension function.

Note: There was a typo in the previous definition. The variable Reg in the 4-tuple was replaced by Space. I changed it in this version.

Note: With this semantics, the universe can comprise things that are not regions, and different regions can have the same spatial extent.

Given an alt-interpretation I^a = (U, Space, (·)^{I^a}, ext), the alt-satisfaction relation in L_RCC-5 is defined as follows, for any regions r₁ and r₂:

I^a ⊨^a r₁ EQ r₂ iff ext((r₁)^{I^a}) = ext((r₂)^{I^a});
I^a ⊨^a r₁ PP r₂ iff ext((r₁)^{I^a}) ⊆ ext((r₂)^{I^a});
I^a ⊨^a r₁ PPi r₂ iff ext((r₂)^{I^a}) ⊆ ext((r₁)^{I^a});
I^a ⊨^a r₁ PO r₂ iff there exist x, y, z such that x ∈ ext((r₁)^{I^a}) \ ext((r₂)^{I^a}), y ∈ ext((r₂)^{I^a}) \ ext((r₁)^{I^a}), and z ∈ ext((r₁)^{I^a}) ⋂ ext((r₂)^{I^a});
I^a ⊨^a r₁ DR r₂ iff ext((r₁)^{I^a}) ⋂ ext((r₂)^{I^a}) = ∅.

If S is a set of formulas and I^a an alt-interpretation in L_RCC-5, we write I^a ⊨^a S iff I^a ⊨ f for all f ∈ S. In this case, we say that I is an alt-model of S.

Questions on alt-semantics

Question 8

Provide the definition of alt-entailment for the alt-semantics.

Answer 8

Cf. Answer 1.

Question 9

Prove that alt-entailment in alt-semantics is equivalent to entailment in L_RCC-5, that is: a set of formulas S alt-entails a L_RCC-5 formula f iff S entails (in the previous semantics) f.

Note: This question was difficult and should have been flagged as such.

Answer 9

Consider a set S of formulas and a formula f.

First, let us assume that S entails f and prove that S alt-entails f. Let us consider an alt-model I^a = (U, Reg, (·)^{I^a}, ext) of S, and we will show that it must alt-satisfy f. From I^a, we build the interpretation I = (U,(·)^I) such that for all r ∈ R, (r)^I = ext((r)^{I^a}). Let us show that I ⊨ r₁ rel r₂ iff I^a ⊨^a r₁ rel r₂ by considering each possible relation rel:
- (case rel = EQ:) I ⊨ r₁ EQ r₂ iff (r₁)^I = (r₂)^I (from the definition of the satisfaction relation) iff ext((r₁)^{I^a}) = ext((r₂)^{I^a}) (from the definition of (·)^I in this proof) iff I^a ⊨^a r₁ EQ r₂ (from the definition of the alt-satisfaction relation);
- (case rel = PP:) I ⊨ r₁ PP r₂ iff (r₁)^I ⊆ (r₂)^I (from the definition of the satisfaction relation) iff ext((r₁)^{I^a}) ⊆ ext((r₂)^{I^a}) (from the definition of (·)^I in this proof) iff I^a ⊨^a r₁ PP r₂ (from the definition of the alt-satisfaction relation);
- (case rel = PPi:) I ⊨ r₁ PPi r₂ iff (r₂)^I ⊆ (r₁)^I (from the definition of the satisfaction relation) iff ext((r₂)^{I^a}) ⊆ ext((r₁)^{I^a}) (from the definition of (·)^I in this proof) iff I^a ⊨^a r₁ PPi r₂ (from the definition of the alt-satisfaction relation);
- (case rel = PO:) I ⊨ r₁ PO r₂ iff there exist x, y, z such that x ∈ (r₁)^I \ (r₂)^I, y ∈ (r₂)^I \ (r₁)^I, and z ∈ (r₁)^I ⋂ (r₂)^I (from the definition of the satisfaction relation) iff there exist x, y, z such that x ∈ ext((r₁)^{I^a}) \ ext((r₂)^{I^a}), y ∈ ext((r₂)^{I^a}) \ ext((r₁)^{I^a}), and z ∈ ext((r₁)^{I^a}) ⋂ ext((r₂)^{I^a}) (from the definition of (·)^I in this proof) iff I^a ⊨^a r₁ PO r₂ (from the definition of the alt-satisfaction relation);
- (case rel = DR:) I ⊨ r₁ DR r₂ iff (r₁)^I ⋂ (r₂)^I = ∅ (from the definition of the satisfaction relation) iff ext((r₁)^{I^a}) ⋂ ext((r₂)^{I^a}) = ∅ (from the definition of (·)^I in this proof) iff I^a ⊨^a r₁ DR r₂ (from the definition of the alt-satisfaction relation).
From this, it follows that if I^a is an alt-model of S, then I is a model of S. But by hypothesis, S entails f, so I must also satisfy f. From what precedes, it follows that I^a alt-satisfies f.
Second, let us assume that S alt-entails f and prove that S entails f. Let us consider a model I = (Δ^I, (·)^I) of S, and we will show that it must satisfy f. From I, we build the alt-interpretation I^a = (Δ^I ∪ R, R, id_R, (·)^I) where id_R is the identity function over R and we use the interpretation function of I as the extension function of I^a. Let us show that I ⊨ r₁ rel r₂ iff I^a ⊨^a r₁ rel r₂ by considering each possible relation rel:
- (case rel = EQ:) I ⊨ r₁ EQ r₂ iff (r₁)^I = (r₂)^I (from the definition of the satisfaction relation) iff (id_R(r₁))^I = (id_R(r₂))^I (by definition of identity) iff I^a ⊨^a r₁ EQ r₂ (from the definition of the alt-satisfaction relation);
- All the other cases are analogous and use the same steps.
From this, it follows that if I is a model of S, then I^a is an alt-model of S. But by hypothesis, S alt-entails f, so I^a must also alt-satisfy f. From what precedes, it follows that I satisfies f.

From Item 1 and 2 above, the equivalence follows.

Description Logic reasoning

Lars wants to model some common sense knowledge about people and things in description logic, in order to classify them automatically, based on facts he adds to a knowledge base.

Among other things, he considers that parents whose children are only girls are happy parents. He models this as follows:

∀hasChild.Girl ⊑ HappyParent

He also does not want to misclassify objects as people, so he adds axioms that model knowledge like “tables do not have children” that he models like this:

Table ⊑ ¬(∃hasChild.⊤)

Lars is about to encode these axioms (and many others) in a file to feed a description logic reasoner. Before undertaking this laborious work, he asks you, as a knowledge engineer, what you think about his model.

Questions

Lars' model entails that Table ⊑ HappyParent and that is probably not what Lars wants.

Question 10 (hard version)

If you want, you can prove this entailment directly using the definitions of interpretation and satisfaction.

Answer 10

To prove this, we must consider a model of Lars' ontology and show that it satisfies the formula. A model I = (Δ^I, (·)^I) of lars' ontology must satisfy ∀hasChild.Girl ⊑ HappyParent and Table ⊑ ¬(∃hasChild.⊤). I satisfies Table ⊑ happyParent iff (Table)^I ⊆ (HappyParent)^I. Consider an element x of (Table)^I. Since I satisfies Table ⊑ ¬(∃hasChild.⊤), we know that x ∈ (¬(∃hasChild.⊤))^I, which means that x ∈ Δ^I \ (∃hasChild.⊤)^I. This means that there is no y such that (x, y) ∈ (hasChild)^I. As from something false, everything follows, we can conclude that for all y such that (x, y) ∈ (hasChild)^I, y ∈ (Girl)^I. By definition of the ∀ construct, this means that x ∈ (∀hasChild.Girl)^I. Further, I being a model of Lars' ontology implies that I satisfies ∀hasChild.Girl ⊑ HappyParent, and therefore x ∈ (HappyParent)^I. Consequently, for any model I of Lars' ontology, all x in (Table)^I are also in (HappyParent)^I, therefore I satisfies Table ⊑ HappyParent.

Question 10 (guided steps using tableau algorithm)

Follow these steps to construct a proof of the entailment, using the tableau algorithm seen in class:

We proceed by contradiction. We assume that there exists an individual x that belongs to class Table but not to HappyParent, that is (Table⊓¬HappyParent)(x).
The axioms provided by Lars are equivalent to:
⊤ ⊑ C₁

⊤ ⊑ C₂
where C₁ and C₂ are concepts that you have to find.
We must therefore show that the assertion (Table⊓¬HappyParent⊓C₁⊓C₂)(x) cannot be satisfied (replacing C₁ and C₂ by the appropriate complex concepts).
Put the concept Table⊓¬HappyParent⊓C₁⊓C₂ into Negative Normal Form (that is, pushing the negation closest to the concept names).
On the resulting concept, apply the tableau rules seen in class to show that all branches lead to a contradiction. Note: to save time, you can replace Table with Ta, HappyParent with HP, hasChild with hC and Girl with G. ⬛

Answer 10'

We follow the proposed steps:

Let x be an individual name.
The first axiom is equivalent to ⊤ ⊑ HappyParent⊔¬(∀hasChild.Girl) and the second to ⊤ ⊑ ¬(∃hasChild.⊤)⊔¬Table.
The assertion that has to be refuted is therefore (Table⊓¬HappyParent⊓(HappyParent⊔¬(∀hasChild.Girl))⊓(¬(∃hasChild.⊤)⊔¬Table))(x).
The concept in NNF is Table⊓¬HappyParent⊓(HappyParent⊔∃hasChild.¬Girl)⊓(∀hasChild.⊥⊔¬Table).
Let us apply the tableau rules:
- We start by labelling the individual x with the concept Table⊓¬HappyParent⊓(HappyParent⊔∃hasChild.¬Girl)⊓(∀hasChild.⊥⊔¬Table).
- By applying the ⟶_⊓ rule, x is labelled with Table, ¬HappyParent, (HappyParent⊔∃hasChild.¬Girl), and (∀hasChild.⊥⊔¬Table).
- Applying the ⟶_⊔ rule on the first disjunction, we split the tableau in 2 parts, one where x is labelled with HappyParent, the other with ∃hasChild.¬Girl.
  - In the first branch, x is labelled with both HappyParent and ¬HappyParent, so the branch is closed.
  - In the second branch, we can apply again the ⟶_⊔ rule on the second disjunction. This leads to 2 branches, one of which labels x with both Table and ¬Table, so that branch is closed.
  - Only one branch remains where x is labelled with Table, ¬HappyParent, ∃hasChild.¬Girl, and ∀hasChild.⊥.
  - We can apply the ⟶_∃ rule and create a new individual y connected to x by an arc labelled with hasChild, and y is itself labelled with ¬Girl.
  - Now that there is an arc labelled hasChild starting from x, we can apply the ⟶_∀ rule on ∀hasChild.⊥. The rule adds ⊥ to the labels of y, and therefore the branch closes.
  - Since all branches are closed, we established the unsatisfiability of the assertion with respect to our ontology.

Knowledge representation and reasoning: Written examination