Limit expressive power?
Defaults, probabilities, etc. can all be thought of as extensions to FOL, with obvious applications
Why not strive for the union of all such extensions?
! a language co-extensive with English?
Problem: automated reasoning
Lesson here:
! reasoning procedures required for more expressive languages may not work very well in practice
Tradeoff: expressiveness vs. tractability
Overview:
– a Description Logic example
– limited languages
– the problem with cases
– vivid reasoning as an extreme case – less vivid reasoning
– hybrid reasoning systems
KR & R! © Brachman & Levesque 2005 Tradeoff
Simple Description Logic
Consider the language FL defined by:
!
! ! !
! ! !
!| (AND
!| (SOME
! | (RESTR
Example:
• (ALLchild (ANDFEMALESTUDENT))
an individual whose children are female students • (ALL(RESTRchild FEMALE)STUDENT)
an individual whose female children are students
! there may or may not be male children and they may or may not be students
Extension functions as before with ! Φ[(RESTR r c)] =
!{(x,y) | (x,y) ∈Φ[r] and y ∈Φ[c]} Subsumption defined as usual
KR & R! © Brachman & Levesque 2005 Tradeoff
Computing subsumption
First for FL ̄ = FL without the RESTR operator • puttheconceptsintonormalizedform
! (AND p1 … pk
!(SOME r1) … (SOME rm) !(ALL s1 c1) … (ALL sn cn) )
• to see if C subsumes D make sure that
1.!for every p ∈C, p ∈D
2.!for every (SOME r) ∈ C, (SOME r) ∈ D
3.!for every (ALLs c) ∈C, find an (ALLs d) ∈D such that c subsumes d.
Can prove that this method is sound and complete relative to definition based on extension functions
Running time:
• normalizationisO(n2) • structuralmatching:
! foreachpartofC, findapartofD: ! !againO(n2)
What about all of FL, including RESTR?
KR & R! © Brachman & Levesque 2005 Tradeoff
Subsumption in FL
Not so easy:
• cannotsettleforpart-by-partmatching
! (ALL(RESTRfriend (ANDMALEDOCTOR)) ! ! (AND TALL RICH))
! !subsumes
!
!
(AND! (ALL (RESTR friend MALE)! ! ! (AND TALL HAPPY)) ! (ALL (RESTR friend DOCTOR)
!
! ! ! (AND RICH SURGEON)))
• complexinteractions
! (SOME (RESTR r (AND a b))) ! !subsumes
!
!
(AND!(SOME(RESTRr (ANDcd))) (ALL (RESTR r c) (AND a e)) (ALL (RESTR r (AND d e)) b))
!
In general: can prove that FL is powerful enough to
encode all of propositional logic
! there is a mapping Ω from CNF wffs to FL where
|= (α ⊃ β) iff Ω[α] is subsumed by Ω[β]
! but |= (α ⊃ (p∧¬p)) iff α is unsatisfiable
Conclusion: there is no good algorithm for FL
! ! unless P=NP
KR & R! © Brachman & Levesque 2005 Tradeoff
Moral
Even small doses of expressive power come at a computational price
Questions:
• whatpropertiesofarepresentationlanguagecontrol its difficulty?
• howfarcanexpressivenessbepushedwithoutlosing good algorithms
• wheniseasyreasoningadequateforKRpurposes?
These questions remain unanswered, but some progress has been made
• needforcaseanalysesisamajorfactor
• tradeoffforDLlanguagesisreasonablywell understood
• bestaddressed(perhaps)bylookingatworking systems
Approach:
• findreasoningtasksthataretractable • analyzedifficultyinextendingthem
KR & R! © Brachman & Levesque 2005 Tradeoff
Limited languages
Some reasoning problems that can be formulated in terms of FOL entailment
? KB |= α
admit very specialized methods because of the restricted form of either KB or α
! although problem could be solved using full resolution theorem proving, there is no need
Example 1: Horn clauses
• SLDresolutionprovidesmorefocussedsearch
• inpropositionalcase,alinearprocedureisavailable
Example 2: Description logics
• CandoDLsubsumptionusingResolution
! Introduce predicate symbols for concepts, and “meaning postulates” like
! !∀x[P(x) ≡ ∀y(Friend(x,y) ⊃ Rich(y))
! !
! for !
! !
! !
∧ ∀y(Child(x,y) ⊃
! ! ∀z(Friend(y,z) ⊃ Happy(z)))]
(AND !(ALL friend RICH)
(ALL child (ALL friend HAPPY)))
! Then ask if MP |= ∀x[P(x) ⊃ Q(x)]
KR & R! © Brachman & Levesque 2005 Tradeoff
Equations
Example 3: linear equations
Let E be the usual axioms for arithmetic
! ∀x∀y(x+y = y+x), ∀x(x+0 = x), … Then have the following:
! E |= (x+2y=4 ∧ x–y=1) ⊃ (x=2 ∧ y=1)
Peano axioms
Can “solve” linear equations using Resolution
But there is a much better way:
! Gauss-Jordan method with back substitution
– subtract (2) from (1): 3y = 3 – divide by 3: y = 1
– substitute in (1): x = 2
In general, a set of linear equations can be solved in O(n3) operations
This idea obviously generalizes!
! always advantageous to use a specialized procedure when it is available, rather than a general method like Resolution
KR & R! © Brachman & Levesque 2005 Tradeoff
When is reasoning hard?
Suppose that instead of a set of linear equations, we have something like
! (x+2y=4 ∨ 3x–y=7) ∧ x–y=1
Can still show using Resolution: y > 0
To use GJ method, we need to split cases:
! x+2y=4 ∧ x–y=1 ß y=1 ! 3x–y=7 ∧ x–y=1 ß y=2
∴y > 0
! (eqnA1 ∨ eqnB1) ∧ (eqnA2 ∨ eqnB2)
What if 2 disjunctions?
! there are four cases to consider with GJ method
What if n binary disjunctions?
! (eqnA1 ∨ eqnB1) ∧ … ∧ (eqnAn ∨ eqnBn)
! there are 2n cases to consider with GJ method
! !withn=30,wouldneedtosolve109
!systems of equations!
Conclusion: even assuming a very efficient method,
case analysis is still a big problem Question: can we avoid case analyses??
KR & R! © Brachman & Levesque 2005 Tradeoff
Expressiveness of FOL
Ability to represent incomplete knowledge
! P(a) ∨ P(b)! ! !
! ∃x P(x)! ! ! !
! !and even
! c≠ 3! ! ! !
but which?
P(a) ∨P(b) ∨P(c) ∨… c=1∨c=2∨c=4∨…
Reasoning with facts like these requires somehow “covering” all the implicit cases
! languages that admit efficient reasoning do not allow this type of knowledge to be represented
e.g. Horn clauses, description logics, linear equations, …
One way to ensure tractability:
! somehow restrict contents of KB so that reasoning by cases is not required
But is complete knowledge enough for tractability? ! suppose KB|=αor KB|=¬α,asintheCWA
! Get: queries reduce to KB |= λ, literals
! But: it can still be hard to answer for literals ! example: KB = {(p ∨q), (¬p ∨q), (¬p ∨¬q)}
! Have: KB|=¬p∧q! ! complete
! !evenliteralsmayrequirecaseanalysis
KR & R! © Brachman & Levesque 2005 Tradeoff
Vivid knowledge
Note: If KB is complete and consistent, then it is satisfied by a unique interpretation I
! Why? define I by I|=p iff KB|=p
! Then for any I*, if I* |= KB then I* agrees with
I! ! ! ! ! on all atomic sentences p
Get: KB|=αiff I|=α
! entailments of KB are sentences that are true at I
! explains why queries reduce to atomic case
! (α∨β) is true iff αis true or βis true, etc.
! if we have the I, we can easily determine
what is or is not entailed
Problem: KB can be complete and consistent, but unique interpretation may be hard to find
as in the type of example on the previous slide
! want a KB that wears this unique interpretation on its sleeve
Solution: a KB is vivid if it is a complete and consistent set of literals (for some language)
! e.g. KB = {¬p, q} ! specifies I directly
To answer queries need only use KB+, the positive literals in KB, as in the CWA!
ignoring quantifiers for now
KR & R! © Brachman & Levesque 2005 Tradeoff
Quantifiers
As with the CWA, we can generalize the notion of vivid to accommodate queries with quantifiers
A first-order KB is vivid iff for some finite set of positive function-free ground literals KB+,
! KB=KB+∪Negs∪Dc∪Un
Get a simple recursive algorithm for KB |= α:
! KB |= ∃x.α iff KB |= α[x/c], for some c ∈ KB+
! KB|=(α∨β)iff KB|=αor KB|=β
! KB|=¬αiff KB|≠α
! KB|=(c=d) iff canddarethesameconstant
! KB|=p iff p∈KB+
This is just database retrieval
! useful to store KB+ as a collection of relations
Note: only KB+ is needed to answer queries, but Negs, Dc, and Un are required to justify procedure
! KB and KB+ are not logically equivalent
! !e.g. KB+ |= λ only if λ is positive
So: could generalize definition to have arbitrary sentences that entail Negs, Dc, and Un
KR & R! © Brachman & Levesque 2005 Tradeoff
Analogues
Can think of a vivid KB as an analogue of the world it is talking about
! there is a 1-1 correspondence between
– objects in the world and constants in the KB+
– relationships in the world and syntactic relationships in the KB+
! for example, if constants c1 and c2 stand for objects in the world o1 and o2
! there is a relationship R holding between objects o1 and o2 in the world
!! iff
! the constants c1 and c2 appear together as a
tuple in the relation represented by R Not true in general
! for example, if KB = {P(a)} then it only uses 1 constant, but could be talking about a world where there are 5 individuals of which 4 satisfy P
Result: certain operations are easy
– how many objects satisfy P (by counting) – changes to the world (by changes to KB+)
KR & R! © Brachman & Levesque 2005 Tradeoff
Beyond vivid
Requirement of vividness is very strict.
Would like to consider weaker alternatives with good reasoning properties
Extension 1
Suppose KB is a finite set of literals
– not necessarily a complete set (no CWA) – assume consistent, else trivial
Cannot reduce KB |= α to literal queries
! !for example, if KB = {p}
! then KB |= (p∧q ∨ p∧¬q)
! but KB|≠p∧q and KB|≠p∧¬q
ignoring quantifiers again
But: assume α is small. Can put into CNF ! αß (c1∧…∧cn)
• KB|=αiff KB|=ci, foreveryclauseinCNFofα
• KB |= c iff c has complementary literals – tautology
! ! or !KB∩c is notempty ! !Why?
KR & R! © Brachman & Levesque 2005 Tradeoff
Extension 2
Imagine KB vivid as before + new definitions: ! ∀xyz[R(x,y,z) ≡ … wff in vivid language …]
! Example: have vivid KB using predicate ParentOf ! add: ∀xy[MotherOf(x,y) ≡ ParentOf(x,y) ∧ Female(x)]
To answer query containing R(t1,t2,t3), simply macro expand it with definition and continue
• canhandlearbitrarylogicaloperatorsindefinition since they become part of query, not KB
• cangeneralizetohandlepredicatesnotonlyinvivid KB, provided that they bottom out to KB+
! !∀xy[AncestorOf(x,y) ≡ ParentOf(x,y) ∨
! ! ∃z ParentOf(x,z) ∧ AncestorOf(z,y)]
• clearrelationtoProlog
Others…
Vivification: given non-vivid KB, attempt to make vivid e.g. by eliminating disjunctions etc.
! e.g. use defaults to choose between disjuncts
Problem: what to do with function symbols, when Herbrand universe is not finite?
! partial Herbrand base?
KR & R! © Brachman & Levesque 2005 Tradeoff
Hybrid reasoning
Want to be able to incorporate into a single system special-purpose efficient reasoners
How can they coexist within a general scheme such as Resolution?
! a variety of approaches for hybrid reasoners
Simple form: semantic attachment
• attachprocedurestofunctionsandpredicates
! e.g. numbers: procedures on plus, LessThan, …
• groundtermsandatomicsentencescanbeevaluated
prior to Resolution
! P(factorial(4), times(2,3)) ß P(24, 6) LessThan(quotient(36,6), 5) ∨ α ß α
• muchbetterthanreasoningdirectlywithaxioms
More complex form: theory resolution
• buildtheoryintounificationprocess
! the way paramodulation builds in =
• extendednotionofcomplementaryliterals
! {α, LessThan(2,x)} and {LessThan(x,1), β} ! ! resolve to {α,β}
KR & R! © Brachman & Levesque 2005 Tradeoff
Using descriptions
Imagine that predicates are defined elsewhere as concepts in a description logic
! Married ≡ (AND …)!! ! Bachelor ≡ (AT-MOST …)
then want
! {P(x), Married(x)} and {Bachelor(john), Q(y)}
! !toresolveto
! {P(john), Q(y)}
! since the other two literals are contradictory
for x=john, given DL definitions
Can use description logic procedure to decide if two predicates are complementary
instead of explicit meaning postulates
Residues: for “almost” complementary literals
! {P(x), Male(x)} and {¬Bachelor(john), Q(y)}
! !resolveto
! {P(john), Q(y), Married(john)}
! since the two literals are contradictory unless John is married
Main issue: completeness of theory resolution
• whatresolventsarenecessarytogetthesame conclusions as if meaning postulates were used
• residuesarenecessaryforcompleteness
KR & R! © Brachman & Levesque 2005 Tradeoff