程序代写代做代考 chain database C go COMP4418

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