(First Order Predicate Logic)

Equivalence Laws In addition to equivalence laws in propositional logic, ... sake of simplicity as ... A term in predicate logic is either a constant,...

0 downloads 197 Views 199KB Size
Resolution Refutation in FOL (First Order Predicate Logic)

Lecture 5

Resolution in Predicate Logic 

Resolution method is used to test unsatisfiability of a set S of clauses in Predicate Logic. – It is an extension propositional logic.





of

resolution

method

for

The resolution principle basically checks whether empty clause is contained or derived from S. A clause is a closed formula of the form (∀x1) … (∀xn) (L1V …V Lm), – where Lk ,(1 ≤ k ≤ m) is a literal and xj, (1 ≤ j ≤ n) are all the variables occurring in L1, …, Lm.

Cont… 





Unsatisfiability of a FOL formula is ensured if there exit no interpretation under which it is true. In FOL, there are infinite number of domains and consequently infinite number of interpretations of a formula. Therefore, unlike propositional logic, – it is not possible to verify a validity and inconsistency / unsatisfiablity of a formula by evaluating it under all possible interpretations.



Hence there is a need of the formalism for verifying inconsistency and validity in FOL.

Prenex Normal Form 



In FOL, there is also a third type of normal form called Prenex Normal Form along with CNF and DNF. A closed formula α of FOL is said to be in Prenex Normal Form (PNF) iff – α is represented as (q1x1) … (qnxn)(M), where, qk , (1 ≤ k ≤ n ) is either ∀ or ∃ quant and M is a formula free from quantifiers. – A list of quantifiers (q1x1) … (qnxn) is called prefix and M is called the matrix of a formula α.

Transformation of Formula into Prenex Normal Form (PNF) 



If α and β are formulae of FOL, then they are logically equivalent iff if I[α] = I[β], ∀ I (interpretations). We use the following conventions: – α [x] –α –Q

 a formula α, that contains a variable x.  a formula without a variable x.  Quantifier (∀ or ∃ ).

Equivalence Laws 

In addition to equivalence laws in propositional logic, – following pairs of logically equivalent formulae (called equivalence laws) are available in FOL. 1. 2. 3. 4. 5.

(q x) α [x] V β α V (q x) β [x] (q x) α [x] Λ β α Λ (q x) β [x] ~ ((∀ ∀x) α [x])

≅ ≅ ≅ ≅ ≅

(q x) (α α [x] V β ) (q x) (α α V β [x]) (q x) (α α [x] Λ β ) (q x) (α α Λ β [x]) (∃ ∃x) (~α α [x])

6.

~ ((∃ ∃x) α [x])



(∀ ∀x) (~ α [x])

Cont… 

  

Equivalence laws (1) to (4) are obviously true because any formula that does not contain x can be brought into the scope of the quantifier q on x. Equivalence laws (5) and (6) are also not difficult to prove. Let us prove equivalence law (5). Equivalence law (6) can be similarly proved.

Equivalence law (5) Prove ~ ((∀x) α [x])



(∃x) (~α [x])

Proof:  





Let I be any interpretation over a domain D. We have to prove that I[~ ((∀x) α [x])] = T iff I[(∃x) (~α [x])] = T . Assume that if I[~ ((∀x) α [x])] = T, then prove that I[(∃x) (~α [x])] = T . I[ ~((∀x) α[x])] = T ⇒

~ I[((∀x) α [x])] = T

Proof Cont… ⇒I[((∀x) α [x])] = F ⇒I[α [c]] = F, for some constant c ∈ D. ⇒~I[α [c]] = T ⇒I[~ α [c]] = T  According to the definition of interpretation, we get I[(∃x) (~α [x])] = T  Hence the result. Converse, if I[(∃x) (~α [x])] = T, then I[~ ((∀x) α [x])] = T can similarly be proved.

Equivalence Laws - Cont… 

There are few more equivalence laws: 7. 8.



(∀ ∀x) α [x] Λ (∀ ∀x) β [x] ≅ (∀ ∀x) (α α [x] Λ β [x] ) (∃ ∃x) α [x] V (∃ ∃x) β [x] ≅ (∃ ∃x) (α α [x] V β [x])

Quantifiers ∀ and ∃ can distribute over Λ and V respectively, but cannot distribute over V and Λ. i. ii.

