4b_Automated_Reasoning.dvi
COMP9414 Automated Reasoning 1
This Lecture
� Proof systems
◮ Soundness, completeness, decidability
� Resolution and Refutation
� Horn clauses and SLD resolution
� Prolog
� Tableau method
UNSW ©W. Wobcke et al. 2019–2021
COMP9414: Artificial Intelligence
Lecture 4b: Automated Reasoning
Wayne Wobcke
e-mail:w. .au
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 Automated Reasoning 3
Mechanizing Proof
� A proof of a formula P from a set of premises S is a sequence of lines
in which any line in the proof is
1. An axiom of logic or premise from S, or
2. A formula deduced from previous lines of the proof using a rule
of inference
and the last line of the proof is the formula P
� Formally captures the notion of mathematical proof
� S proves P (S ⊢ P) if there is a proof of P from S;
alternatively, P follows from S
� Example: Natural Deduction proof
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 Automated Reasoning 2
Summary So Far
� Propositional Logic
◮ Syntax: Formal language built from ∧, ∨, ¬,→
◮ Semantics: Definition of truth table for every formula
◮ S |= P if whenever all formulae in S are True, P is True
� Proof System
◮ System of axioms and rules for deduction
◮ Enables computation of proofs of P from S
� Basic Questions
◮ Are the proofs that are computed always correct? (soundness)
◮ If S |= P, is there always a proof of P from S (completeness)
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 Automated Reasoning 5
Resolution
� Another type of proof system based on refutation
� Better suited to computer implementation than systems of axioms and
rules (can give correct ‘no’ answers)
� Decidable in the case of Propositional Logic
� Generalizes to First-Order Logic (see later in term)
� Needs all formulae to be converted to clausal form
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 Automated Reasoning 4
Soundness and Completeness
� A proof system is sound if (intuitively) it preserves truth
◮ Whenever S ⊢ P, if every formula in S is True, P is also True
◮ Whenever S ⊢ P, S |= P
◮ If you start with true assumptions, any conclusions must be true
� A proof system is complete if it is capable of proving all consequences
of any set of premises (including infinite sets)
◮ Whenever P is entailed by S, there is a proof of P from S
◮ Whenever S |= P, S ⊢ P
� A proof system is decidable if there is a mechanical procedure
(computer program) which when asked whether S ⊢ P, can always
answer ‘yes’ – or ‘no’ – correctly
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 Automated Reasoning 7
Conversion to Conjunctive Normal Form
� Eliminate↔ rewriting P↔ Q as (P→ Q)∧ (Q→ P)
� Eliminate→ rewriting P→ Q as ¬P∨Q
� Use De Morgan’s laws to push ¬ inwards (repeatedly)
◮ Rewrite ¬(P∧Q) as ¬P∨¬Q
◮ Rewrite ¬(P∨Q) as ¬P∧¬Q
� Eliminate double negations: rewrite ¬¬P as P
� Use the distributive laws to get CNF [or DNF] – if necessary
◮ Rewrite (P∧Q)∨R as (P∨R)∧ (Q∨R) [for CNF]
◮ Rewrite (P∨Q)∧R as (P∧R)∨ (Q∧R) [for DNF]
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 Automated Reasoning 6
Normal Forms
� A literal ℓ is a propositional variable or the negation of a propositional
variable (P or ¬P)
� A clause is a disjunction of literals ℓ1∨ ℓ2∨·· ·∨ ℓn
� Conjunctive Normal Form (CNF) — a conjunction of clauses, e.g.
(P∨Q∨¬R)∧ (¬S∨¬R) – or just one clause, e.g. P∨Q
� Disjunctive Normal Form (DNF) — a disjunction of conjunctions of
literals, e.g. (P∧Q∧¬R)∨ (¬S∧¬R) – or just one conjunction, e.g.
P∧Q
� Every Propositional Logic formula can be converted to CNF and DNF
� Every Propositional Logic formula is equivalent to its CNF and DNF
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 Automated Reasoning 9
Resolution Rule of Inference
A1∨·· ·∨Am∨B ¬B∨C1∨·· ·∨Cn
A1∨·· ·∨Am∨C1∨·· ·∨Cn
❧
❧
❧
❧
❧
❧
❧❧
✱
✱
✱
✱
✱
✱
✱✱
where B is a propositional variable and Ai and C j are literals
� B and ¬B are complementary literals
� A1∨·· ·∨Am∨C1∨·· ·∨Cn is the resolvent of the two clauses
� Special case: If no Ai and C j, resolvent is empty clause, denoted �
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 Automated Reasoning 8
Example Clausal Form
Clausal Form = set of clauses in the CNF
� ¬(P→ (Q∧R))
� ¬(¬P∨ (Q∧R))
� ¬¬P∧¬(Q∧R)
� ¬¬P∧ (¬Q∨¬R)
� P∧ (¬Q∨¬R)
� Clausal Form: {P, ¬Q∨¬R}
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 Automated Reasoning 11
Applying Resolution: Naive Method
� Convert knowledge base into clausal form
� Repeatedly apply resolution rule to the resulting clauses
� P follows from the knowledge base if and only if each clause in the
CNF of P can be derived using resolution from the clauses of the
knowledge base (or subsumption)
� Example
◮ {P→ Q,Q→ R} ⊢ P→ R
◮ Clauses ¬P∨Q, ¬Q∨R, show ¬P∨R
◮ Follows from one resolution step
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 Automated Reasoning 10
Resolution Rule: Key Idea
� Consider A1∨·· ·∨Am∨B and ¬B∨C1∨·· ·∨Cn
◮ Suppose both are True
◮ If B is True, ¬B is False and C1∨·· ·∨Cn is True
◮ If B is False, A1∨·· ·∨Am is True
◮ Hence A1∨·· ·∨Am∨C1∨·· ·∨Cn is True
Hence the resolution rule is sound
� Starting with true premises, any conclusion made using resolution
must be true
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 Automated Reasoning 13
Applying Resolution Refutation
� Negate query to be proven (resolution is a refutation system)
� Convert knowledge base and negated query into CNF
� Repeatedly apply resolution until either the empty clause (contradic-
tion) is derived or no more clauses can be derived
� If the empty clause is derived, answer ‘yes’ (query follows from
knowledge base), otherwise answer ‘no’ (query does not follow from
knowledge base)
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 Automated Reasoning 12
Refutation Systems
� To show that P follows from S (i.e. S ⊢ P) using refutation, start with
S and ¬P in clausal form and derive a contradiction using resolution
� A contradiction is the “empty clause” (a clause with no literals)
� The empty clause � is unsatisfiable (always False)
� So if the empty clause � is derived using resolution, the original set
of clauses is unsatisfiable (never all True together)
� That is, if we can derive � from the clausal forms of S and ¬P, these
clauses can never be all True together
� Hence whenever the clauses of S are all True, at least one clause from
¬P must be False, i.e. ¬P must be False and P must be True
� By definition, S |= P (so P can correctly be concluded from S)
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 Automated Reasoning 15
Resolution: Example 2
P→¬Q, ¬Q→ R ⊢ P→ R
Recall P→ R⇔¬P∨R
Clausal form of ¬(¬P∨R) is {P, ¬R}
1. ¬P∨¬Q [Premise]
2. Q∨R [Premise]
3. P [¬ Query]
4. ¬R [¬ Query]
5. ¬Q [1, 3 Resolution]
6. R [2, 5 Resolution]
7. � [4, 6 Resolution]
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 Automated Reasoning 14
Resolution: Example 1
(G∨H)→ (¬J∧¬K), G ⊢ ¬J
Clausal form of (G∨H)→ (¬J∧¬K) is
{¬G∨¬J, ¬H ∨¬J, ¬G∨¬K, ¬H ∨¬K}
1. ¬G∨¬J [Premise]
2. ¬H ∨¬J [Premise]
3. ¬G∨¬K [Premise]
4. ¬H ∨¬K [Premise]
5. G [Premise]
6. J [¬ Query]
7. ¬G [1, 6 Resolution]
8. � [5, 7 Resolution]
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 Automated Reasoning 17
Soundness and Completeness Again
For Propositional Logic
� Resolution refutation is sound, i.e. it preserves truth (if a set of
premises are all true, any conclusion drawn from those premises must
also be true)
� Resolution refutation is complete, i.e. it is capable of proving all
consequences of any knowledge base (not shown here!)
� Resolution refutation is decidable, i.e. there is an algorithm
implementing resolution which when asked whether S ⊢ P, can
always answer ‘yes’ or ‘no’ (correctly)
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 Automated Reasoning 16
Resolution: Example 3
⊢ ((P∨Q)∧¬P)→ Q
Clausal form of ¬(((P∨Q)∧¬P)→ Q) is {P∨Q, ¬P, ¬Q}
1. P∨Q [¬ Query]
2. ¬P [¬ Query]
3. ¬Q [¬ Query]
4. Q [1, 2 Resolution]
5. � [3, 4 Resolution]
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 Automated Reasoning 19
Horn Clauses
Idea: Use less expressive language
� Review
◮ literal – proposition variable or negation of proposition variable
◮ clause – disjunction of literals
� Definite Clause – exactly one positive literal
◮ e.g. B∨¬A1∨ . . .∨¬An, i.e. B← A1∧ . . .∧An
� Negative Clause – no positive literals
◮ e.g. ¬Q1∨¬Q2 (negation of a query)
� Horn Clause – clause with at most one positive literal
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 Automated Reasoning 18
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 is a subset of the literals
� Ordering strategies
◮ Resolve unit clauses (only one literal) first
◮ Start with query clauses
◮ Aim to shorten clauses
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 Automated Reasoning 21
Prolog
� Horn clauses in First-Order Logic (see later in term)
� SLD resolution
� Depth-first search strategy with backtracking
� User control
◮ Ordering of clauses in Prolog database (facts and rules)
◮ Ordering of subgoals in body of a rule
� Prolog is a programming language based on resolution refutation
relying on the programmer to exploit search control rules
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 Automated Reasoning 20
SLD Resolution – ⊢SLD
� Selected literals Linear form Definite clauses resolution
� SLD refutation of a clause C from a set of clauses KB is a sequence
1. First clause of sequence is C
2. Each intermediate clause Ci is derived by resolving the previous
clause Ci−1 and a copy of a clause from KB
3. The last clause in the sequence is �
C1
…
C2
C
KB
� Theorem. For a definite KB and negative clause query Q: KB∪Q ⊢�
if and only if KB∪Q ⊢SLD �
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 Automated Reasoning 23
Prolog Interpreter
Input: A query Q and a logic program KB
Output: ‘yes’ if Q follows from KB, ‘no’ otherwise
Initialize current goal set to {Q}
while the current goal set is not empty do
Choose G from the current goal set; (first in goal set)
Choose a copy G′ :- B1, . . . ,Bn of a clause from KB (try all in KB)
(if no such rule, try alternative rules)
Replace G by B1, . . . ,Bn in current goal set
if current goal set is empty
output ‘yes’
else output ‘no’
� Depth-first, left-right with backtracking
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 Automated Reasoning 22
Prolog Example
r. # facts
u.
v.
q :- r, u. # rules
s :- v.
p :- q, r, s.
?- p. # query
yes
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 Automated Reasoning 25
Tableau Method Example
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 Automated Reasoning 24
Tableau Method
UNSW ©W. Wobcke et al. 2019–2021
COMP9414 Automated Reasoning 26
Conclusion: Propositional Logic
� Propositions built from ∧, ∨, ¬,→
� Sound, complete and decidable proof systems (inference procedures)
◮ Natural deduction
◮ Resolution refutation
◮ Prolog for special case of definite clauses
◮ Tableau method
� Limited expressive power
◮ Cannot express ontologies, e.g. AfPak Ontology
� First-Order Logic can express knowledge about objects, properties
and relationships between objects
UNSW ©W. Wobcke et al. 2019–2021