Baumgartner P. Theory Reasoning in Connection Calculi

Подождите немного. Документ загружается.

A.2 Proofs for Chapter 5 — Linearizing Completion 255

We will show that there is a (I

)

-derivation D

000

≺

Lin

, where I

I or I

is obtained from I by application of a mandatory transformation

rule from Lin. Then we deﬁne D

= D[D

000

]

λ,1,2

. By monotonicity of 

Lin

(Proposition 5.3.2) then it follows D

≺

Lin

D, which was to be shown.

Since L ∈ Punit(I) by deﬁnition

L → F ∈I. Let L

→ F be a new

variant. As in case 1, the mandatory Unit2 transformation rule can be applied

→ F and L

,... ,E

→ C ∈I, yielding

R =(K

,... ,E

→ C)σ,

where σ is the MGU for L

and L

used in that deduction step. Now either

a variant of R already is contained in I, and in this case deﬁne I

= I.

Otherwise deﬁne I

= I∪{R}.

As in case 1 there are ground substitutions δδ

, γ

and γ

such that

{|K

,... ,E

,C|}σδδ

= {|K

,... ,E

,C|}γ

= {|K

,... ,E

,C|}γ

By these equalities we can build the desired derivation

000

=(K

···E

======⇒

Rδδ

Cγ

)

with rule Rδδ

∈I

Note that D

000

and D

coincide in top and derived literals. Hence the

replacement as suggested above can be done. It remains to show D

000

≺

Lin

This proof is literally the same as the corresponding proof in case 1 above,

except that Lγ is to be replaced by K. This completes the proof for the case

6= ε.

Case 2.2: (D

= ε). It holds that n>0. Proof: Suppose, to the contrary that

n = 0. Then the refutation consists of a single inference step with the rule

→ F ∈I

. On the other hand from T

∈ Punit(I

) it follows T

→ F ∈I

But then I would be unsatisﬁable, since no interpretation can satisfy both,

and T

. By this we would arrive at a contradiction to the satisﬁability of

the underlying theory T where I stems from.

The given derivation D can be written more speciﬁcally as (n ≥ 0, cf.

Figure A.4) :

D =(Lγ

=⇒

→T

)γ

...T

==⇒T

n+1

===⇒T

n+2

)(∗)

where T

6= F,(L

→ T

)γ

∈I

is a ground instance of the rule L

→ T

∈I,

= Lγ and T

= T

Since L ∈ Punit(I) by deﬁnition

L → F ∈I. Let L

→ F be a new

variant, variable disjoint from the premise {|L

|} of the applied inference rule.

Since Lγ = L

and L

is a variant of L there is a ground substitution γ

with L

= L

. Since L

is a new variant, γ

can be supposed not to act

256 A. Appendix: Proofs

Lγ T

Used inference rule

Unit1

New top literal

Shorten

D :

Figure A.4. A case in the proof of Lemma 5.5.3 (ground case)

upon the variables of L

. Hence L

= L

. Since γ

is a uniﬁer for

and L

there is a most general uniﬁer σ for L

and L

and substitution δ

such that σδ = γ

(**). By the existence of this MGU, the mandatory

Unit1 transformation rule can be applied to L

→ T

∈Iand L

→ F ∈I.

The result is the new inference rule

R = T

→ F .

Now either a variant of R is already contained in I, and in this case deﬁne

= I. Otherwise deﬁne I

= I∪{R}.

Now let δ

be the restriction of γ

to the domain Var (T

) \ Var (L

). To-

gether with (**) it follows

σδδ

= T

(= T

= T

)(∗∗∗)

Thus with R ∈I

it follows T

∈ Punit((I

)

). By this fact we can cut oﬀ

the ﬁrst inference step in D, yielding

= D|

2,n+2

=(T

...T

==⇒T

n+1

===⇒T

n+2

) ,

which is a derivation from M ∪ Punit((I

)

) as desired.

It remains to prove D

≺

Lin

D. By deﬁnition of 

Lin

this is the same

as to show compl(D

) ≺

NMW

compl(D); for this proof the weights of the

involved inference rules can be neglected, since decreasingness follows alone

from properties of multiset orderings:

A.2 Proofs for Chapter 5 — Linearizing Completion 257

compl(D)={|0, compl(ε), compl(D

),... ,compl(D

n+1

)|}

= {|0, ∅, compl(D

),... ,compl(D

n+1

)|}



NMW

{|0, compl(D

),... ,compl(D

n+1

)|}

