CS计算机代考程序代写 prolog database AI algorithm interpreter 4b_Automated_Reasoning.dvi

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]

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

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

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

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 �

…

� Theorem. For a definite KB and negative clause query Q: KB∪Q ⊢�

if and only if KB∪Q ⊢SLD �

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

COMP9414 Automated Reasoning 22

Prolog Example

r. # facts

q :- r, u. # rules

s :- v.

p :- q, r, s.

?- p. # query

yes

COMP9414 Automated Reasoning 25

Tableau Method Example

COMP9414 Automated Reasoning 24

Tableau Method

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

Related Posts