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

Q -substitution ϕ , ( ρ ◦ ϕ )

with no unification pairs) such that for any Q ∃ is an

U -solution, and every U -solution can be obtained in this way. Since the empty

Q -substitution, substitution is a ρ Q ∃ is an U -solution, which is most general

in the sense stated.

unif ( Q, r = s ) denotes the result of the unification algorithm at U = Q r = s .

4ProofS ch

A Q -sequent has the form P⇒G ,where P is a list of Q -clauses and G is a

Q -goal.

We write M [ P ] to indicate that all assumption variables in the derivation M

concern clauses in P .

M G i
i

n S

Write for a set S of sequents if there are derivations [ P i ]inlong

such that # <n

normal form for all ( P i ⇒ G i ) ∈ S M i ≤ n .Let S mean

∃m<n m S

.
We now prove correctness and completeness of the proof search procedure:
correctness is the if-part of the two lemmata to follow, and completeness the
only-if-part.

Lemma 3. Let Q be a ∀∃∀ -prefix, {P ⇒ ∀ x . D → A}∪SQ -sequents with x , D

not both empty. Then we have for every substitution ϕ :

n {P ⇒ ∀ x . D → A}∪S ϕ

ϕ is a Q -substitution such that

if and only if

<n {P ∪ D ⇒ A}∪S ϕ ϕ is a Q∀ x -substitution such that .

<n {P ∪ D ⇒ A}∪S ϕ

Proof. “If” .Let ϕ be a Q∀ x -substitution and .Sowe

have

N Aϕ [

D ϕ ∪Pϕ ] .

Since ϕ is a Q∀ x -substitution, no variable in x can be free in Pϕ ,orfreein yϕ

for some y ∈ dom ( ϕ ). Hence

( ∀ x . D →A ) ϕ [

λ x λ u D ϕ N M Pϕ ]:=

is a correct derivation.
“Only if” .Let

n {P ⇒ ∀ x . D → A}∪S ϕ

ϕ be a Q -substitution and .This

means we have a derivation (in long normal form)

( ∀ x . D →A ) ϕ [

λ x λ u D ϕ .N Aϕ [ M Pϕ ]= D ϕ ∪Pϕ ] .

<n {P ∪ D ⇒ A}∪S ϕ

Now # N< # M , hence ,and ϕ clearly is a Q∀ x -

substitution.