Proof Search in Minimal Logic - Artificial Intelligence and Symbolic Computation - page 23

Lemma 4. Let Q be a ∀∃∀ -prefix, {P ⇒ P r }∪SQ -sequents and ϕ a substitu-

tion. Then

n {P ⇒ P r }∪S ϕ

ϕ Q

is a -substitution such that

if and only if there is a clause ∀ x . G → P s in P such that the following holds.

Let z be the final universal variables in Q , x be new (“raised”) variables such

Q ∗

that X i z has the same type as x i ,let be Q with the existential variables

extended by x ,andlet ∗ indicate the substitution [ x 1 ,...,x n := X 1 z ,...,X n z ] .

Q ∗ , r s ∗ )=( Q ,ρ Q -substitution ϕ such that Then unif ( = ) and there is a

<n {P ⇒ G ∗ }∪S ρϕ ,and ρ ◦ ϕ ) ϕ =( Q ∃ .

Q ∗ , r s ∗ )=( Q ,ρ ϕ is a Q -substitu- Proof. “If” .Let unif ( = ), and assume that

N i P⇒ G ∗ ρϕ .Let

ϕ ρ ◦ ϕ ) Q ∃ .From unif ( Q ∗ , r

tion such that := ( =

s ∗ )=( Q ,ρ r ρ s ∗ ρ r ϕ s ∗ ρϕ .Then

)weknow = , hence =

ϕ (

z N G ∗ ρϕ

( ∀ x . G →P s )

x ρϕ )

u

P s ∗ ρϕ (i.e., derives P r ϕ )from Pϕ .

“Only if” . Assume ϕ is a Q -substitution such that ( P⇒P r ) ϕ ,sayby

( ∀ x . G →P s ) ϕ tN ( G ϕ )[ x := t ] ,with

u ∀ x . G → P s aclausein P , and with additional

assumptions from Pϕ in N .Then r ϕ =( s ϕ )[ x := t ]. Since we can assume that

the variables x are new and in particular not range variables of ϕ ,with

ϑ := ϕ ∪ [ x := t ]

we have r ϕ = s ϑ .Let z be the final universal variables in Q , x be new (“raised”)

Q ∗ be

variables such that X i z has the same type as x i ,let Q with the existential

variables extended by x , and for terms and formulas let ∗ indicate the substitu-

tion [ x 1 ,...,x n := X 1 z ,...,X n z ]. Moreover, let

ϑ ∗ := ϕ ∪ [ X 1 ,...,X n := λ z .t 1 ,...,λ z .t n ] .

r ϑ ∗ = r ϕ s ϑ s ∗ ϑ ∗ , i.e., ϑ ∗ is a solution to the unification problem

Then = =

Q ∗ and r s

. Hence by Lemma 2 unif (

Q ∗ , r s ∗ )=( Q ,ρ

given by = = )andthere

Q -substitution ϕ such that ϑ ∗ =( ρ ◦ ϕ ) Q ∃ , hence ρ ◦ ϕ )

is a ϕ =( Q ∃ .Also,

G ∗ ϑ ∗ = G ρϕ .

( G ϕ )[ x := t ]= G ϑ =

A state is a pair ( Q, S )with Q aprefixand S a finite set of Q -sequents. By

thetwolemmasjustprovedwehave state transitions

→ ε ( ( Q, {P ⇒ ∀ x . D → A}∪S ) Q∀ x , {P ∪ D ⇒ A}∪S )

→ ρ ( Q , {P ⇒ G ∗ }∪S ( Q, {P ⇒ P r }∪S ) ( ) ρ ) ,

where in the latter case there is a clause ∀ x . G → P s in P such that the following

holds. Let z be the final universal variables in Q , x be new (“raised”) variables

Q ∗ be such that X i z has the same type as x i ,let Q with the existential variables

extended by x ,andlet ∗ indicate the substitution [ x 1 ,...,x n := X 1 z ,...,X n z ],

Q ∗ , r s ∗ )=( Q ,ρ

and unif ( ).

Notice that by Lemma 1, if

=

P⇒P r is a Q -sequent (which means that

P→P r

P⇒ G ∗ ) Q -sequent. is a Q -goal), then ( ρ is a