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

8a_First_Order_Logic.dvi

COMP9414 First-Order Logic 1

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

COMP9414: Artificial Intelligence

Lecture 8a: First-Order Logic

Wayne Wobcke

e-mail:w. .au

UNSW ©W. Wobcke et al. 2019–2021

COMP9414 First-Order Logic 3

Syntax of First-Order Logic

� Constant symbols: a, b, . . . , Mary (objects)

� Variables: x, y, . . .

� Function symbols: f , mother of , sine, . . .

� Predicate symbols: Mother, likes, . . .

� Quantifiers: ∀ (universal); ∃ (existential)

UNSW ©W. Wobcke et al. 2019–2021

COMP9414 First-Order Logic 2

This Lecture

� First-Order Logic

◮ Syntax

◮ Semantics

� Automated Reasoning

◮ Conjunctive Normal Form

◮ First-order resolution and unification

◮ Soundness, completeness, decidability

� Applications

◮ Ontologies

◮ Reasoning About Action

UNSW ©W. Wobcke et al. 2019–2021

COMP9414 First-Order Logic 5

Converting English into First-Order Logic

� Everyone likes lying on the beach – ∀x likes lying on beach(x)

� Someone likes Fido – ∃x likes(x, Fido)

� No one likes Fido – ¬∃x likes(x, Fido) (or ∀x¬likes(x, Fido))

� Fido doesn’t like everyone – ¬∀x likes(Fido, x)

� All cats are mammals – ∀x(cat(x)→ mammal(x))

� Some mammals are carnivorous – ∃x(mammal(x)∧ carnivorous(x))

� Note: ∀xA(x)⇔¬∃x¬A(x), ∃xA(x)⇔¬∀x¬A(x)

UNSW ©W. Wobcke et al. 2019–2021

COMP9414 First-Order Logic 4

Language of First-Order Logic

� Terms: constants, variables, functions applied to terms (refer to

objects)

◮ e.g. a, f (a), mother of (Mary), . . .

� Atomic formulae: predicates applied to tuples of terms

◮ e.g. likes(Mary, mother of (Mary)), likes(x, a)

� Quantified formulae:

◮ e.g. ∀x likes(x, a), ∃x likes(x, mother of (y))

◮ here the second occurrences of x are bound by the quantifier (∀ in

the first case, ∃ in the second) and y in the second formula is free

UNSW ©W. Wobcke et al. 2019–2021

COMP9414 First-Order Logic 7

Existential Quantifiers

Some cats are immortal: ∃x(cat(x)∧¬mortal(x))

� ∃xP is (almost) equivalent to the disjunction of instantiations of P

� ∃x(cat(x)∧¬mortal(x))⇔

(cat(Alan)∧¬mortal(Alan))

∨ (cat(Bill)∧¬mortal(Bill))

∨ (cat(Colin)∧¬mortal(Colin))

∨ . . .

. . . only if every object (not only cat) in the domain has a name

UNSW ©W. Wobcke et al. 2019–2021

COMP9414 First-Order Logic 6

Universal Quantifiers

All men are mortal: ∀x(man(x)→ mortal(x))

� ∀xP is (almost) equivalent to the conjunction of instantiations of P

� ∀x(man(x)→ mortal(x))⇔

(man(Alan)→ mortal(Alan))

∧ (man(Bill)→ mortal(Bill))

∧ (man(Colin)→ mortal(Colin))

∧ . . .

. . . only if every object (not only man) in the domain has a name

UNSW ©W. Wobcke et al. 2019–2021

COMP9414 First-Order Logic 9

Defining Semantic Properties

Brothers are siblings

∀x∀y(brother(x, y)→ sibling(x, y))

“Sibling” is symmetric

∀x∀y(sibling(x, y)↔ sibling(y, x))

One’s mother is one’s female parent

