COMP4418
⃝c UNSW, 2019
COMP4418: Knowledge Representation and Reasoning
Logic and Prolog
Maurice Pagnucco
School of Computer Science and Engineering University of New South Wales
NSW 2052, AUSTRALIA morri@cse.unsw.edu.au
COMP4418, Monday 30 September, 2019 Reasoning Under Uncertainty 1
Logic and Prolog
Prolog stands for programming in logic
How does the implementation of Prolog relate to logic?
Prolog is based on resolution theorem proving in first-order logic
In this lecture we will look at the relationship between automated reasoning in first-order logic and Prolog
References:
◮ Ivan Bratko, Prolog Programming for Artificial Intelligence,
Addison-Wesley, 2001. (Chapter 2)
COMP4418 ⃝c UNSW, 2019 Generated: 15 September 2019
COMP4418, Monday 30 September, 2019
Reasoning Under Uncertainty 2
Overview
Problems
Undecidability of first-order logic Horn Clauses
SLD Resolution
Prolog
Back Chaining
Forward Chaining
Negation as Failure
Conclusion
COMP4418
⃝c UNSW, 2019
Generated: 15 September 2019
COMP4418, Monday 30 September, 2019 Reasoning Under Uncertainty 3
Resolution — Problem 1
We have seen that the resolution rule is sound: If Γ ⊢ φ, then Γ |= φ
However, the resolution rule is not complete in general:
{¬P} |= ¬P ∨ ¬Q but cannot show this using resolution ({¬P} ⊢ ¬P∨¬Q)
Resolution is sound and complete when used as a refutation system though:
Γ ⊢ if and only if Γ |=
Therefore, resolution should be used as a refutation system as we
have done so far
COMP4418 ⃝c UNSW, 2019 Generated: 15 September 2019
COMP4418, Monday 30 September, 2019 Reasoning Under Uncertainty 4
Resolution — Problem 2
KB = {P(f(x) → P(x)}
Q=P(a)?
Obviously KB ̸|= Q
However, let us attempt to show this using resolution
COMP4418
⃝c UNSW, 2019
Generated: 15 September 2019
~P(f(x)) v P(x)
~P(a) x/a
~P(f(a)) x/f(a)
~P(f(f(a)) x/f(f(a))
~P(f(f(f(a))) …
COMP4418, Monday 30 September, 2019 Reasoning Under Uncertainty 5
Undecidability of First-Order Logic
Can we determine in general when this problem will arise?
Answer: no!
There is no general procedure
if (KB unsatisfiable) return Yes; Halt else return No; Halt
Resolution is refutation complete so if KB is unsatisfiable search tree will contain empty clause somewhere
Can find empty clause using breadth-first search (why?) but if the search tree does not contain the empty clause the search may go on forever
Even in the propositional case (which is decidable), complexity of resolution is O(2n)
COMP4418 ⃝c UNSW, 2019 Generated: 15 September 2019
COMP4418, Monday 30 September, 2019 Reasoning Under Uncertainty 6
Horn Clauses
Idea: use less expressive language
Review
◮ Literals — atomic sentence or its negation ◮ Clause — disjunction of literals
Horn Clause – at most one positive literal (e.g., ¬P∨Q, P∨¬Q∨R∨ S)
◮ Essentially represents a formula of the form A1 ∧ . . . ∧ An → C ◮ Thatis,ifA1 and…andAn,thenC
Definite (Positive) Clause – exactly one positive literal
Negative Clause – no positive literals
COMP4418 ⃝c UNSW, 2019 Generated: 15 September 2019
COMP4418, Monday 30 September, 2019 Reasoning Under Uncertainty 7
SLD Resolution — ⊢SLD
Selected literals Linear form Definite clauses resolution
SLD derivation of a clause C from a set of clauses KB is a sequence of clauses such that
1. First clause of sequence comes from KB
2. Each intermediate clause Ci is derived by resolving the previous
clause Ci−1 and a clause from KB 3. The last clause in the sequence is C
KB
ForsetofHornclausesKB:KB⊢ifandonlyifKB⊢SLD
COMP4418 ⃝c UNSW, 2019 Generated: 15 September 2019
C 1
C 2
…
C
COMP4418, Monday 30 September, 2019 Reasoning Under Uncertainty 8
Prolog
Horn clauses in first-order logic (facts and rules)
SLD resolution
Depth-first search strategy with backtracking
User control
◮ Ordering of predicates in Prolog database (facts and rules) ◮ Ordering of subgoals in body of a rule
◮ Cut (!) operator
◮ Negation as failure
That is, Prolog is a restricted form of first-order logic (Horn clauses) and puts more control of the theorem proving process into the hands of the programmer allowing them to use problem-specific knowledge to reduce search
COMP4418 ⃝c UNSW, 2019 Generated: 15 September 2019
COMP4418, Monday 30 September, 2019 Reasoning Under Uncertainty 9
Backward Chaining
(Brachman & Levesque) Show whether Horn knowledge base satisfiable Goal driven
Start with hypothesis and work backwards using rules in knowledge base to easily confirmed findings
Check satisfiabilty of set of Horn clauses:
prove(Q1 ∧…∧Qn) {
if n = 0 return yes % empty clause for each R ∈ KB do
if R = Q1 ← G1 ∧…∧Gm and prove(G1 ∧…∧Gm ∧ Q2 ∧…∧Qn)
then return yes return no }
Depth-first, left-right, backward chaining
Strategy applied by Prolog
COMP4418 ⃝c UNSW, 2019 Generated: 15 September 2019
COMP4418, Monday 30 September, 2019 Reasoning Under Uncertainty 10
Forward Chaining
(Brachman & Levesque) Determine whether Horn knowledge base entails q u e r y : K B |= Q
Data driven
1. if Q marked solved then return yes
2. if G ← G1 ∧ . . . ∧ Gm ∈ K B and G1 , . . . , Gm marked solved and G not marked solved
COMP4418
⃝c UNSW, 2019 Generated: 15 September 2019
then mark G solved; goto 1 else return no
COMP4418, Monday 30 September, 2019 Reasoning Under Uncertainty 11
Negation as Failure
Prolog does not implement classical negation
Prolognotisknownasnegationasfailure
not(G) :- G, !, fail. % If G succeeds return no not(G). % else return yes
KB⊢not(G)—cannotproveG
KB⊢¬G—canprove¬G
They are not the same
Negation as failure is finite failure
COMP4418 ⃝c UNSW, 2019 Generated: 15 September 2019
COMP4418, Monday 30 September, 2019 Reasoning Under Uncertainty 12
Conclusion
First-order logic is an expressive formal language and allows for powerful reasoning
Theorem proving is undecidable in general
Other options:
◮ Search heuristics (ordering of predicates, subgoals; depth-first search)
◮ Sacrifice expressivity (e.g., Horn clauses although still undecid- able in first-order case)
◮ User control (cut operator)
PrologisbasedonSLDresolutioninfirst-orderHornlogicandallows
programmer to use knowledge about domain to control search Blend of theory and pragmatics
COMP4418 ⃝c UNSW, 2019 Generated: 15 September 2019