Predicate Calculus
Chapter 12
Predicate calculus
§ Predicate: function that maps constants and variables to true and false
§ First order predicate calculus: notation and inference rules for constructing and reasoning about propositions:
§ Operators: § and ⋀
§ or ⋁
§ not ¬
§ implication → § equivalence ⟷
§ Quantifiers:
§ existential ∃
§ universal ∀
2
Predicate calculus
§ Examples
∀C(rainy(C) ⋀ cold(C) → snowy(C))
∀A,∀B(takes(A, C) ⋀ takes(B, C) → classmates(A, B))
§ Fermat’s last Theorem:
∀N ((N > 2) → ¬(∃A ∃B ∃C(AN + BN = CN)))
§ ∀, ∃ bind variables like λ in λ-calculus
3
Predicate calculus
§ Normal form
§ the same thing can be written in different ways:
(P→Q) ≡ (¬P ∨Q) ¬∃X (P(X)) ≡ ∀X (¬P(X)) ¬(P ∧ Q) ≡ (¬P ∨ ¬Q)
§ This is good for humans, bad for machines
§ Automatic theorem proving requires a normal form
4
Clausal Form
§ Clausal form § Example:
∀X (¬student(X) → (¬resident(X) ∧ ¬∃Y (takes(X, Y) ∧ class(Y))))
§ 1. eliminate → and ↔:
∀X (student(X) ∨ (¬resident(X) ∧ ¬∃Y (takes(X, Y) ∧ class(Y))))
5
Clausal Form
∀X (student(X) ∨ (¬resident(X) ∧ ¬∃Y (takes(X, Y) ∧ class(Y))))
§ 2. move ¬ inward (using De Morgan’s laws):
∀X (student(X) ∨ (¬resident(X) ∧ ∀Y (¬(takes(X, Y) ∧
class(Y))))) ≡
∀X (student(X) ∨ (¬resident(X) ∧ ∀Y (¬takes(X, Y) ∨ ¬class(Y))))
6
Clausal Form
∀X (student(X) ∨ (¬resident(X) ∧ ∀Y (¬takes(X, Y) ∨ ¬class(Y))))
§ 3. eliminate existential quantifiers
§ Skolemization (not necessary here)
§ 4. pull universal quantifiers to the outside of the proposition (some renaming might be needed)
∀X ∀Y (student(X) ∨ (¬resident(X) ∧ (¬takes(X, Y) ∨ ¬class(Y))))
§ convention: rules are universally quantified § we drop the implicit ∀’s:
student(X) ∨ (¬resident(X) ∧ (¬takes(X, Y) ∨ ¬class(Y)))
7
Clausal Form
student(X) ∨ (¬resident(X) ∧ (¬takes(X, Y) ∨ ¬class(Y)))
§ 5. convert the proposition in conjunctive normal form § conjunction of disjunctions
(student(X) ∨ (¬resident(X)) ∧ (student(X) ∨ ¬takes(X, Y) ∨ ¬class(Y))
8
Clausal Form
(student(X) ∨ (¬resident(X)) ∧ (student(X) ∨ ¬takes(X, Y) ∨ ¬class(Y))
§ We can rewrite as: (resident(X) → student(X)) ∧
((takes(X, Y) ∧ class(Y)) → student(X)) ≡
(student(X) ← resident(X)) ∧ (student(X)← (takes(X,Y)∧class(Y)))
9
Clausal Form
§ We obtained:
(student(X) ← resident(X)) ∧
(student(X)← (takes(X,Y)∧class(Y))) § which translates directly to Prolog:
student(X) :- resident(X).
student(X) :- takes(X, Y), class(Y).
:- means “if” , means “and”
10
Horn Clauses
§ Horn clauses
§ particular case of clauses: only one non-negated:
¬Q1 ∨¬Q2 ∨…∨¬Qk ∨P ≡ Q1∧Q2 ∧…∧Qk →P≡ P←Q1 ∧Q2 ∧…∧Qk
§ which is a rule in Prolog:
P :- Q1, Q2,…,Qk.
§ for k = 0 we have a fact: P.
11
Automated proving
§ Rule: both sides of :-
P :- Q1, Q2,…,Qk. means P ← Q1 ∧ Q2 ∧…∧ Qk
§ Fact: left-hand side of (implicit) :- P. means P ← true
§ Query: right-hand side of (implicit) :-
?- Q1, Q2,…,Qk. means false ← Q1 ∧ Q2 ∧…∧ Qk
§ Automated proving: given a collection of axioms (facts and rules), add the negation of the theorem (query) we want to prove and attempt (using resolution) to obtain a contradiction
12
Automated proving
§ Example student(john).
?- student(john).
true.
§ Fact: student(john) ← true
§ Query (negated): false ← student(john)
§ We obtain a contradiction (that proves the query): false ← student(john) ← true
§ The above contradiction is obvious; in general, use resolution. 13
Resolution
§ Resolution (propositional logic):
§ From hypotheses:
(A1 ∨A2 ∨…∨Ak∨C)∧(B1 ∨B2 ∨…∨Bl∨¬C)
§ We can obtain the conclusion:
A1 ∨A2 ∨…∨Ak∨B1 ∨B2 ∨…∨Bl
§ Example: modus ponens
p→q∧p gives q (becausep→q is ¬p∨q)
§ In predicate logic:
§ C and ¬C’: where C, C’ may not be identical but can be unified: that means, they can be made identical by substituting variables (details later)
14
Resolution
§ Example:
student(X) :- resident(X).
student(X) :- takes(X, Y), class(Y).
resident(john).
takes(mark, 3342).
class(3342).
?- student(john).
true
§ Resolution (add negation of query): (¬resident(X) ∨ student(X)) ∧
(¬takes(Y, Z) ∨ ¬class(Z) ∨ student(Y)) ∧ resident(john) ∧
takes(mark, 3342) ∧
class(3342) ∧
¬student(john)
15
Resolution
(¬resident(X) ∨ student(X)) ∧
(¬takes(Y, Z) ∨ ¬class(Z) ∨ student(Y)) ∧ resident(john) ∧
takes(mark, 3342) ∧
class(3342) ∧
¬student(john)
§ student(X) and student(john) unify: X = john
¬resident(john) ∧
(¬takes(Y, Z) ∨ ¬class(Z) ∨ student(Y)) ∧ resident(john) ∧
takes(mark, 3342) ∧
class(3342)
16
Resolution
¬resident(john) ∧
(¬takes(Y, Z) ∨ ¬class(Z) ∨ student(Y)) ∧ resident(john) ∧
takes(mark, 3342) ∧
class(3342)
§ Resolution gives: (◻) ∧
(¬takes(Y, Z) ∨ ¬class(Z) ∨ student(Y)) ∧ takes(mark, 3342) ∧
class(3342)
§ The empty clause (◻) is not satisfiable
§ We obtained a contradiction showing that student(john) is provable from the given axioms
17
Resolution
?- student(matthew).
false.
§ Resolution:
(¬resident(X) ∨ student(X)) ∧
(¬takes(Y, Z) ∨ ¬class(Z) ∨ student(Y)) ∧ resident(john) ∧
takes(mark, 3342) ∧
class(3342) ∧
¬student(matthew)
¬resident(matthew) ∧
(¬takes(Y, Z) ∨ ¬class(Z) ∨ student(Y)) ∧
resident(john) ∧ takes(mark, 3342) ∧ class(3342)
18
Resolution
¬resident(matthew) ∧ (¬takes(Y, 3342) ∨ student(Y)) ∧
resident(john) ∧ takes(mark, 3342)
¬resident(matthew) ∧ student(mark) ∧
resident(john)
§ cannot obtain a contradiction
19
Skolemization
§ So far we did not worry about existential quantifiers § What if we have:
∃X (takes(X, 3342) ∧ year(X, 2))
§ To get rid of the ∃, we introduce a constant a (as a notation
for the one which is assumed to exists by ∃) takes(a, 3342) ∧ year(a, 2)
20
Skolemization
§ What if we do this inside the scope of a universal quantifier ∀: ∀X (¬resident(X) ∨ ∃Y (address(X, Y)))
§ We get rid again of ∃ by choosing an address which depends on X, say ad(X):
∀X (¬resident(X) ∨ (address(X, ad(X))))
21
Skolemization
§ In Prolog takes(a, 3342).
year(a, 2).
address(X, ad(X)) :- resident(X). class_with_2nd(C) :- takes(X, C), year(X, 2). has_address(X) :- address(X, Y).
resident(b).
?- class_with_2nd(C).
C = 3342
?- has_address(X). X=b
22
Skolemization
?- takes(X, 3342). X=a
§ We cannot identify a 2nd-year student in 3342 by name ?- address(b, X).
X = ad(b).
§ We cannot find out the address of b
23
Horn Clauses Limitations
§ Horn clauses: only one non-negated term (head): ¬Q1 ∨¬Q2 ∨…∨¬Qk ∨P ≡ P←Q1 ∧Q2 ∧…∧Qk
P :- Q1, Q2,…,Qk.
§ If we have more than one non-negated term (two heads):
¬Q1 ∨¬Q2 ∨…∨¬Qk ∨P1 ∨P2 ≡P1 ∨P2 ←Q1 ∧Q2 ∧…∧Qk
§ then we have a disjunction in the left-hand side of ← (:-) P1 or P2 :- Q1, Q2,…,Qk.
§ which is not allowed in Prolog
24
Horn Clauses Limitations
§ If we have less than one (zero) non-negated terms:
¬Q1 ∨ ¬Q2 ∨…∨ ¬Qk
≡
false ← Q1 ∧ Q2 ∧…∧ Qk
§ then we have:
:- Q1, Q2,…,Qk.
§ which Prolog allows a query, not a rule
25
Horn Clauses Limitations
§ Example: two heads
“every living thing is an animal or a plant”
§ Clausal form:
animal(X) ∨ plant(X) ← living(X) ≡ animal(X) ∨ plant(X) ∨ ¬living(X)
§ In Prolog, the closest we can do is:
animal(X) :- living(X), not(plant(X)).
plant(X) :- living(X), not(animal(X)).
§ which is not the same, because, as we’ll see later, not indicates Prolog’s inability to prove, not falsity
26