= compl(D

)

By concluding this ﬁnal case the lemma is proven.

Proposition 5.5.4. Let S be a Punit-normalizing transformation system

wrt. N , and let I be a completed inference system wrt. S. Whenever there

is a ground derivation D =(L ⇒

∗

,M∪Punit (I

)

) with D ∈N then there

is also a ground derivation D

=(K ⇒

∗

) with D

 D, D

∈N and

some K ∈ M ∪{L}.

Proof. By well-founded induction on derivations wrt. the well-founded deriva-

tion ordering associated to S.IfUsed(D)∩Punit(I

)=∅ then no literal from

Punit(I

) is used in D then D is also a derivation from M alone. Hence we

take D

= D.

Otherwise, by deﬁnition of Punit-normalizing transformation systems

there is a derivation D

=(L ⇒

∗

)

,M∪Punit ((I

)

) with D

≺ D, where

(1) I

= I or (2) I`

I∪{P → C} = I

by some mandatory transformation

rule from S.

In case 1 D

is also a I

-derivation of M ∪Punit(I

); now consider case 2:

since I is completed it holds by Deﬁnition 5.4.3 P → C ∈Ior (2.2) P → C is

-c-redundant in I. In case 2.1 I

= I and hence D

is also a I

-derivation

of M ∪ Punit(I

). In case 2.2 P → C is not of the form ¬A → F (such

rules are by deﬁnition never c-redundant). Hence Punit(I

)=Punit(I). If

no ground instance of P → C is used in D

then D

is also a I

-derivation

of M ∪ Punit(I

), otherwise by deﬁnition of c-redundancy there is a ground

derivation D

000

=(L ⇒

∗

,M∪Punit ((I)

)

) with D

000

≺ D

(note that this

is a I

-derivation). From D

000

≺ D

≺ D it follows by downward closure of

N also D

∈N and D

000

∈N. Thus, in any case there is a I

-derivation of

M ∪ Punit(I

) which is contained in N and which is strictly smaller wrt. 

than the given derivation.

Now apply the induction hypothesis to that derivation.

A.2.5 Section 5.6 — Completeness

Lemma 5.6.1 (Top Literal Lemma). Let I be a completed inference sys-

tem wrt. the transformation system Lin. Suppose there is a linear ground

derivation D =(L

⇒

∗

) with L

∈ M.LetT ∈ M such that

T ∈ Used(D). Then there is a linear ground derivation D

=(T ⇒

∗

Proof. Let the given derivation be

D =(L

==⇒L

...

k−1

===⇒L

===⇒

k+1

===⇒ ...L

n−1

====⇒L

)

(A.60)

258 A. Appendix: Proofs

where n>1 (otherwise the claim is trivial), k ∈{1 ...n} and R

is a

ground instance of R

= L

→ L

k+1

∈I, L

= L

, T = T

= M

and L

k+1

= L

k+1

We do induction on the top distance k of the inference step using T .

Induction start (k = 1): The ﬁrst inference step is L

===⇒

.By

swapping T and L

it can be replaced by the inference step T

====⇒

which yields the desired linear derivation.

Induction step (k − 1 → k): See Figure A.5 on Page 259 for illustration.

Suppose k>1, and as the induction hypothesis assume the claim to hold for

derivations with top distance strictly smaller than k. D then can be written

==⇒L

...

k−2

===⇒L

k−1

| {z }

z }| {

k−1

===⇒

k+1

===⇒ ...

n−1

====⇒L

| {z }

(A.61)

where n ≥ 3 and R

is a ground instance of R

= L

k−1

→ L

∈I,

k−1

= L

k−1

, M

k−1

= M

k−1

and L

= L

Without loss of generality suppose that R

is variable disjoint from R

Consequently, we may assume that the domains of γ

and γ

are disjoint, too.

Hence R

= R

and R

= R

. Together with L

= L

it follows that L

= L

. In other words, γ

is a uniﬁer.

Hence there is a MGU σ and a substitution δ such that γ

= σδ.Bythe

existence of this MGU, the Deduce transformation rule can be applied to R

and R

by unifying L

and L

with σ. The result is the inference rule R =

k−1

→ L

k+1

)σ. Since Deduce is a mandatory transformation

rule and I is completed (1) R ∈Ior (2) R is 

Lin

-c-redundant in I. In case

(1) the derivation D

in (A.61) can be replaced by the one step derivation

k−1

=======⇒

k−1

→L

k+1

)σδ

k+1

using Rδ. Since δ is a ground substitution Rδ ∈I

and the replacement

results in a I

derivation with same structure. Furthermore, its top distance

is k − 1. Hence we can apply the induction hypothesis to obtain the desired

derivation.

In case (2) things are more complicated. First consider the (I∪{R})

derivation

k−1

==========⇒

Rδ

k+1

Since R is 

Lin

-c-redundant in I there is a linear I

-derivation

=(T ⇒

∗

k−1

∪M

∪{L

k−1

}

k+1

) .

A.2 Proofs for Chapter 5 — Linearizing Completion 259

k−1

k+1

Replace:

k+1

k−1

Induction:

becomes top literal

R is deleted and

replaced by derivation

k−1

k+1

Deduce

Figure A.5. Illustration of proof of Lemma 5.6.1 (ground case).

260 A. Appendix: Proofs

Note that M

k−1

⊆ M. Now concatenate to D

= D

· D

and obtain a

linear derivation of the form

=(T ⇒

∗

,M∪{L

k−1

}

)

Next the applications of the literal {L

k−1

} in D

have to be eliminated. This

can be done one at another by the procedure described below. Once this is

done we obtain the desired linear derivation of the form T ⇒

∗

If L

k−1

is not used in D

we are done. Otherwise let

= D

λ,l,l+1

=(K

k−1

=====⇒

,γ

l+1

)

be such an inference step using L

k−1

. Swapping K

and L

k−1

implies the

existence of the I

-derivation

=(L

k−1

====⇒

,γ

l+1

)

Now concatenate D

· D

to obtain the I

-derivation

=(L

==⇒L

...

k−2

===⇒L

k−1

====⇒

,γ

l+1

) .

The top distance of K

in D

is k − 1 hence we can apply the induction

hypothesis to D

and obtain a linear I

-derivation

=(K

⇒

∗

l+1

) .

Next build D

0=D

]

λ,l,l+1

, i.e. replace the inference step using L

k−1

by a derivation not using L

k−1

. Hence the number of applications of the

literal L

k−1

has decreased by 1, which guarantees the termination of the

just described procedure when applied repeatedly in order to eliminate all

applications of L

k−1

. Hence the desired derivation exists.

Lifting Lemma for Background Refutations. In order to prove a lifting

lemma for background refutations we need one preliminary result:

Lemma A.2.8. Let α, β be substitutions and M be a literal set. Then

α(β|Var (Mα)) = αβ [Var (M)]

Proof. Let x be a variable. It suﬃces to show that both substitutions yield

the same result when applied to x. We distinguish two disjoint cases.

1. x/∈ Var (M). Trivial, since both substitutions yield x.

2. x ∈ Var (M). By deﬁnition of restriction of substitution it suﬃces to show

xα(β|Var (Mα)) = xαβ .

From x ∈ Var (M) it follows Var (xα) ⊆ Var (Mα) (*). Now we compute

xαβ = xα(β|Var (xα))

(∗)

= xα(β|Var (Mα))

which was to be shown.

A.2 Proofs for Chapter 5 — Linearizing Completion 261

Lemma A.2.9 (Lifting Lemma for Background Refutations). Let M

be a literal set, L

∈ M be literal, and γ be a ground substitution for M.For

every ground background refutation L

γ ⇒

∗

,Mγ

2 there is a ﬁrst-order back-

ground refutation L

⇒

∗

I,M,σ

2 such that σ ≤ γ [Var (M )].

Proof. Let the given refutation be

D =(L

===⇒

→L

)γ

===⇒L

...L

===⇒2) .

The proof is by induction on the length n of the derivation.

Induction start (n = 1): Deﬁne γ

= γγ

. We can safely assume that all

inference rules instances of which are used in D are all “new” variants. As a

consequence we get that the domains of γ and γ

are disjoint. Hence it holds

that

({|L

|}∪M

)

=({|L

|}∪M

)γ

where ({|L

|}∪M

)

is suitable ampliﬁcation of {|L

|}∪M

. Thus there is also

a multiset MGU σ

and a substitution δ

such that σ

= γ

(*). Using this

MGU we can build the ﬁrst-order refutation

=(L

==⇒

→L

,σ

with ampliﬁcation ({|L

|}∪M

)

and answer substitution σ

. It remains to

show that σ

satisﬁes the claimed property. From (*) and γ

= γγ

it follows

= γ

= γγ

= γ [Dom(γ)]. The last identity holds because γ is a

ground substitution. Since γ acts on every variable in M and in L

it holds

Dom(γ) ⊇ Var (M), and thus in particular σ

= γ [Var (M)]. This is the

same as σ

≤ γ [Var (M)] which was to be shown.

Induction step (n−1 → n): Suppose n>1 and as the induction hypothesis

assume the result to hold for derivations with length <n. Consider the ﬁrst

inference step in D. Deﬁne σ

and δ

in the same way as in the induction start,

i.e. σ

= γγ

(*) and σ

= γ [Var (M)]. Further it holds L

= L

γγ

due to the new variant used in the ﬁrst step. Thus, with (*) we have L

. Further, with the identity L

= L

and with σ

= γ [Var (M)]

we can delete the ﬁrst inference step from D and arrive at the refutation

=====⇒L

...L

=====⇒2 .

By the induction hypothesis we can lift this (still linear) refutation to a

(linear) refutation

===⇒

,σ

...L

···σ

n−1

==========⇒

,σ

with answer substitution

262 A. Appendix: Proofs

···σ

≤ δ

[Var (Mσ

)]

i.e. for some δ, σ

···σ

δ = δ

[Var (Mσ

)] (**). Since σ

is an appropriate

uniﬁer (as in the induction start) we can prepend this derivation with the

ﬁrst-order inference step L

==⇒

→L

,σ

to obtain

==⇒

→L

,σ

==⇒

,σ

...L

Mσ

···σ

n−1

=========⇒

,σ

2 ,

which is a linear ﬁrst-order refutation of L

as desired with answer substitu-

tion σ

···σ

. It remains to show that the answer substitution satisﬁes

the claimed property. Hence we compute

···σ

δ|Var (M)=σ

(σ

···σ

δ|Var (Mσ

))|Var (M)

(by Lemma A.2.8)

= σ

(δ

|Var (Mσ

))|Var (M ) (by (**))

= σ

|Var (M) (by Lemma A.2.8)

= γ|Var (M) (see induction start).

But then by deﬁnition σ

≤ γ [Var (M)] which was to be shown.

B. What is Where?

Notation

All chapters

¬, ∧, ∨, →, ↔ Connectives

∀, ∃ Quantiﬁers

Σ Signature

PF(Σ) The set of all formulas of signature Σ

CPF(Σ) The set of all closed formulas (i.e. sentences) of signature

T Theory

∀F , ∃F Universal and existential closure of formula F

a,b,... Constant symbol

f,g,... Function symbol

s,t,u,... Term

x,y,z,... (First-order) variable

A,B,C,... Atom

C,D,... Clause

P,Q,... Predicate symbol or literal

K,L,... Literal

α, β, δ,

φ, γ, σ, τ, µ Substitutions

 Empty substitution

 (Partial Strict) Ordering

∪=





Extension of  to multisets

P. Baumgartner: Theory Reasoning in Connection Calculi, LNAI 1527 , pp. 263-266, 1998

 Springer-Verlag Berlin Heidelberg 1998

264 B. What is Where?

Chapter 2

F, P, X Set of function symbols, predicate symbols, variables.

Term(F) The set of (ground) terms with function symbols from F

Term(F, X ) The set of terms with function symbols from F and vari-

ables from X

F, G Formula

S Sentence

M Set of sentences

S Structure

U Universe, as component of structure S also denoted by |S|

Assignment for variables X

I Interpretation, its universe denoted by |I|

hI,v

i Interpretation plus assignment (extended interpretation)

(X) Value of X in hI,v

Herbrand universe of Σ

HB(Σ) Herbrand base of Σ

Herbrand interpretation

Th(I) The theory of interpretation I

Cons(X) The theory of axiom set X

Chapter3+4+5

c computation rule

D Foreground calculi derivation

D, E Linearizing completion derivation

I,J Inference system

K Key set (of theory inference)

M,N Clause set, literal set

p, q Branch, read as a multiset

[p], [q] Branch, read as a sequence

···L

] Branch, labeled with literals L

,... ,L

P, Q Branch set

P Premise part of inference rule

C Conclusion of inference rule

S Transformation system

R Residue (in partial theory inference)

 Empty I-derivation (Chapter 5)



Ordering on multisets with weight



NMW

Ordering on nested multisets with weight

Note that some symbols are overloaded, e.g. C can be an atom or a clause.

Confusion is less likely in these cases as the meaning can always be detected

from the context. Where appropriate, sub- and superscripts will be used to

enlarge the repository of symbols.