∀x∀y(mother(x, y)↔ (female(x)∧parent(x, y))

A (first) cousin is a child of a parent’s sibling

∀x∀y(cousin(x, y)↔∃p∃s(parent(p, x)∧ sibling(p, s)∧parent(s, y)))

UNSW ©W. Wobcke et al. 2019–2021

COMP9414 First-Order Logic 8

Nested Quantifiers

The order of quantification is very important

� Everything likes everything – ∀x∀ylikes(x, y) (or ∀y∀x likes(x, y))

� Something likes something – ∃x∃ylikes(x, y) (or ∃y∃x likes(x, y))

� Everything likes something – ∀x∃ylikes(x, y)

� There is something liked by everything – ∃y∀x likes(x, y)

UNSW ©W. Wobcke et al. 2019–2021

COMP9414 First-Order Logic 11

Scope of Quantifiers

� The scope of a quantifier in a formula A is that subformula B of A of

which that quantifier is the main logical operator

� Variables belong to the innermost quantifier that mentions them

� Examples

◮ Q(x)→∀yP(x, y) – scope of ∀y is ∀yP(x, y)

◮ ∀zP(z)→¬Q(z) – scope of ∀z is ∀zP(z) but not Q(z)

◮ ∃x(P(x)→∀xP(x))

◮ ∀x(P(x)→ Q(x))→ (∀xP(x)→∀xQ(x))

UNSW ©W. Wobcke et al. 2019–2021

COMP9414 First-Order Logic 10

Scope Ambiguity

� Typical pattern for ∀ and ∃

◮ ∀x(type of (x)→ predicate(x))

◮ ∃x(type of (x)∧predicate(x))

� Every student took an exam

◮ ∀x(student(x)→∃y(exam(y)∧ took(x, y)))

◮ ∃y(exam(y)∧∀x(student(x)→ took(x, y)))

UNSW ©W. Wobcke et al. 2019–2021

COMP9414 First-Order Logic 13

Towards Resolution for First-Order Logic

� Based on resolution for Propositional Logic

� Extended syntax: allow variables and quantifiers

� Define “clausal form” for first-order logic formulae

� Eliminate quantifiers from clausal forms

� Adapt resolution procedure to cope with variables (unification)

UNSW ©W. Wobcke et al. 2019–2021

COMP9414 First-Order Logic 12

Semantics of First-Order Logic

� An interpretation is required to give semantics to first-order logic. An

interpretation is a non-empty “domain of discourse” (set of objects).

The truth of any formula depends on the interpretation.

� The interpretation defines, for each

constant symbol an object in the domain

function symbol a function from domain tuples to the domain

predicate symbol a relation over the domain (a set of tuples)

� Then by definition

universal quantifier ∀xP(x) is True iff P(a) is True for all

assignments of domain elements a to x

existential quantifier ∃xP(x) is True iff P(a) is True for at least one

assignment of domain element a to x

UNSW ©W. Wobcke et al. 2019–2021

COMP9414 First-Order Logic 15

Conversion to CNF – Continued

6. Skolemize (replace each existentially quantified variable by a new

term)

◮ ∃xP(x) becomes P(a0) using a Skolem constant a0 since ∃x

occurs at the outermost level

◮ ∀x∃yP(x, y) becomes P(x, f0(x)) using a Skolem function f0

since ∃y occurs within ∀x

7. The formula now has only universal quantifiers and all are at the left

of the formula: drop them

8. Use distribution laws to get CNF and then clausal form

UNSW ©W. Wobcke et al. 2019–2021

COMP9414 First-Order Logic 14

Conversion to Conjunctive Normal Form

1. Eliminate implications and bi-implications as in propositional case

2. Move negations inward using De Morgan’s laws

◮ plus rewriting ¬∀xP as ∃x¬P and ¬∃xP as ∀x¬P

3. Eliminate double negations

4. Rename bound variables if necessary so each only occurs once

◮ e.g. ∀xP(x)∨∃xQ(x) becomes ∀xP(x)∨∃yQ(y)

5. Use equivalences to move quantifiers to the left

◮ e.g. ∀xP(x)∧Q becomes ∀x(P(x)∧Q) where x is not in Q

◮ e.g. ∀xP(x)∧∃yQ(y) becomes ∀x∃y(P(x)∧Q(y))

UNSW ©W. Wobcke et al. 2019–2021

COMP9414 First-Order Logic 17

CNF: Example 2

¬∃x∀y∀z((P(y)∨Q(z))→ (P(x)∨Q(x)))

1. ¬∃x∀y∀z(¬(P(y)∨Q(z))∨P(x)∨Q(x))

2. ∀x¬∀y∀z(¬(P(y)∨Q(z))∨P(x)∨Q(x))

2. ∀x∃y¬∀z(¬(P(y)∨Q(z))∨P(x)∨Q(x))

2. ∀x∃y∃z¬(¬(P(y)∨Q(z))∨P(x)∨Q(x))

2. ∀x∃y∃z((P(y)∨Q(z))∧¬(P(x)∨Q(x)))

6. ∀x((P( f (x))∨Q(g(x)))∧¬P(x)∧¬Q(x))

7. (P( f (x))∨Q(g(x))∧¬P(x)∧¬Q(x)

8. {P( f (x))∨Q(g(x)), ¬P(x), ¬Q(x)}

UNSW ©W. Wobcke et al. 2019–2021

COMP9414 First-Order Logic 16

CNF: Example 1

∀x [∀yP(x, y)→¬∀y(Q(x, y)→ R(x, y))]

1. ∀x [¬∀yP(x, y)∨¬∀y(¬Q(x, y)∨R(x, y))]

2, 3. ∀x [∃y¬P(x, y)∨∃y(Q(x, y)∧¬R(x, y))]

4. ∀x [∃y¬P(x, y)∨∃z(Q(x, z)∧¬R(x, z))]

5. ∀x∃y∃z [¬P(x, y)∨ (Q(x, z)∧¬R(x, z))]

6. ∀x [¬P(x, f (x))∨ (Q(x, g(x))∧¬R(x, g(x)))]

7. ¬P(x, f (x))∨ (Q(x, g(x))∧¬R(x, g(x)))

8. (¬P(x, f (x))∨Q(x, g(x)))∧ (¬P(x, f (x))∨¬R(x, g(x)))

8. {¬P(x, f (x))∨Q(x, g(x)), ¬P(x, f (x))∨¬R(x, g(x))}

UNSW ©W. Wobcke et al. 2019–2021

COMP9414 First-Order Logic 19

Examples

� {P(x,a),P(b,c)} is not unifiable

� {P( f (x),y),P(a,w)} is not unifiable

� {P(x,c),P(b,c)} is unifiable by {x/b}

� {P( f (x),y),P( f (a),w)} is unifiable by

σ = {x/a,y/w}, τ = {x/a,y/a,w/a}, υ = {x/a,y/b,w/b}

Note that σ is an mgu and τ = σθ where θ = . . .?

� {P(x),P( f (x))} is not unifiable (c.f. occur check!)

UNSW ©W. Wobcke et al. 2019–2021

COMP9414 First-Order Logic 18

Unification

� A unifier of two atomic formulae is a substitution of terms for

variables that makes them identical

◮ Each variable has at most one associated term

◮ Substitutions are applied simultaneously

� Unifier of P(x, f (a), z) and P(z, z, u) : {x/ f (a), z/ f (a), u/ f (a)}

� Substitution σ1 is a more general unifier than a substitution σ2 if for

some substitution τ, σ2 = σ1τ (i.e. σ1 followed by τ)

� Theorem. If two atomic formulae are unifiable, they have a most

general unifier (mgu).

UNSW ©W. Wobcke et al. 2019–2021

COMP9414 First-Order Logic 21

Applying Resolution Refutation

� Negate query to be proven (resolution is a refutation system)

� Convert knowledge base and negated query into CNF

� Repeatedly apply resolution to clauses or copies of clauses until either

the empty clause (contradiction) is derived or no more clauses can be

derived (a copy of a clause is the clause with all variables renamed)

� If the empty clause is derived, answer ‘yes’ (query follows from

knowledge base), otherwise answer ‘no’ (query does not follow from

knowledge base) . . . and if there are an infinite number of clauses that

can be derived, don’t answer at all

UNSW ©W. Wobcke et al. 2019–2021

COMP9414 First-Order Logic 20

First-Order Resolution

A1∨·· ·∨Am∨B ¬B
′∨C1∨·· ·∨Cn

(A1∨·· ·∨Am∨C1∨·· ·∨Cn)θ






❧❧




✱✱

where B, B′ are positive literals, Ai, C j are literals, θ is an mgu of B and B

� 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 First-Order Logic 23

Resolution: Example 2

⊢ ∃x∀y∀z((P(y)∨Q(z))→ (P(x)∨Q(x)))

1. P( f (x))∨Q(g(x)) [¬ Query]

2. ¬P(x) [¬ Query]

3. ¬Q(x) [¬ Query]

4. ¬P(y) [Copy of 2]

5. Q(g(x)) [1, 4 Resolution {y/ f (x)}]

6. ¬Q(z) [Copy of 3]

7. � [5, 6 Resolution {z/g(x)}]

UNSW ©W. Wobcke et al. 2019–2021

COMP9414 First-Order Logic 22

Resolution: Example 1

⊢ ∃x(P(x)→∀xP(x))

CNF(¬∃x(P(x)→∀xP(x)))

1, 2. ∀x¬(¬P(x)∨∀xP(x))

2. ∀x(¬¬P(x)∧¬∀xP(x))

2, 3. ∀x(P(x)∧∃x¬P(x))

4. ∀x(P(x)∧∃y ¬P(y))

5. ∀x∃y(P(x)∧¬P(y))

6. ∀x(P(x)∧¬P( f (x)))

8. P(x), ¬P( f (x))

1. P(x) [¬ Query]

2. ¬P( f (y)) [Copy of ¬ Query]

3. � [1, 2 Resolution {x/ f (y)}]

UNSW ©W. Wobcke et al. 2019–2021

COMP9414 First-Order Logic 25

Examples

� S = { f (x,g(x)), f (h(y),g(h(z)))}

D0 = {x,h(y)} so σ1 = {x/h(y)}

S1 = { f (h(y),g(h(y))), f (h(y),g(h(z)))}

D1 = {y,z} so σ2 = {x/h(z),y/z}

S2 = { f (h(z),g(h(z))), f (h(z),g(h(z)))}

i.e. σ2 is an mgu

� S = { f (h(x),g(x)), f (g(x),h(x))} . . .?

UNSW ©W. Wobcke et al. 2019–2021

COMP9414 First-Order Logic 24

Unification Algorithm

� The disagreement set of S: Find the leftmost position at which not all

members E of S have the same symbol; the set of subexpressions of

each E in S that begin at this position is the disagreement set of S.

� Algorithm

1. S0 = S, σ0 = {}, i = 0

2. If Si is not a singleton find its disagreement set Di, otherwise

terminate with σi as the most general unifier

3. If Di contains a variable vi and term ti such that vi does not occur

in ti then

σi+1 = σi{vi/ti}, Si+1 = Si{vi/ti}

otherwise terminate as S is not unifiable

4. i = i+1; resume from step 2

UNSW ©W. Wobcke et al. 2019–2021

COMP9414 First-Order Logic 27

Logic and Prolog

� Prolog stands for programming in logic

� Prolog is based on resolution refutation in first-order logic, but with

additional imposed search control rules

� How does the implementation of Prolog relate to logic?

UNSW ©W. Wobcke et al. 2019–2021

COMP9414 First-Order Logic 26

Soundness and Completeness

For First-Order 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 not decidable, i.e. there is no algorithm

implementing resolution which when asked whether S ⊢ P, can

always answer ‘yes’ or ‘no’ (correctly)

UNSW ©W. Wobcke et al. 2019–2021

COMP9414 First-Order Logic 29

Undecidability of First-Order Logic

� Can we determine in general when this problem will arise? No!

� There is no general procedure

if (KB unsatisfiable)

return yes

else return no

� Resolution refutation is complete so if KB is unsatisfiable, the search

tree will contain the empty clause somewhere

� . . . 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) for problems of size n

UNSW ©W. Wobcke et al. 2019–2021

COMP9414 First-Order Logic 28

Undecidability of First-Order Logic

� KB = {P( f (x))→ P(x)}

� Q = P(a)?

� Obviously KB 6|= Q

� However, now try to show this using resolution

~P(f(x)) v P(x) ~P(a)

~P(f(a))

~P(f(f(a))

~P(f(f(f(a)))

x/a

x/f(a)

x/f(f(a))

UNSW ©W. Wobcke et al. 2019–2021

COMP9414 First-Order Logic 31

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 First-Order Logic 30

Horn Clauses

Idea: Use less expressive language

� Review

◮ literal – atomic formula or negation of atomic formula

◮ 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 First-Order Logic 33

Prolog Example

r(a,b). # facts

u(a).

v(b).

q(X) :- r(X,b), u(X). # rules

s(f(X)) :- v(X).

p(X) :- q(X), r(X,Z), s(f(Z)).

?- p(X). # query

X = a

Can give answer substitutions

UNSW ©W. Wobcke et al. 2019–2021

COMP9414 First-Order Logic 32

Prolog

� Horn clauses in First-Order Logic

� 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 First-Order Logic 35

Negation as Failure

� Prolog does not implement classical negation

◮ KB ⊢ ¬G if KB can prove ¬G

� Prolog not is known as negation as failure

◮ KB ⊢ not(G) if all attempts to prove G from KB fail

� Negation as failure is finite failure

UNSW ©W. Wobcke et al. 2019–2021

COMP9414 First-Order Logic 34

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 rule from KB for which
most general unifier of G,G′ is θ (try all in KB)

(if no such rule, undo unifications and try alternative rules)

Apply θ to the current goal set

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 First-Order Logic 37

Conclusion

� First-order logic can express objects, properties of objects and

relationships between objects, and allows quantification over

variables

� First-order logic is highly expressive

� Resolution refutation is sound and complete, but not decidable

� Prolog is more programming language than theorem prover

� Gödel’s incompleteness theorem

◮ Any first-order logic system with Peano’s axioms for arithmetic

cannot be both consistent and prove all true statements (where

statements are encoded using numbers)

UNSW ©W. Wobcke et al. 2019–2021

COMP9414 First-Order Logic 36

Soundness and Completeness Again

� Prolog including negation as failure is not sound, i.e. it does not

preserve truth

� Pure Prolog (without negation as failure) is not complete, i.e. it is

incapable of proving all consequences of any knowledge base (this is

because of the search order)

� Even pure Prolog is not decidable, i.e. the Prolog implementation of

resolution when asked whether KB ⊢ Q, can not always answer ‘yes’

or ‘no’ (correctly)

UNSW ©W. Wobcke et al. 2019–2021