(∀x) α [x] V (∀x) β [x] ≠ (∀x) (α [x] V β [x] ) (∃x) α [x] Λ (∃x) β [x] ≠ (∃x) (α [x] Λ β [x])

Cont.. Show through an example that (∀x) α[x] V (∀x) β[x] and (∀x) (α[x] V β[x] ) are not equivalent. Example: Consider α : (∀x) P(x) V (∀x) Q(x) and an interpretation I as follows.



I



D = {1, 2} I[P(1)] = T, I[P(2)] = F I[Q(1)] = F, I[Q(2)] = T

We can easily show that α is false under interpretation I whereas a formula (∀x) (P(x) V Q(x)) is true under I.

Renaming Bound Variables 

For the following cases, we have to do something special. – (∀x) α [x] V (∀x) β [x] ≠ (∀x) (α [x] V β [x] ) – (∃x) α [x] Λ (∃x) β [x] ≠ (∃x) (α [x] Λ β [x])

 

Every bound variable x in β[x] can be renamed by y such that y ∉ {α, β} . Therefore, for the first case – (∀x) α [x] V (∀x) β [x]

≅ ≅

(∀x) α [x] V (∀y) β [y] , (∀x) (∀y) (α [x] V β [y] ) (using laws 1 and 2)

Cont… 

Thus by renaming all occurrence of x by y ∉ {α, β} in a formula β, we get, two more equivalence laws as follows: 9. (∀ ∀x) α [x] V (∀ ∀x) β [x] ≅ (∀ ∀x) (∀ ∀y) (α α [x] V β [y] ) 10. (∃ ∃x) α [x] Λ (∃ ∃x) β [x] ≅ (∃ ∃x) (∃ ∃y) (α α [x] Λ β [y] )



To transform a formula into PNF, ten equivalence laws discussed above are used.

Skolemisation (Standard Form) 

 



PNF of a formula is further transformed into special form called Skolemisation or Standard Form. This form is used in resolution of clauses. The process of eliminating existential quantifiers and replacing the corresponding variable by a constant or a function is called skolemisation. A constant or a function is called skolem constant or function.

Convertion of PNF to its Standard Form 

Scan prefix (q1x1) … (qnxn) of PNF {(q1x1) … (qnxn)(M)} of a formula from left to right. – If q1 is the first existential quantifier then choose a new constant c, different from the constants occurring in Matrix. – Replace all occurrence of x1 appearing in Matrix by c and delete (q1 x1) from the prefix to obtain new prefix and matrix. – If qr is an existential quantifier and q1….qr-1 are universal quantifiers appearing before qr , then choose a new (r-1) place function symbol 'f ' different from other function symbols appearing in Matrix.

Cont… – Replace all occurrence of xr in Matrix by f(x1,.. ,xr-1 ) and remove (qr xr ). – Repeat the process till all existential quantifiers are removed from matrix. 

Standard form of any formula α in FOL is of the form – (∀ ∀x1)… (∀ ∀xn) (C1 Λ… Λ Cm), where Ck ,(1≤ k ≤m) is formula in disjunctive normal form.



Since all the variables in prefix are universally quantified, we omit prefix part from the standard form for the sake of convenience and write standard form as – (C1 Λ… Λ Cm).

Example 

Obtain standard forms of the following formula. – (∃ ∃x) (∀ ∀y) (∀ ∀z) (∃ ∃u) ( ~ P(x, z) Λ ~ P(y, z) Λ Q(x, y, u) )

Solution: Since (∃x) is very first quantifier, replace x by any constant say, c. Therefore, – (∃x) (∀y) (∀z) (∃u) ( ~ P(x, z) Λ ~ P(y, z) Λ Q(x, y, u) )

≅ (∀y) (∀z) (∃u) ( ~ P(c, z) Λ ~ P(y, z) Λ Q(c, y, u))) ≅ (∀y) (∀z) ( ~ P(c, z) Λ ~ P(y, z) Λ Q(c, y, f (y, z)) ) { u = f (y, z), f is a skolem function} 

Hence the standard form is: – (∀ ∀y) (∀ ∀z) ( ~ P(c, z) Λ ~ P(y, z) Λ Q(c, y, f (y, z)) )

