程序代写代做代考 COMP4418

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