COMP4418
⃝c UNSW, 2019
COMP4418: Knowledge Representation and Reasoning
Propositional Logic: Automating Reasoning
Maurice Pagnucco
School of Computer Science and Engineering University of New South Wales
NSW 2052, AUSTRALIA morri@cse.unsw.edu.au
COMP4418, Monday 16 September, 2019 Propositional Logic 1
Propositional Logic
Thus far we have considered propositional logic as a knowledge representation language
We can now write sentences in this language (syntax)
We can also determine the truth or falsity of these sentences
(semantics)
What remains is to reason; to draw new conclusions from what we know (proof theory) and to do so using a computer to automate the process
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 16 September, 2019 Propositional Logic 2
Overview
Normal Forms
Resolution
Refutation Systems
Correctness of resolution rule — soundness and completeness revisited
Conclusion
COMP4418 ⃝c UNSW, 2019 Generated: 15 September 2019
COMP4418, Monday 16 September, 2019 Propositional Logic 3
Motivation
COMP4418
⃝c UNSW, 2019
Generated: 15 September 2019
If either George or Herbert wins, then both Jack and Kenneth lose George wins
Therefore, Jack loses
(G∨H)→(¬J∧¬K) G
¬J
COMP4418, Monday 16 September, 2019 Propositional Logic 4
Normal Forms
A normal form is a “standardised” version of a formula Common normal forms:
COMP4418
⃝c UNSW, 2019 Generated: 15 September 2019
Negation Normal Form — negation symbols occur in front of propositional letters only (e.g., (P ∨ ¬Q) → (P ∧ (¬R ∨ S))
(A literal is a propositional letter or the negation of a propositional letter.)
Conjunctive Normal Form (CNF) — a conjunct of disjunctions (e.g., (P∨Q∨¬R)∧(¬S∨¬R))
Disjunctions of literals are known as clauses
Disjunctive Normal Form (DNF) — a disjunct of conjunctions (e.g., (P∧Q∧¬R)∨(¬S∧¬R))
COMP4418, Monday 16 September, 2019 Propositional Logic 5
Negation Normal Form
To simplify matters, let us suppose we are only dealing with formulae containing the connectives ¬, ∧, ∨
A(sub)formulaφ→ψisequivalentto¬φ∨ψ
A(sub)formulaφ↔ψisequivalenttoφ→ψandψ→φ
DeMorgan’s laws:
◮ ¬(φ∧ψ) ≡ ¬φ∨¬ψ
◮ ¬(φ∨ψ) ≡ ¬φ∧¬ψ
DoubleNegation:¬¬P≡P
To put a formula in negation normal form, repeatedly apply De
Morgan’s laws and double negation
For example, ¬(P∨(¬R∧P)) ≡ ¬P∧¬(¬R∧P) ≡ ¬P∧(R∨¬P)
COMP4418 ⃝c UNSW, 2019 Generated: 15 September 2019
COMP4418, Monday 16 September, 2019 Propositional Logic 6
Conjunctive Normal Form
Note the following distributive identities: (φ∧ψ)∨χ ≡ (φ∨χ)∧(ψ∨χ)
(φ∨ψ)∧χ ≡ (φ∧χ)∨(ψ∧χ)
To put a formula in conjunctive normal form (CNF) firstly put the formula into negation normal form and then repeatedly apply the identities above
For example, R → (P∧Q) ≡ (¬R∨P)∧(¬R∨Q)
COMP4418 ⃝c UNSW, 2019 Generated: 15 September 2019
COMP4418, Monday 16 September, 2019 Propositional Logic 7
Resolution Rule
Resolution Rule:
α∨β ¬β∨γ
❧✱ ❧✱ ❧✱ ❧✱ ❧✱ ❧✱
❧✱
α∨γ
Where β is a literal (i.e., a propositional letter or its negation)
COMP4418 ⃝c UNSW, 2019 Generated: 15 September 2019
COMP4418, Monday 16 September, 2019 Propositional Logic 8
Resolution Rule
¬α→β β→γ
❧✱ ❧✱ ❧✱ ❧✱ ❧✱ ❧✱
❧✱
¬α→γ
Resolution is essentially equivalent to the transitivity of material
implication
In fact, it is a form of the well known cut rule in logic
COMP4418 ⃝c UNSW, 2019 Generated: 15 September 2019
COMP4418, Monday 16 September, 2019
Propositional Logic 9
Applying Resolution
The resolution rule is sound
What does that mean?
How can we use the resolution rule?
◮ Convert premises into CNF
◮ Repeatedly apply resolution rule to the resultant clauses
◮ Each clause produced can be inferred from the original premises
◮ If you have a query sentence goal, it follows from the premises if and only if each of the clauses in CNF(goal) is produced by resolution
There is a better way …
COMP4418 ⃝c UNSW, 2019 Generated: 15 September 2019
COMP4418, Monday 16 September, 2019 Propositional Logic 10
Refutation Systems
Ifwewouldliketoproveasentenceφisatheorem(i.e.,⊢φ),westart with ¬φ and produce a contradiction
A “proof by contradiction”
Similarly, if we wish to prove ψ1, …, ψn ⊢ φ, start with ¬φ and
together with ψ1, …, ψn produce a contradiction
Resolution can be used to implement a refutation system
Repeatedly apply resolution rule until empty clause results
COMP4418 ⃝c UNSW, 2019 Generated: 15 September 2019
COMP4418, Monday 16 September, 2019 Propositional Logic 11
Applying Resolution
Negate conclusion (resolution is a refutation system)
Convert premises and negated conclusion into CNF (clausal form)
Repeatedly apply Resolution Rule, Double Negation
Ifemptyclauseresultsyouhaveacontradictionandcanconcludethat the conclusion follows from the premises
COMP4418 ⃝c UNSW, 2019 Generated: 15 September 2019
COMP4418, Monday 16 September, 2019 Propositional Logic 12
Resolution — Example 1
(G∨H)→(¬J∧¬K), G⊢¬J
CNF[(G ∨ H) → (¬J ∧ ¬K)] ≡ (¬G ∨ ¬J) ∧ (¬H ∨ ¬J) ∧ (¬G ∨ ¬K) ∧
(¬H∨¬K)
1. ¬G∨¬J
2. ¬H ∨ ¬J
3. ¬G∨¬K
4. ¬H ∨ ¬K
5. G [Premise]
6. ¬¬J [¬ Conclusion]
7. J 8. ¬G 9.
[6. Double Negation] [1, 7. Resolution]
COMP4418
⃝c UNSW, 2019
Generated: 15 September 2019
[Premise] [Premise]
[Premise] [Premise]
[5, 8. Resolution]
COMP4418, Monday 16 September, 2019
Propositional Logic
13
Resolution — Example 2
P→¬Q, ¬Q→R⊢P→R P→R≡¬P∨R
CNF[¬(¬P∨R)] ≡ {¬¬P, ¬R}
1. ¬P∨¬Q [Premise] 2. ¬¬Q∨R [Premise] 3. ¬¬P [¬ Conclusion]
4. ¬R 5. P 6. ¬Q 7. R 8.
[¬ Conclusion]
[3. Double Negation]
COMP4418
⃝c UNSW, 2019
Generated: 15 September 2019
[1, 5. Resolution] [2, 6. Resolution]
[4, 7. Resolution]
COMP4418, Monday 16 September, 2019 Propositional Logic
14
Resolution — Example 3
⊢ ((P∨Q)∧¬P) → Q
CNF[¬(((P∨Q)∧¬P) → Q)] ≡ (P∨Q)∧¬P∧¬Q
1. P ∨ Q 2. ¬P 3. ¬Q 4. Q
[¬ Conclusion] [¬ Conclusion]
5.
[¬ Conclusion] [1, 2. Resolution] [3, 4. Resolution]
COMP4418
⃝c UNSW, 2019
Generated: 15 September 2019
COMP4418, Monday 16 September, 2019 Propositional Logic 15
Soundness and Completeness — Recap
An inference procedure (and hence a logic) is sound if and only if it preserves truth
Inotherwords⊢issoundiffwheneverλ⊢ρ,thenλ|=ρ
A logic is complete if and only if it is capable of proving all truths
Inotherwords,wheneverλ|=ρ,thenλ⊢ρ
Decidability
A logic is decidable if and only if there is a mechanical procedure that, when asked λ ⊢ ρ, can eventually halt and answer “yes” or halt and answer “no”
Propositional logic is decidable
COMP4418 ⃝c UNSW, 2019 Generated: 15 September 2019
COMP4418, Monday 16 September, 2019 Propositional Logic 16
Heuristics in applying Resolution
Clause elimination — can disregard certain types of clauses
◮ Pure clauses: contain literal L where ¬L doesn’t appear elsewhere
◮ Tautologies: clauses containing both L and ¬L
◮ Subsumed clauses: another clause exists containing a subset of the literals
Ordering strategies
◮ Unit preference: resolve unit clauses (only one literal) first
Manyothers…
COMP4418 ⃝c UNSW, 2019 Generated: 15 September 2019
COMP4418, Monday 16 September, 2019 Propositional Logic 17
Conclusion
We have now investigated one knowledge representation and reasoning formalism
This means we can draw new conclusions from the knowledge we have; we can reason
Have enough to build a knowledge-based agent
However, propositional logic is a weak language; there are many
things we can’t express in it
It cannot be used to express knowledge about objects, their properties and the relationships that exist between objects
For this purpose we need a more expressive language: first-order logic
COMP4418 ⃝c UNSW, 2019 Generated: 15 September 2019