Definitions 

A literal is an atom or negation of an atom. – A literal prefixed with not (~) symbol is called a negative literal, otherwise it is called a positive literal.



A clause is a closed formula of the form – (∀ ∀x1) … (∀ ∀xn) (L1V … V Lm), where each Lk is a literal and x1,…,xn are variables occurring in L1, …, Lm.



Since all the variables in a clause are universally quantified, we omit them and write clause for the sake of simplicity as – (L1V … V Lm )



Example of a clause: – (∀ ∀x) (∀ ∀y) (∀ ∀z) ( P(x, z) V ~ Q(x, y) V ~ R(y, z) )

Definitions – Cont… 

Let α be any formula – β be its standard form represented as C1 Λ… ΛCm – S = { C1, … ,Cm } to be a set of clauses of β.



S is said to be unsatisfiable (inconsistent) iff there ∃ no interpretation that satisfies all the clauses of S simultaneously. – A formula α is unsatisfiable (inconsistent) iff its corresponding set S is unsatisfiable.



S is said to be satisfiable (consistent) iff each clause is consistent i.e., – ∃ an interpretation that satisfies all the clauses of S simultaneously. – Alternatively, an interpretation I models S iff I models each clause of S.

Cont… Lemma: If an interpretation I models α (i.e., α is consistent), then I need not model S. In other words, α is not logically equivalent to S. Example: Consider α : (∃x) P(x)  Standard form of α is P(c), where c is skolem constant.  Therefore, S = {P(c)}.  Consider the following interpretation. Clearly α is true under I but S is false . D = {1, 2}; I[c] = 1; I[P(1)] = F, I[P(2)] = T  Hence if α is consistent, then S need not be consistent.  Note that a formula may have more than one standard forms.

Resolution in Predicate Logic Resolution for the clauses containing no variables is very simple and is similar to prop logic.  It becomes complicated when clauses contain variables.  In such case, two complementary literals are resolved after proper substitutions so that both the literals have same arguments. Example: Consider two clauses C1 and C2 as follows: 

C1 C2

= =

P(x) V Q(x) ~ P(f(x)) V R(x)

Example – Cont… 

Substitute 'f(a)' for 'x' in C1 and 'a' for 'x' in C2 , where 'a' is a new constant from the domain, then C3 C4



= =

P(f(a)) V Q(f(a)) ~ P(f(a)) V R(a)

Resolvent C of C3 and C4 is C = [Q(f(a)) V R(a)] • Here C3 and C4 do not have variables. They are called ground instances of C1 and C2 .



In general, if we substitute 'f(x)' for 'x' in C1, then C'1



=

P(f(x)) V Q(f(x))

Resolvent C' of C'1 and C2 is C' = [Q(f(x)) V R(x)]



We notice that C is an instance of C' .

Substitution & Unification 

A substitution θ = {x1 / t1, …., xn / tn}, is a finite set of elements, – where each xk is a distinct variable and each tk is a term different from xk , ( 1 ≤ k ≤ n). – Each element xk / tk of a set θ is called a binding for xk .



 

A term in predicate logic is either a constant, a variable or n-place function symbol with t1, …, tn as arguments, where each ti (1 ≤ ti ≤ n) is a term. A ground term is one which is free from variables. A substitution θ is – a ground if t1, t2 ,…, tn are all ground terms. – a pure variable substitution if t1, t2 ,…, tn are all variables.



Let θ = {x1 / t1, …., xn / tn} be a substitution and F be any formula in predicate logic.

Cont… 

Let θ = {x1 / t1, …., xn / tn} be a substitution and F be any formula in predicate logic. – Formula Fθ is obtained by replacing all occurrence of the variable xk in F by the corresponding term tk . – Fθ is called an instance of F. – If Fθ is ground, then it is called ground instance of F.



Let θ = {x1 / t1,…, xn / tn} and σ = {y1 / s1,…, ym / sm} be two substitutions. Composition of θ and σ (denoted by θ ο σ) is obtained as follows: – θ ο σ = { x1/(t 1σ),..., xn /(tn σ), y1/s1, …., ym / sm } after deleting any binding xk / (tk σ) for which xk= tk σ and binding yj / sj for which yj ∈ {x1, …., xn}

Example 

