Introduction to Artificial Intelligence LECTURE 11: Nonmonotonic Reasoning : Introduction to Artificial Intelligence LECTURE 11: Nonmonotonic Reasoning Motivation: beyond FOL + resolution
Closed-world assumption
Default rules and theories
Ref: “Logical Foundations of AI”, Genesereth and Nilsson, Morgan Kauffman, 1987.
Knowledge representation with FOL + resolution : Knowledge representation with FOL + resolution FOL + resolution have limitations in the kind of sentences and deductions we can make.
cannot express uncertainty
cannot make unsound but likely deductions
cannot revise conclusions in light of new knowledge
cannot make conclusions based on the entire state of the KB
Motivation: incompleteness : Motivation: incompleteness If we cannot prove P or ~P from KB, what should we conclude? KB: neighbor(israel,jordan) neighbor(israel,egypt) neighbor(lebanon,syria)
…
Query: neighbor(israel,morroco)
Cannot conclude anything unless there is an explicit statement (negation) in KB!
Motivation: exceptions : Motivation: exceptions All rules have exceptions! For each, we must forsee all of them and explicitly state them: “all birds fly” X bird(X) => flies(X) “except ostriches” X bird(X) /\ ~ostrich(X) => flies(X) “except newborns” X bird(X) /\ ~ostrich(X) /\ ~newborn(X) => flies(X)
We would like to conclude flies(X) from bird(X) unless something is abnormal with X X bird(X) /\ ~Abnormal(X) => flies(X)
Motivation: changes : Motivation: changes We assumed that all clauses in KB are true and remain true. What if we later discover that this is not the case? How do we revise conclusions already made? X citizen(X) /\ income(X,Y) => pay_tax(X,Y)
As the rules change, we need to revise all the intermediate conclusions!
We would like to identify only those that indeed need revision
Possible extensions : Possible extensions Language: make it more expressive without loosing some of its computational properties
Semantics: revise the concept of truth value
Inferencing: design new inference rules to deal with exceptions, uncertainty, etc
Minimal extensions to FOL+new inference rules!
Nonmonotonic logics (NML) : Nonmonotonic logics (NML) FOL + resolution is monotonic: if KB |= P then (KB U {Q}) |= P for all consistent KB and all Q obtained from KB by applying resolution.
The number of statements known to be true is strictly increasing over time
Non-monotonic: “jump” to conclusions that can later be withdrawn (defeasible conclusions)
Consistency in NML : Consistency in NML A deduction rule R is consistent iff:
KR |=R c
KR U {c} |= Ø iff KR |= Ø
TR(KB) = the set of all conclusions from KB using inference rule R (transitive closure).
Note: R is applied in parallel!
Nonmonotonic frameworks : Nonmonotonic frameworks 1. Closed World Assumption
if you cannot prove P or ~P from KB, add ~P to KB.
2. Default Rules
new inference rules on how to augment KB
3. (Predicate completion -- Circumscription)
compute a formula which says how KB should be satisfied
4. (Truth Maintenance Systems)
methods to maintain consistency in a KB where statements are constantly added and deleted
1. Closed-world assumption (CWA) : 1. Closed-world assumption (CWA) if you cannot prove P or ~P from KB,
add ~P to KB
KB |= c and KB |= ~c then add ~c
Idea: if you cannot prove P, assume it is false. This means you assume you know everything there is to know about the world (e.g. the world is closed).
This is the semantics of databases and of PROLOG.
Complete theories : Complete theories A theory T is a set of sentences closed under logical implication (like transitive closure)
T is complete if either every ground literal in the language or its negation is in the theory KB: neighbor(israel,jordan) neighbor(israel,egypt)
X Yneighbor(X,Y) <=> neighbor(Y,X)
T(KB) is not complete because neither neighbor(egypt,jordan) or ~neighbor(egypt,jordan) is in T(KB).
Theory completion : Theory completion Given an incomplete KB, include the negation of a ground literal when the ground literal does not follow from KB
KB: neighbor(israel,jordan) neighbor(israel,egypt)
X Y neighbor(X,Y) <=> neighbor(Y,X)
The atom ~neighbor(egypt,jordan) will be added
Is this always consistent? NO!
Completion inconsistency : Completion inconsistency Completion can lead to inconsistent theories: KB: p(a) \/ p(b) neither KB |= ~p(a), p(a) nor KB |= ~p(b), p(b) follow So we add ~p(a) and ~p(b) to KB: KB’: p(a) \/ p(b) ~p(a) ~p(b) KB’ is inconsistent!
Modify the completion rule for consistency
CWA theorem (1) : CWA theorem (1) Augment a consistent KB with a new set of sentences (beliefs), to obtain a new consistent set CWA(KB).
Theorem: CWA(KB) is consistent iff for every disjunction p1 \/ p2 \/ …. \/ pn, that follows from KB, where pi is a positive-ground literal, there is at least one pi such that KB |= pi
Eq: CWA(KB) is inconsistent iff there are positive ground literals p1, … pn such that KB |= p1 \/ p2 \/ …. \/ pn but for all i, KB | pi.
CWA theorem (2) : CWA theorem (2) Intuition: add all of ~ pi except one, so no contradiction occurs!
Proof: Let KBassumed be the set of all conclusions ~p derived
with CWA rule:
~p is in KBassumed iff KB |= p and KB |= ~p
CWA(KB) is inconsistent only if KB U KBassumed is.
Then, there is a finite subset of KBassumed that
contradicts KB. Let this subset be L = {~p1,…,~pn}.
Then KB |= p1 \/ p2 \/ …. \/ pn, the negation of L. Since each
~pi is in KBassumed by the definition of KBassumed KB |= pi contradiction!
Consistent CWA rule : Consistent CWA rule Complete a KB by including all ground literals that do not contradict the theorem.
Important: define the constant atoms first
Ex1: KB: p(a) \/ p(b) is not consistent
Ex2: KB: X p(X) \/ q(X) p(a) q(b) for atoms a,b, the augmentation is ~q(a) and ~p(b) OK
for atom c, the augmentation is inconsistent: NOT OK (p(X) \/ q(X)) | p(c) or (p(X) \/ q(X)) | q(c)
CWA consistency for Horn clauses : CWA consistency for Horn clauses In general, testing for consistency to see what negated ground literals to add to KB can be expensive!
Not so for Horn clauses: Theorem: CWA(KB) is always consistent when KB is a consistent set of Horn clauses.
Follows from the fact that Horn clauses have a single positive literal.
Variant: define CWA for a subset of clauses only.
Restricted CWA : Restricted CWA Define the predicates on which CWA is applied
KB: X q(X) => p(X)
q(a)
p(b) \/ r(b)
If we apply CWA to p(X), we will conclude only
~p(b), which keeps consistency (~r(b) cannot
be inferred)
Other assumptions : Other assumptions Domain closure assumption:
Limit the constant terms in the language to be those that can be named using constant and function symbols in KB. Strong assumption: allows replacing universal quantifiers by finite conjunctions and disjunctions. X p(X) is (X=a1 \/ X = a2…) /\ p(X)
Unique names assumption: if ground terms cannot be proved equal, assume they can be assumed unequal. p(f1(a)) = p(f2(a))
where f1 and f2 are Skolem functions
2. Default rules and theories : 2. Default rules and theories Define a nonstandard, nonmonotonic set D of inference rules to augment the basic KB. The augmentation of KB with D, denoted E(KB,D) is the theory that contains the usual conclusions + those obtained by applying D on KB.
The default rules in D are of the form: bird(X) : flies(X)
flies(X)
“if X is a bird, and it is consistent to believe that X can fly, then it can be believed that X can fly”.
Default rules semantics : Default rules semantics
(X): (X) (X)
If there is an instance x of X for which the ground instance (x) follows from E(KB,D) and for which (x) is consistent with E(KB,D), then include (x) in E(KB,D).
Default rules are useful to express beliefs that are usually but not necessarily true
In general, E(KB,D) is not unique!
Example 1 : Example 1 KB: bird(tweety)
X ostrich(X) => ~flies(X)
D: bird(X): flies(X)
flies(X)
then flies(tweety) is in E(KB,D).
If we add ostrich(tweety), then we cannot deduce flies(tweety) because it is not consistent with KB.
Example 1 (continued) : Example 1 (continued) KB: feathers(tweety)
D: bird(X) : flies(X) feathers(X): bird(X)
flies(X) bird(X)
Default proof that flies(tweety).
If we add
ostrich(tweety)
ostrich(X) => ~flies(X)
ostrich(X) => feathers(X)
we cannot (as expected) prove that flies(tweety).
Example 2 : Is the default rule :~p(X)
~p(X)
the same as CWA? No!
KB: p \/ q D: :~p and :~q ~p ~q
CWA(KB) is inconsistent
E(KB,D) can be either {p \/ q, ~p} or {p \/ q,~q}
However, the union of both is inconsistent! Example 2
Properties of default theories : Properties of default theories Default theories might have more than one augmentation (see previous example)
There are default theories with no augmentations KB = {p(X)}, D is :p(X)/~p(X)
Every normal default theory (only D statements of the form (X): (X)/ (X)) has an augmentation
If D’ D are sets of normal rules then for any E(KB,D’) there is a E(KB,D) such that E(KB,D’) E(KB,D).
Normal default rules are semi-monotonic.
Example 3: anomalities (1) : Example 3: anomalities (1) Typically, drug dealers are adults
Typically, adults are employed
dealer(X): adult(X) adult(X):employed(X)
adult(X) employed(X)
dealer(joe)
adult(joe) (from default rule 1)
employed(joe) (from default rule 2)
Question: how to fix this anomality?
Example 3: anomalities (2) : Example 3: anomalities (2) Exchange the second rule by:
adult(X) : ~dealer(X) /\ employed(X)
employed(X)
but it is not in normal form!
Consider instead the new rules:
dealer(X): adult(X) adult(X) /\ ~dealer(X) :employed(X)
adult(X) employed(X)
adult(X): ~dealer(X)
~dealer(X)
Default rules: observations : Default rules: observations The difference between CWA(KB) and E(KB,D)
CWA: add ~p if consistent with KB
Default: add ~p if consistent with E(KB,D)
=> the order matters!!
Inference with normal defaults: (X): (X)
(X)
Forward: check (X) at the time of the application
Backward: two passes. First, ignore consistency
checks and them verify them on the resulting chain
3. Predicate completion : 3. Predicate completion The only objects that satisfy a predicate are those who must do so
KB: p(a) (a single predicate and atom)
X X= a => p(X) if
Assuming there are no other atoms satisfying P:
X p(X) => X = a only if This is the completion of the if formula
Def: The completion of P in KB is
COMP(KB;p) KB /\ (X p(X) => X = a)
X p(X) <=> X = a
Predicate completion: example : Predicate completion: example What about more than one atom?
KB: p(a)
p(b)
COMP(KB;p) X ((X=a) \/ (X=b)) <=> p(X)
In these examples, predicate completion works like a CWA with respect to a predicate
Predicate completion is not defined for arbitrary formulas -- only for solitary clauses
Solitary clauses : Solitary clauses Def: A set of clauses is solitary in p if each clause with a positive occurrence of p has at most one occurrence of p.
KB: p(a) \/ q(a) p and q are solitary
KB: p(a) \/ q(a) \/ ~p(b) p is not solitary
Predicate completion (1) : Predicate completion (1) Rewrite all clauses solitary in p in the form
Y q1 /\ q2 /\ ... /\ qk => p(T)
where qi are literals not containing p
T is a tuple of terms T = (T1, ...., Tn)
p(a,b) T = (a,b)
p(c,d) T= (c,d)
The qi and t may contain variables, i.e the tuple of variables Y.
Predicate completion (2) : Predicate completion (2) The expression is equivalent to:
YX (X=T) /\ q1 /\ q2 /\ ... /\ qk) => p(X)
where X is a tuple of variables not occurring in T and (X = T) stands for (X1 = t1 /\ .... /\ Xn = tn)
Since Y appears only in the antecedent of the implication, this is equivalent to:
X ( Y (X=T) /\ q1 /\ q2 /\ ... /\ qk) => p(X))
We re-write in normal form all such clauses
X E1 => p(X) ....
X Ek => p(X)
Predicate completion rule (3) : Predicate completion rule (3) where Ei are existentially quantified conjunction of literals
Grouping them together, we obtain:
X (E1 \/… \/ Ek) => p(X)
The completion rule is then
X p(X) => (E1\/…\/ Ek)
COMP(KB;p) KB /\
X p(X) <=> (E1\/…\/ Ek)
where Ei are the antecedents of the normal forms of the clauses in KB
Predicate completion example : Predicate completion example Given the KB:
1. X ostrich(X) => bird(X) all ostriches are birds
2. bird(tweety) tweety is a bird
3. ~ostrich(sam) sam is not an ostrich
Question: is sam a bird?
bird is solitary in 1. Its completion is: 4. X (X = tweety) \/ ostrich(X) <=> bird(X)
We can now prove ~bird(sam)
More on nonmonotonic logics : More on nonmonotonic logics Many different formalisms to deal with inferences of this type
circumscription: extension of predicate completion
Truth Maintenance Systems
To learn more, see advanced courses
deduction systems
advanced logics and AI courses