EECS 3401 — AI and Logic Prog. — Lecture 6
Adapted from slides of Prof. Yves Lesperance
Vitaliy Batusov
vbatusov@cse.yorku.ca
York University
September 30, 2020
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 6 September 30, 2020 1 / 29
Inference in First-Order Logic
Today: Inference in First-Order Logic
Required reading: Russell & Norvig, Chapters 9.1, 9.2, 9.5
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 6 September 30, 2020 2 / 29
Computing Logical Consequences
Recap:
KB is a set of axioms
Reasoning = finding logical consequences of a KB
Logical consequence is a semantic notion
If a formula φ holds in every model of a KB, then KB |= φ
Can this be done mechanically/in code?
Yes. There are procedures for generating logical consequences Called proof procedures
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 6 September 30, 2020 3 / 29
Proof Procedures
Proof procedures operate by simply manipulating formulas. They pay no heed whatsoever to interpretations
Still, they respect the semantics of the interpretations!
We will develop a proof procedure for FOL called resolution
Prolog uses resolution, you’ve seen it work already.
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 6 September 30, 2020 4 / 29
Properties of Proof Procedures
Notation: KB ⊢ φ means that formula φ can be proved from the KB (using some implicit proof procedure).
Generally speaking, what properties do we expect a proof procedure to have?
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 6 September 30, 2020 5 / 29
Properties of Proof Procedures
Two fundamental properties:
Soundness If KB ⊢ φ, then KB |= φ
(if we derive a formula from KB via the proof procedure, it better be a logical consequence of KB)
Completeness If KB |= φ, then KB ⊢ φ
(if a formula is a logical consequence, our proof procedure should be capable of deriving it from KB)
Note: proof procedures are computable, but they might have very bad complexity in the worst case. Completeness is not necessarily achievable in practice
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 6 September 30, 2020 6 / 29
Resolution: Clausal Form
Resolution works with formulas in a particular form — clausal form A literal is an atomic formula or the negation of an atomic formula
A literal: dog(fido). Also a literal: ¬cat(fido).
Not a literal: cat(fido) ∨ dog(fido) because contains disjunction
A clause is a disjunction of literals
A clause: cat(fido) ∨ dog(fido)
Also a clause: ¬owns(fido, fred) ∨ ¬dog(fido) ∨ person(fred)
Not a clause: ¬cat(fido) ∧ ¬dog(fido) because contains conjunction Since a clause is always a disjunction, we can treat it as a
collection/tuple of literals:
(¬owns(fido, fred), ¬dog(fido), person(fred))
A clausal theory is a conjunction of clauses
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 6 September 30, 2020 7 / 29
Clausal Form
A Horn clause is a clause with no more than one positive literal A Horn clause: (¬owns(fido, fred), ¬dog(fido), person(fred))
Not a Horn clause: (cat(fido),dog(fido))
Prolog programs are clausal theories. Every fact or rule in a Prolog
program is a Horn clause.
¬q1 ∨¬q2 ∨…∨¬qn ∨p (q1 ∧ q2 ∧ . . . ∧ qn) → p
p :- q_1, q_2, … , q_n.
Horn clause same, as an implication same, as a Prolog rule
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 6
September 30, 2020
8 / 29
Resolution Rule for Ground Clauses
Basic Principle of Resolution: From two clauses (p,q1,q2,…,qk) and (¬p,r1,r2,…,rn),
infer the new clause
(q1,q2,…,qk,r1,r2,…,rn).
Example: from
(¬largerThan(clyde, cup), ¬fitsIn(clyde, cup)) and
infer the new clause
(¬largerThan(clyde, cup)). Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 6
(fitsIn(clyde, cup)),
September 30, 2020 9 / 29
Resolution Proof: Forward Chaining
Logical consequences can be generated from the resolution rule in two ways: Forward Chaining and Refutation.
Forward Chaining Inference: chain multiple resolution steps Suppose we have a sequence of clauses C1, C2, . . . , Ck
Suppose that each Ci is either in the KB or is the result of a resolution step involving two prior clauses in the sequence
Then, we have that KB ⊢ Ck
Forward chaining is sound, so we also have KB |= Ck
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 6 September 30, 2020 10 / 29
Resolution Proof: Refutation Proofs
Refutation Proofs: a proof by contradiction
Fact: KB |= φ iff KB ∧ ¬φ has no model (“unsatisfiable”)
Since resolution is sound, then if we can derive a contradiction from KB ∧ ¬φ, we consider φ proved
A contradiction is the empty clause ()
A proof:
Suppose we have a sequence of clauses C1, C2, . . . , Cm
Suppose that each Ci is either in the KB ∧ ¬φ or is the result of resolving two prior clauses in the sequence
Suppose Cm is ()
Then KB ⊢ φ
By soundness, KB |= φ.
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 6 September 30, 2020 11 / 29
Resolution Proof Example: Forward Chaining
Knowledge Base: (in clausal form)1
(elephant(clyde), giraffe(clyde)) (¬elephant(clyde), likes(clyde, peanuts)) (¬giraffe(clyde), likes(clyde, leaves)) (¬likes(clyde, leaves))
Want to prove: likes(clyde,peanuts)
Using forward chaining:
Resolve (3) & (4), get new clause (5) = (¬giraffe(clyde)) Resole (5) & (1), get new clause (6) = (elephant(clyde)) Resolve (6) & (2), get desired conclusion (likes(clyde,peanuts))
1Reminder: A → B stands for ¬A ∨ B
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 6 September 30, 2020
(1) (2) (3) (4)
12 / 29
Resolution Proof Example: Refutation
Knowledge Base:
(elephant(clyde), giraffe(clyde)) (¬elephant(clyde), likes(clyde, peanuts)) (¬giraffe(clyde), likes(clyde, leaves)) (¬likes(clyde, leaves))
Want to prove: likes(clyde,peanuts)
(1) (2) (3) (4)
Using refutation:
Add negation of query Resolve (5) & (2), get Resolve (6) & (1), get Resolve (7) & (3), get Resolve (8) & (4), get
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU)
to KB: (5) = ¬likes(clyde,peanuts) (6) = (¬elephant(clyde))
(7) = (giraffe(clyde))
(8) = (likes(clyde,leaves))
the empty clause ()
EECS 3401 Lecture 6 September 30, 2020
13 / 29
Resolution Proofs
Proofs by refutation have the advantage that they are easier to find — they are more focused on the particular conclusion we are trying to reach
To develop a complete resolution proof procedure for First-Order Logic, we need:
1 A way of converting a KB and the query φ into clausal form [Today’s focus]
2 A way of extending resolution to work on formulas with variables [unification! Will cover next Monday]
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 6 September 30, 2020 14 / 29
Conversion to Clausal Form
An 8-step procedure to convert a KB into clausal form:
1 Eliminate implications
2 Move negations inwards and simplify ¬¬q
3 Standardize variables
4 Skolemize
5 Convert to Prenex form
6 Distribute conjunctions over disjunctions
7 Flatten nested conjunctions and disjunctions
8 Convert to clauses
Will use this example to illustrate:
∀X p(X)→ ∀Y p(Y)→p(f(X,Y)) ∧¬ ∀Y(¬q(X,Y)∧p(Y))
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 6 September 30, 2020 15 / 29
Step 1: Eliminate Implications
Given:
∀X p(X)→ ∀Y p(Y)→p(f(X,Y)) ∧¬ ∀Y(¬q(X,Y)∧p(Y)) Eliminate implications: replace A → B with ¬A ∨ B
Obtain:
∀X ¬p(X)∨ ∀Y ¬p(Y)∨p(f(X,Y)) ∧¬ ∀Y(¬q(X,Y)∧p(Y))
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 6 September 30, 2020 16 / 29
Step 2: Move Negation Inwards
Given:
∀X ¬p(X)∨ ∀Y ¬p(Y)∨p(f(X,Y)) ∧¬ ∀Y(¬q(X,Y)∧p(Y)) Move negation inwards and simplify double negations
Obtain:
¬(¬A) ¬(A∧B) ¬(A∨B) ¬∀X (A) ¬∃X (A)
becomes becomes becomes becomes becomes
A
(¬A ∨ ¬B) (¬A ∧ ¬B) ∃X (¬A) ∀X (¬A)
∀X ¬p(X)∨ ∀Y ¬p(Y)∨p(f(X,Y)) ∧ ∃Y(q(X,Y)∨¬p(Y))
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 6 September 30, 2020 17 / 29
Step 3: Standardize Variables
Given:
∀X ¬p(X)∨ ∀Y ¬p(Y)∨p(f(X,Y)) ∧ ∃Y(q(X,Y)∨¬p(Y)) Rename variables so that each quantified variable is unique
Obtain:
∀X ¬p(X)∨ ∀Y ¬p(Y)∨p(f(X,Y)) ∧ ∃Z(q(X,Z)∨¬p(Z))
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 6 September 30, 2020 18 / 29
Step 4: Skolemize
Given:
∀X ¬p(X)∨ ∀Y ¬p(Y)∨p(f(X,Y)) ∧ ∃Z(q(X,Z)∨¬p(Z)) “Skolemize”: remove all existential quantifiers ∃ by introducing new
function symbols in place of the formerly-quantified variables Obtain:
∀X ¬p(X)∨ ∀Y ¬p(Y)∨p(f(X,Y)) ∧ q(X,g(X))∨¬p(g(X))
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 6 September 30, 2020 19 / 29
Skolemization Explained
Consider an example:
∃Y (elephant (Y ) ∧ friendly (Y ))
This states that there is some individual (a binding for Y ) that is
both an elephant and friendly
To remove the existential quantifier, we invent a name for this entity, let’s say a. This is a new constant symbol, not equal to any previous constant symbols. We get a logically equivalent statement:
elephant(a) ∧ friendly(a)
This is saying exactly the same thing, since we know nothing about this new constant apart from the fact that it exists and has to be bound to some individual
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 6 September 30, 2020 20 / 29
Skolemization Explained
It is essential that the introduced symbol a is new. Otherwise, we might know something about a from the KB
If the KB had something to say about the constant a, we would be asserting more than the existential did about that individual(s) hiding under the name Y
In the original quantified formula, we know nothing about the variable Y except what was being asserted by the formula itself
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 6 September 30, 2020 21 / 29
Skolemization Explained
A less trivial example:
∀X ∃Y (loves(X , Y ))
This states that for every X there is some Y that loves X — could be
a different Y for each X
Replacing the existential by a new constant won’t work
∀X (loves (X , a))
because now there is one particular individual a loved by every X
To properly convert existential quantifiers which are inside the scope of universal quantifiers, we must use functions and not just dumb constants
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 6 September 30, 2020 22 / 29
Skolemization Explained
We must use a function which takes as an argument (i.e., depends on) every universally quantified variable that scopes the existential
In our example, Y is inside the scope of ∀X (“X scopes Y ”), so we must replace the existential Y by a function of X:
∀X(loves(X,g(X))), where g is a new function symbol.
Now, the formula asserts that for every X there is some individual (as given by g(X)) that X loves. Since g is a new symbol, it could be interpreted arbitrarily, so g(X) could be different for each binding of X.
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 6 September 30, 2020 23 / 29
Skolemization: Some More Examples
∀X∀Y∀Z∃W. r(X,Y,Z,W) becomes
∀X∀Y∀Z. r(X,Y,Z,h1(X,Y,Z))
∀X∀Y∃W. r(X,Y,g(W)) becomes
∀X∀Y. r(X,Y,g(h2(X,Y)))
∀X ∀Y ∃W ∀Z . r (X , Y , W ) ∧ q(Z , W ) becomes
∀X∀Y∀Z. r(X,Y,h3(X,Y))∧q(Z,h3(X,Y))
Vitaliy Batus∀ovXvb∀atYuso∃v@Wcse∀.yZork(ur.c(aX(Y,orYkU,) W )E∧ECqS 3(4Z01,LWectu)re)6 becomes September 30, 2020 24 / 29
Step 5: Convert to Prenex Normal Form
Given:
∀X ¬p(X)∨ ∀Y ¬p(Y)∨p(f(X,Y)) ∧ q(X,g(X))∨¬p(g(X))
Bring all quantifiers to the outside (front). At this point, we only have universals left, and each quantifies a differently-named variable
Obtain:
∀X∀Y ¬p(X)∨ ¬p(Y)∨p(f(X,Y)) ∧ q(X,g(X))∨¬p(g(X))
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 6 September 30, 2020 25 / 29
Step 6: Conjunctions Over Disjunctions
Given:
∀X∀Y ¬p(X)∨ ¬p(Y)∨p(f(X,Y)) ∧ q(X,g(X))∨¬p(g(X))
Apply the distributive law: A ∨ (B ∧ C) becomes (A ∨ B) ∧ (A ∨ C) Obtain:
∀X∀Y ¬p(X)∨(¬p(Y)∨p(f(X,Y)))
∧¬p(X)∨(q(X,g(X))∨¬p(g(X)))
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 6 September 30, 2020 26 / 29
Step 7: Flatten
Given:
∀X∀Y ¬p(X)∨(¬p(Y)∨p(f(X,Y)))
∧¬p(X)∨(q(X,g(X))∨¬p(g(X)))
Flatten nested conjunctions and disjunctions: (A ∨ (B ∨ C )) becomes (A ∨ B ∨ C )
Obtain:
∀X∀Y ¬p(X)∨¬p(Y)∨p(f(X,Y))
∧¬p(X)∨q(X,g(X))∨¬p(g(X))
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 6 September 30, 2020 27 / 29
Step 8: Convert to Clauses
Given:
∀X∀Y ¬p(X)∨¬p(Y)∨p(f(X,Y))
∧¬p(X)∨q(X,g(X))∨¬p(g(X))
Remove quantifiers and break apart conjunctions (this is purely notational, we are not changing the formula any more. The removed symbols become implicit)
Obtain:
¬p(X)∨¬p(Y)∨p(f(X,Y)) ¬p(X)∨q(X,g(X))∨¬p(g(X))
We are now in clausal form.
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 6 September 30, 2020 28 / 29
End of Lecture
(¬p(X),¬p(Y),p(f(X,Y))) (¬p(X),q(X,g(X)),¬p(g(X)))
Observe: we now have variables in the clauses! Next lecture: how resolution handles this (Unification)
Vitaliy Batusov vbatusov@cse.yorku.ca (YorkU) EECS 3401 Lecture 6 September 30, 2020 29 / 29