Consider two substitutions θ and σ defined as follows: – θ ={x / f(y), y / z} and – σ = {x / a, y / b, z / y}.

Show that θ ο σ = {x / f(b), z / y}. Solution: 

θ οσ = = =  

{x / f(y), y / z} ο σ {x / (f(y) σ) , y / (z σ) , x / a, y / b, z / y } {x / f(b), y / y, x / a , y / b , z / y}

According to the definition, delete y / y, x / a and y / b from above set. Hence θ ο σ = {x / f(b), z / y}

Definition 

 

The substitution given by an empty set is called identity substitution and denoted by ε. It satisfies the condition F ε = F, ∀ formulae F. Let F1 and F2 be two formulae. F1 and F2 are variants of each other, if there exist substitutions θ and σ such that F1 = F2 θ and F2 = F1σ.

Example: Show that P(f(x, y), g(z), a) and P(f(y, x), g(u), a) are variant of each other. Solution:Consider two substitutions θ ={x / y, y / x, z / u} and σ = {y / x, x / y, u / z} Let F1 = P(f(x, y), g(z), a) and F2 = P(f(y, x), g(u), a) Then, F1 = F2 θ and F2 = F1σ, hence variant of each other.

Definitions – Cont…  

Let F be a formula and U be a set of variables occurring in F. A renaming substitution for F is made a pure variable substitution such as {x1 / y1 , …, xn / yn } if following conditions are satisfied. – {x1 , …, xn }⊆ U and yk (1 ≤ k ≤ n) are distinct – { U – {x1 , …, xn }} ∩ {y1 , …, yn } = Φ



If ∑ = {F1, …, Fn} is a finite set of formulae and θ is any substitution, then – ∑θ = {F1θ, …, Fnθ}.



A substitution θ is called a unifier for a set ∑ iff ∑θ is a singleton set i.e., – a set containing single element i.e., F1θ = ….= Fn θ.

Example Consider ∑ = {P(f(x), z), P(y, a)}. Find an unifier of ∑ , if it exist Solution:  Consider a substitution θ = {y / f(a) , x / a , z / a}. 

– ∑θ 

= =

{ P(f(a), a), P(f(a), a)} { P(f(a), a)}

Since ∑θ is a singleton set, therefore, – θ = {y / f(a) , x / a , z / a} is an unifier of ∑.





An unifier σ for a set ∑={ F1, …, Fn } is most general unifier (mgu), if for each unifier θ of ∑, there exists a substitution ν such that θ = σ ο ν. The most general unifier may not be unique.

Example – Cont… Consider ∑ = {P(f(x), z), P(y, a)}. Find mgu. Solution:  The most general unifier for ∑ is σ = {y/f(x),z/a}, because for any unifier, say, θ = {y/f(a), x/a, z/a}, ∃ a substitution ν = {x / a} such that θ = σ ο ν  Consider 

σον



= {y / f(x), z / a} ο {x / a} = {y/f(a), x/a, z/a} = θ

Hence θ = σ ο ν and therefore σ = {y/f(x), z/a} is mgu.

Disagreement Set 

Consider two formulae F1 = P(a) and F2 = P(x). – These are not identical. – The disagreement is that 'a' occurs in F1 but variable 'x' occurs in F2 .





In order to unify F1 and F2, find out the disagreement set and then try to eliminate it. In this case disagreement set is {a, x}.

Disagreement Set Procedure 

In general disagreement set of S is obtained as follows: – Locate the leftmost symbol position at which all the formulae of ∑ are different. – Extract those sub formulae from ∑ beginning at the position located above. – This set is called disagreement set of ∑ denoted by D( ∑ ) at the particular position located above.

Examples 

Find disagreement problems:

for

the

following

i. ∑ = {P(f(x), h(y), a), P(f(x), z, a) }, ii. ∑ = {P(x, f(y, z)), P(x, a), P(x, g(h(k(x)))) },

Solutions:  Disagreement sets are: i. D( ∑ ) = {h(y), z} ii. D( ∑ ) = {f(y, z), a, g(h(k(x))) }

Unification Algorithm   

