COMP4418
⃝c UNSW, 2019
COMP4418: Knowledge Representation and Reasoning
First-Order Logic
Maurice Pagnucco
School of Computer Science and Engineering University of New South Wales
NSW 2052, AUSTRALIA morri@cse.unsw.edu.au
COMP4418, Monday 23 September, 2019 First-Order Logic 1
First-Order Logic
First-orderlogicfurnishesuswithamuchmoreexpressiveknowledge representation language than propositional logic
We can directly talk about objects, their properties, relations between them, etc. . . .
Here we discuss first-order logic and resolution
However, there is a price to pay for this expressiveness in terms of
decidability References:
◮ Ivan Bratko, Prolog Programming for Artificial Intelligence, Addison-Wesley, 2001. (Chapter 15)
◮ Stuart J. Russell and Peter Norvig, Artificial Intelligence: A Modern Approach, Prentice-Hall International, 1995. (Chapter 6)
COMP4418 ⃝c UNSW, 2019 Generated: 15 September 2019
COMP4418, Monday 23 September, 2019
First-Order Logic
2
Overview
Syntax of First-Order Logic
Semantics of First-Order Logic Conjunctive Normal Form
Unification
First-Order Resolution
Soundness and Completeness Decidability
Conclusion
COMP4418 ⃝c UNSW, 2019
Generated: 15 September 2019
COMP4418, Monday 23 September, 2019 First-Order Logic 3
Syntax of First-Order Logic
ConstantSymbols:a,b,…,Mary(objects)
Variables:x,y,…
FunctionSymbols: f,mother of,sine,…
PredicateSymbols:Mother,likes,…
Quantifiers: ∀ (universal); ∃ (existential)
Terms: constant, variable, functions applied to terms (refer to
objects)
Atomic Sentences: predicate applied to terms (state facts)
Ground (closed) term: a term with no variable symbols
COMP4418 ⃝c UNSW, 2019 Generated: 15 September 2019
COMP4418, Monday 23 September, 2019 First-Order Logic 4
Syntax of First-Order Logic
Sentence ::= AtomicSentence ∥ Sentence Connective Sentence
∥ Quantifier Variable Sentence ∥ ¬ Sentence ∥ ( Sentence )
AtomicSentence ::= Predicate ( Term∗ ) Term ::= Function ( Term∗ ) ∥ Constant Connective ::= → ∥ ∧ ∥ ∨ ∥ ↔ Quantifier ::= ∀ ∥ ∃
∥ Variable
Constant ::= a ∥ John ∥ …
Variable ::= x ∥ men ∥ …
Predicate ::= P ∥ Red ∥ Between ∥ … Function ::= f ∥ Father ∥ …
COMP4418 ⃝c UNSW, 2019
Generated: 15 September 2019
COMP4418, Monday 23 September, 2019 First-Order Logic 5
Converting English into First-Order Logic
Everyone likes lying on the beach — ∀x Beach(x)
Someone likes Fido — ∃x Likes(x, Fido)
No one likes Fido — ¬∃x Likes(x, Fido)
Fido doesn’t like everyone — ¬∀x Likes(Fido, x)
Allcatsaremammals—∀x(Cat(x)→Mammal(x))
Somemammalsarecarnivorous—∃x(Mammal(x)∧Carnivorous(x))
COMP4418 ⃝c UNSW, 2019 Generated: 15 September 2019
COMP4418, Monday 23 September, 2019 First-Order Logic 6
Nested Quantifiers
Note that the order of quantification is very important Everything likes everything — ∀x ∀y Likes(x, y)
Something likes something — ∃x ∃y Likes(x, y)
Everything likes something — ∀x ∃y Likes(x, y)
There is something liked by everything — ∃y ∀x Likes(x, y)
COMP4418 ⃝c UNSW, 2019 Generated: 15 September 2019
COMP4418, Monday 23 September, 2019 First-Order Logic 7
Scope of Quantifiers
The scope of a quantifier in a formula φ is that subformula ψ of φ of which that quantifier is the main logical operator
Variables belong to the innermost quantifier that mentions them
Examples:
◮ Q(x)→∀yP(x, y)—scopeof∀yisP(x, y)
◮ ∀zP(z)→¬Q(z)—scopeof∀zisP(z)butnotQ(z) ◮ ∃x(P(x) → ∀x P(x))
◮ ∀x(P(x) → Q(x)) → (∀x P(x) → ∀x Q(x))
COMP4418 ⃝c UNSW, 2019 Generated: 15 September 2019
COMP4418, Monday 23 September, 2019 First-Order Logic 8
Terminology
Free-variable occurrences in a formula —
◮ All variables in an atomic formula
◮ The free-variable occurrences in ¬φ are those in φ
◮ The free-variable occurrences in φ ⊕ ψ are those in φ and ψ for any connective ⊕
◮ The free-variable occurrences in ∀x Φ and ∃x Φ are those in Φ except for occurrences of x
Open formula — A formula in which free variables occur Closed formula — A formula with no free variables
Closed formulae are also known as sentences
COMP4418 ⃝c UNSW, 2019 Generated: 15 September 2019
COMP4418, Monday 23 September, 2019 First-Order Logic 9
Semantics of First-Order Logic
A world in which a sentence is true under a particular interpretation is known as a model of that sentence under the interpretation
Constant symbols an interpretation specifies which object in the world a constant refers to
Predicate symbols an interpretation specifies which relation in the model a predicate refers to
Function symbols an interpretation specifies which function in the model a function symbol refers to
Universal quantifier is true iff all all instances are true Existential quantifier is true iff one instance is true
COMP4418 ⃝c UNSW, 2019 Generated: 15 September 2019
COMP4418, Monday 23 September, 2019 First-Order Logic 10
Conversion into Conjunctive Normal Form
1. Eliminate implication
2. Move negation inwards (negation normal form)
3. Standardise variables
(∀x P(x)) ∨ (∃x Q(x)) becomes (∀x P(x)) ∨ (∃y Q(y))
φ→ψ≡¬φ∨ψ
¬(φ∧ψ) ≡ ¬φ∨¬ψ ¬(φ∨ψ) ≡ ¬φ∧¬ψ ¬ ∀x φ ≡ ∃x ¬φ
¬ ∃x φ ≡ ∀x ¬φ ¬¬φ≡φ
COMP4418 ⃝c UNSW, 2019 Generated: 15 September 2019
COMP4418, Monday 23 September, 2019 First-Order Logic 11
Conversion into Conjunctive Normal Form
4. Skolemise
∃x P(x) ⇒ P(a)
∀x∃y P(x, y) ⇒ ∀x P(x, f (x))
∀x∀y∃z P(x, y, z) ⇒ ∀x∀y P(x, y, f (x, y))
5. Drop universal quantifiers 6. Distribute ∧ over ∨
(φ∧ψ)∨χ ≡ (φ∨χ)∧(ψ∨χ) 7. Flatten nested conjunctions and disjunctions
(φ∧ψ)∧χ ≡ φ∧ψ∧χ;(φ∨ψ)∨χ ≡ φ∨ψ∨χ
(8. In proofs, rename variables in separate clauses — standardise apart)
COMP4418 ⃝c UNSW, 2019 Generated: 15 September 2019
COMP4418, Monday 23 September, 2019 First-Order Logic 12
CNF — Example 1
∀x[(∀y P(x, y)) → ¬∀y(Q(x, y) → R(x, y))]
1. ∀x[¬(∀y P(x, y)) ∨ ¬∀y(¬Q(x, y) ∨ R(x, y))]
2. ∀x[(∃y P(x, y)) ∨ ∃y(Q(x, y) ∧ ¬R(x, y))]
3. ∀x[(∃y ¬P(x, y)) ∨ ∃z(Q(x, z) ∧ ¬R(x, z))]
4. ∀x[¬P(x, f(x))∨(Q(x, g(x))∧¬R(x, g(x)))]
5. ¬P(x, f(x))∨(Q(x, g(x))∧¬R(x, g(x)))
6. (¬P(x, f(x))∨Q(x, g(x)))∧(¬P(x, f(x))∨¬R(x, g(x)))
8. ¬P(x, f(x))∨Q(x, g(x)) ¬P(y, f(y))∨¬R(y, g(y))
COMP4418 ⃝c UNSW, 2019 Generated: 15 September 2019
COMP4418, Monday 23 September, 2019 First-Order Logic 13
CNF — Example 2
¬∃x∀y∀z((P(y) ∨ Q(z)) → (P(x) ∨ Q(x)))
¬∃x∀y∀z(¬(P(y) ∨ Q(z)) ∨ (P(x) ∨ Q(x))) [Eliminate →] ∀x¬∀y∀z(¬(P(y) ∨ Q(z)) ∨ (P(x) ∨ Q(x))) [Move ¬ inwards] ∀x∃y¬∀z(¬(P(y) ∨ Q(z)) ∨ (P(x) ∨ Q(x))) [Move ¬ inwards] ∀x∃y∃z¬(¬(P(y) ∨ Q(z)) ∨ (P(x) ∨ Q(x))) [Move ¬ inwards] ∀x∃y∃z(¬¬(P(y) ∨ Q(z)) ∧ ¬(P(x) ∨ Q(x))) [Move ¬ inwards] ∀x∃y∃z((P(y) ∨ Q(z)) ∧ (¬P(x) ∧ ¬Q(x))) [Move ¬ inwards] ∀x((P( f (x)) ∨ Q((g(x))) ∧ (¬P(x) ∧ ¬Q(x))) [Skolemise]
(P( f (x)) ∨ Q((g(x))) ∧ ¬P(x) ∧ ¬Q(x) [Drop ∀]
COMP4418 ⃝c UNSW, 2019 Generated: 15 September 2019
COMP4418, Monday 23 September, 2019 First-Order Logic 14
Unification
Unification takes two atomic formulae and returns a substitution that makes them look the same
Example:
{x/a, y/z, w/f(b, c)}
Note:
1. Each variable has at most one associated expression
2. No variable with an associated expression occurs within any
associated expression
{x/g(y),y/f(x)}isnotasubstitution
Substitution σ that makes a set of expressions identical known as a unifier
Substitution σ1 is a more general unifier than a substitution σ2 if for some substitution τ, σ2 = σ1τ.
COMP4418 ⃝c UNSW, 2019 Generated: 15 September 2019
COMP4418, Monday 23 September, 2019 First-Order Logic
15
First-Order Resolution
Generalised Resolution Rule: For clauses χ∨Φ and ¬Ψ∨ζ
χ∨Φ ¬Ψ∨ζ
❧✱ ❧✱ ❧✱ ❧✱ ❧✱ ❧✱
❧✱
(χ ∨ ζ).θ
Where θ is a unifier for atomic formulae Φ and Ψ
χ∨ζisknownastheresolvent COMP4418 ⃝c UNSW, 2019
Generated: 15 September 2019
COMP4418, Monday 23 September, 2019 First-Order Logic
16
Resolution — Example 1
⊢ ∃x(P(x) → ∀xP(x)) CNF(¬∃x(P(x) → ∀xP(x)))
∀x¬(¬P(x) ∨ ∀x P(x)) [Drive ¬ inwards] ∀x(¬¬P(x) ∧ ¬∀x P(x)) [Drive ¬ inwards] ∀x(P(x) ∧ ∃x ¬P(x)) [Drive ¬ inwards] ∀x(P(x) ∧ ∃z ¬P(z)) [Standardise Variables] ∀x(P(x) ∧ ¬P( f (x))) [Skolemise]
P(x) ∧ ¬P( f (x)) [Drop ∀] 1. P(x) [¬ Conclusion]
2. ¬P( f (y)) [¬ Conclusion] 3. P(f(y)) [1. {x/f(y)}]
4. [2, 3. Resolution] COMP4418
⃝c UNSW, 2019
Generated: 15 September 2019
COMP4418, Monday 23 September, 2019
First-Order Logic
17
Resolution — Example 2
1. P( f (x)) ∨ Q(g(x)) [¬ Conclusion] 2. ¬P(y) [¬ Conclusion]
3. ¬Q(z) [¬ Conclusion]
4. P(f(a))∨Q(g(a)) [1. {x/a}]
5. ¬P(f(a))
6. ¬Q(g(a))
7. Q(g(a))
8. [6, 7. Resolution]
COMP4418
⃝c UNSW, 2019
Generated: 15 September 2019
[2. {y/f(a)}]
[3. {z/g(a)}] [4, 5. Resolution]
COMP4418, Monday 23 September, 2019
First-Order Logic
18
Resolution — Example 3
1. man(Marcus) [Premise]
2. Pompeian(Marcus) [Premise]
3. ¬Pompeian(x)∨Roman(x) [Premise]
4. ruler(Caesar) [Premise]
5. ¬Roman(y) ∨ loyaltyto(y, Caesar) ∨ hate(y, Caesar)
[Premise]
6. loyaltyto(z, f(z)) [Premise]
7. ¬man(w)∨¬ruler(u)∨¬tryassassinate(w, u)∨¬loyaltyto(w, u) [Premise]
8. tryassassinate(Marcus, Caesar) [Premise]
9. ¬hate(Marcus, Caesar) [¬ Conclusion]
10. ¬Roman(Marcus)∨loyaltyto(Marcus, Caesar)∨hate(Marcus, Caesar) [5.
{y/Marcus}]
11. ¬Roman(Marcus) ∨ loyaltyto(Marcus, Caesar) [9, 10. Resolution] COMP4418 ⃝c UNSW, 2019 Generated: 15 September 2019
COMP4418, Monday 23 September, 2019 First-Order Logic 19
Resolution — Example 3
12. ¬Pompeian(Marcus)∨Roman(Marcus) [3. {x/Marcus}]
13. loyaltyto(Marcus, Caesar)∨¬Pompeian(Marcus) [11, 12.
Resolution]
14. loyaltyto(Marcus, Caesar) [2, 13. Resolution]
15. ¬man(Marcus)∨ ¬ruler(Caesar)∨ ¬tryassassinate(Marcus, Caesar)∨ ¬loyaltyto(Marcus, Caesar) [7. {w/Marcus, u/Caesar}]
16. ¬man(Marcus)∨¬ruler(Caesar)∨¬tryassassinate(Marcus, Caesar) [14, 15. Resolution]
17. ¬ruler(Caesar)∨¬tryassassinate(Marcus, Caesar) [1, 16. Resolution]
18. ¬tryassassinate(Marcus, Caesar) [4, 17. Resolution] 19. [8, 18. Resolution]
COMP4418
⃝c UNSW, 2019 Generated: 15 September 2019
COMP4418, Monday 23 September, 2019 First-Order Logic
20
Soundness and Completeness
Resolution is
◮ sound(ifλ⊢ρ,thenλ|=ρ)
◮ complete(ifλ|=ρ,thenλ⊢ρ)
Decidability
First-order logic is not decidable How would you prove this?
COMP4418 ⃝c UNSW, 2019
Generated: 15 September 2019
COMP4418, Monday 23 September, 2019 First-Order Logic 21
Conclusion
First-order logic allows us to speak about objects, properties of objects and relationships between objects
It also allows quantification over variables
First-order logic is quite an expressive knowledge representation
language; much more so than propositional logic
However, we do need to add things like equality if we wish to be able to do things like counting
We have also traded expressiveness for decidability
How much of a problems is this?
Ifweadd(Peano)axiomsformathematics,thenweencounterGo ̈del’s famous incompleteness theorem (which is beyond the scope of this course)
COMP4418 ⃝c UNSW, 2019 Generated: 15 September 2019