Logic Engineering (4)

Bijan Parsia

Limitations

• Require empty ABox/Tbox 
• I.e., no data or schema
• Sat(C) returns true when 
• \(C \equiv D \sqcap E\)
  \(D \equiv F\)
  \(E \equiv \neg F\)
• Sat(C) returns true when
•  \(a:(D \sqcap \neg D)\)
• Thus, our tableau is not a decision procedure for (definitorial) ALC
• It is incomplete
• Also (at the moment)
• Only concept sat
• No subsumption entailment
• No instantiation entailment

Restricted TBox

• Remember our restrictions
1. Only definitions (i.e., A \equiv C, where A is atomic)
2. Only one definition per (atomic) class per TBox
3. No directly or indirectly cyclic definitions, e.g, no \[A \equiv \exists.P(C\sqcap D)\]\[D \equiv C \sqcap \neg A\]
• Such TBoxs are unfoldable
• I.e., we can treat definitions as macros
• recursively replace terms with their definitions
• Now, concept Sat with TBoxes can be reduced to concept Sat without

Eager Unfolding

• Unfold as part of normalization
• Simple
• No need to change tableau
• Correct
• Cons
• The unfolded TBox can be HUGE
• TBox: \(C \equiv (\forall P.D \sqcap \exists P.D)\)
  \(D \equiv (\forall P.E \sqcap \exists P.E)\)
  \(E \equiv (\forall P.F \sqcap \exists P.F)\)
• \(Sat(C) =Sat(\forall P.D \sqcap \exists P.D)\)
• \(=Sat(\forall P.(\forall P.E \sqcap \exists P.E)\sqcap \exists P.(\forall P.E \sqcap \exists P.E))\)
• \(=Sat(\forall P.(\forall P.(\forall P.F \sqcap \exists P.F) \sqcap\) 
• \( \exists P.(\forall P.F \sqcap \exists P.F))\) 
• \(\sqcap \exists P.(\forall P.(\forall P.F \sqcap \exists P.F) \sqcap\)
• \( \exists P.(\forall P.F \sqcap \exists P.F)))\)

Lazy Unfolding

• Unfold only on demand
• inside tableau expansion
• minimally
• Unfold-rule:
• Condition: \(A \in \mathcal{L}(x)\) 
• and the current branch is complete but not closed
• and there is a definition \(A \equiv RHS\) in the TBox
• Action: \(\mathcal{L}(x) \leftarrow \mathcal{L}(x) \cup \{RHS\}\)
• This always helps!
• In ALC with empty TBox can explore each branch independantly
• In ALC plus definitorial TBox can expand and explore each branch independantly
• Possibility for early clash detection:
• \(C \equiv (\forall P.D \sqcap \exists P.\neg D)\)
  \(D \equiv (\forall P.E \sqcap \exists P.E)\)
• Eager unfolding forces 

Expressiveness

• When is logic A "more expressive" than logic B?
• When A can express things than B cannot?
• What sort of things? What's the test of successful expressing?
• \(BobIsAPerson\) vs. \(Bob:Person\)
• When A can express things in a given space that B cannot?
• Polynomially smaller? Exponentially smaller?
• Decidable logic A  is strictly less expressive than semi-decidable B
• Why? Because it is possible to encode a semi-decidable problem in B
• Not so in A!
• That is, given an inference service S (which is decidable) for A, and an undecidable problem P, it is not possible to encode P in A (A(p)) such that S says YES (rep. NO) for A(P) just in case the answer for P is YES (rep. NO)
• Not so for B. But then this means S for B cannot always be decided

Other Expressiveness

• Consider C disjointWith D
• vs. \(C \subseteq \neg D\)
• vs. (the stronger) \(C \equiv \neg D\)
• What happens when you want \([C_1\ldots C_n]\) to all be mutually disjoint?
• N*N axioms!
• Compare with  allDisjoint\([C_1\ldots C_n]\)
• Likely no effect on reasoner!
• Needs to maintain all the information anyway
• Free to use some efficient representation
• Easier for people
• Easier for editors, parsers, loaders, etc.