For resolving two clauses, unify them by finding out mgu of these clauses. Unification algorithm is used to find mgu of a given set S. It is a iterative process. (Algorithm on next slide) – At each iteration, find disagreement Dk set of S. – Try to find 'x' and 't' in Dk such that 'x' is a variable that does not occur in term 't'. – This is called occurs check. – We say that a variable 'x' satisfies occurs check with respect to a term 't'.

Unification Algorithm – Cont…  

Initialize k = 0, σk = ε (identity substitution), Sk = Sσk If Sk is a singleton set then σk is mgu of S else find disagreement set of Sk and denote it by Dk . – If ∃ a variable 'x' and a term 't' in Dk such that 'x' does not occur in 't‘. • Compute σk+1 = σk ο {x / t}; • k = k+1; • Sk = Sk-1σk ;

– else S is not unifiable. 

Repeat the process

Example Apply unification algorithm and find mgu of a set S = {P(a, x, f(g(y))) , P(z, f(z), f(u)) }. Solution: 

 

σ0 = ε ; S0 = {P(a, x, f(g(y))) , P(z, f(z), f(u)) } – D0 = {a, z}, σ1 = {z / a };



S1 = Sσ1 = { P(a, x, f(g(y))), P(a, f(a), f(u)) } – D1 = {x, f(a)};



σ2 = σ1 ο {x / f(a) } = {z / a, x / f(a) },

S2 = S1σ2 = { P(a, f(a), f(g(y))), P(a, f(a), f(u)) } – D2 = {g(y), u}; σ3 = σ2 ο {u / g(y) }= {z / a, x / f(a), u / g(y) },



S3 = S2σ3 = {P(a, f(a), f(g(y))), P(a, f(a), f(g(y))) } – Since S3 is a singleton set, therefore, σ3 = {z / a, x / f(a), u / g(y) } is the mgu of S.

Logical Consequence in FOL A clause L is defined to be a logical consequence of a set of clauses S iff every interpretation I that satisfies S also satisfies L. Lemma: If S = {C1,...,Cn} is a set of clauses, then L is a logical consequence of S iff ( C1 Λ … Λ Cn → L ) is valid. Lemma: Alternatively, we define L to be a logical consequence of S iff 

~ ( C1 Λ … Λ Cn → L ) is unsatisfiable OR ~(~( C1 Λ …ΛCn ) V L) is unsatisfiable or inconsistent. OR C1 Λ …ΛCn Λ ~L is unsatisfiable or inconsistent.

Cont… Theorem: L is a logical consequence of S iff S ∪ { ~ L} = { C1, …, Cn , ~ L} is unsatisfiable. – A deduction of an empty clause from a set S of clauses is called a resolution refutation of S.

Theorem: (Soundness and completeness of resolution): There is a resolution refutation of S iff S is unsatisfiable (inconsistent). Theorem: L is a logical consequence of S iff there is a resolution refutation of S ∪ {~L}.

Procedure 

To show that L to be a logical consequence the of set of formulae {α1, …, αn }, follow the following steps: – Obtain a set S of all the clauses by converting each αk to its corresponding standard form and then to the clauses. – Show that a set S ∪ { ~ L} is unsatisfiable i.e., the set S ∪ { ~ L} contains either empty clause or empty clause can be derived in finite steps using resolution method. – If so, then report 'Yes' and conclude that L is a logical consequence of S and subsequently of formulae α1, …, αn otherwise report 'No'.

Example Consider the following set of formulae: α : (∀ ∀x) (P(x) → (Q(x) Λ R(x))) β : (∃ ∃x) (P(x) Λ U(x)) Show that L = (∃x) (U(x) Λ R(x)) is a logical consequence of α and β. Solution: Convert α and β to its corresponding clauses by generating their standard forms.  Standard form of α :(∀x) (~ P(x) V (Q(x) Λ R(x))) is (∀x) ((~ P(x) V Q(x)) Λ (~ P(x) V R(x)))  Clauses of α are ~ P(x) V Q(x) and ~ P(x) V R(x)  Similarly the clauses of β are P(a) and U(a), where ‘a’ is a skolem constant.  Then, – S = { ~ P(x) V Q(x) , ~ P(x) V R(x), P(a), U(a) } 

Example – Cont… 

Negation of a goal L is:

~ ((∃x) (U(x) Λ R(x))) ≅ (∀x) (~ U(x) V ~ R(x) )  Clause of ~ L is ~ U(x) V ~ R(x) 

Therefore, set S ∪ { ~ L} is {~ P(x) V Q(x), ~ P(x) V R(x), P(a), U(a), ~ U(x) V ~ R(x) }



Clauses of set S ∪ { ~ L} are: ~ P(x) V Q(x) ~ P(x) V R(x) P(a) U(a) ~ U(x) V ~ R(x)



Now resolve the clauses to get empty clause.

Resolution Tree 



Inverted tree (resolution tree) is given below whose root is deduced as (empty clause) by resolving clauses in a set S ∪ { ~ L}. Hence L is a logical consequence of α and β . U(a)

~ U(x) V ~ R(x) {x / a} ~ R(a)

~ P(x) V R(x) {x / a} ~ P(a)

P(a)

Remarks 

If the choice of clauses to resolve at each step is made in a systematic way, then resolution algorithm will find a contradiction if one exists.



There exist various strategies for making the right choice that can speed up the process considerably.

Useful Tips 

Initially choose a clause from the negated goal clauses as one of the parents to be resolved – This corresponds to intuition that the contradiction we are looking for must be because of the formula we are trying to prove.

  

Choose a resolvent and some existing clause if both contain complementary literals. If such clauses do not exists, then resolve any pairs of clauses containing complementary literals. Whenever possible, resolve with the clauses with single literal. – Such resolution generate new clauses with fewer literals than the larger of their parent clauses and thus probably algorithm terminates faster.

Subsumption 



During resolution, irrelevant and redundant clauses in S are generated which may not affect the unsatisfiability of S if removed. Such clauses are of the following types. – If the set contains tautologies (which are always true) and if S is unsatisfiable, then the set obtained after removing tautologies from S will still be unsatisfiable. – Another type of clauses which could be deleted are the subsumed clauses whenever possible.

Subsumption Definition: A clause C subsumes a clause D iff ∃ a substitution σ such that Cσ ⊆ D.  Here D is called subsumed clause. Example: Let C = P(x) and D = P(a) V Q(a) be two clauses. Show that C subsumes D. Solution:  Consider a substitution σ = {x /a}.  Since Cσ = P(a) ⊆ D,  So C subsumes D.

Cont…  

 

Let C and D be two clauses. Consider σ = {x1 / a1,…, xn / an } to be any substitution such that xk’s are variables in D and ak’s are new distinct constants not occurring in C and D. Assume that D = L1V …V Lm , Then Dσ = L1σ V …V Lmσ and ~ Dσ = ~ L1σ Λ …Λ ~ Lmσ

Subsumption Algorithm Input: Given two clauses C and D Output: Whether C subsumes D or not Method:  Let W = {~L1σ , …~Lmσ}; k = 0 ; U0 = C ; progress = true;  While (progress = true) and (empty clause ∉ Ck ) do { if ∃ a literal M in Uk such that M = Ljσ with appropriate substitution then { k = k + 1; Uk = Resolvent (Uk-1, a clause from W with appropriate substitution}; else set progress = false } {end of while}

If (progress = false) then report that C does not subsume D else C subsumes D; Stop



Example Let C = ~ P(x) V Q(g(x), a) and D = ~ P(h(y)) V Q(g(h(y)), a) V ~ P(z) be two clauses. Show whether C subsumes D or not. Solution: Consider a substitution σ = {y / b, z / c} such that y, z ∈ D and b, c ∉ D. Dσ = ~ P(h(b)) V Q(g(h(b)), a) V ~ P(c) and ~ Dσ = P(h(b)) Λ ~ Q(g(h(b)), a) Λ P(c) Procedure:  Let W = { P(h(b)), ~ Q(g(h(b)), a), P(c) }; progress = true; and U0 = C = {~ P(x) V Q(g(x), a) }

Example – Cont… 

Since progress = true and C0 does not contain empty clause, – compute U1 by resolving P(h(b)) and ~ P(x) with binding {x / h(b)}.



U1 = {Q(g(h(b)), a)} Again progress = true and C1 does not contain empty clause, – compute U2 by resolving Q(g(h(b)), a) and ~ Q(g(h(b)), a).



U2 = { empty clause} Since U2 contains empty clause, – therefore, C subsumes D using subsumption algorithm.