Baumgartner P. Theory Reasoning in Connection Calculi

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

A.2 Proofs for Chapter 5 — Linearizing Completion 245

Now for the construction of F (cf. Figure A.1): the inference step G can

be written as

G =(L

=⇒

(L,N→C)γ

) ,

where P = {|L|}∪N, γ is a ground substitution, L

= Lγ, C

= Cγ and D

a sequence of derivations of Nγ; the complexity is

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

)|} .

From the assumption of the proposition we learn that a I\{P →

C}-

derivation

=((L = L

)

==⇒ ...

n−1

===⇒(L

= C))

exists such that hD

i≺≺

hN,wi (for 1 ≤ i ≤ n), where w

is the weight

of the inference rule used in the i-th inference step.

Applying the instantiation lemma to γ and F

(Lemma A.2.2) yields a

(I\{P → C})

-derivation

=((L

= L

γ)

==⇒ ...

n−1

====⇒(L

γ = C

)) .

Note that with I⊆J it holds that F

isa(J\{P → C})

-derivation as

well.

From hD

i≺≺

hN,wi it follows

γ,w

i≺≺

hNγ,wi . (A.50)

Since D

is a sequence of derivations of Nγ we can ﬁnd for every sequence

γ ⊆ Nγ a sequence D

⊆ D

such that D

is a sequence of derivations of

γ. But then we can replace every side derivation D

γ in F

by D

, yielding

still a (J\{P →

C})

-derivation (recall that we assume that no ground

instance of P →

C is used in G)

F =(L

==⇒ ...

==⇒C

)

with complexity

compl(F )={|0, hcompl(D

),w

i,... ,hcompl(D

n−1

),w

n−1

i|} .

Now consider (A.50) again: either it holds D

⊂ N which implies by con-

struction D

⊂ D

, which in turn implies hD

i≺≺

NMW

,wi; or else it

holds D

= N and w

<w, which implies by construction D

= D

and hence

also hD

i≺≺

NMW

,wi. It follows in any case F ≺ LinG which was to

be shown.

246 A. Appendix: Proofs

A.2.3 Section 5.4 — Transformation Systems

Lemma 5.4.1. Let S be a transformation system with derivation ordering

. Suppose P → C is -c-redundant in some I, and suppose that I`

J .

Then P → C is also -c-redundant in J .

Proof. J is obtained from I by deletion of a -c-redundant rule (case 1),

or by adding a new rule (case 2). We know that P → C is not of the form

¬A → F.

Case 1: We have J = I\{P

→ C

} for some rule P

→ C

∈Ito be

deleted. By deﬁnition of c-redundancy we have to show that whenever

D =(L

⇒

∗

((I\{P

→C

})∪{P →C})

) (A.51)

and P → C is used in D, then a

=(L

⇒

∗

((I\{P

→C

})\{P →C})

) (A.52)

exists such that D

≺ D.

From I\{P

→ C

}⊂Iand (A.51) it follows D =(L

⇒

∗

(I∪{P →C})

). We are given that P → C is -c-redundant in I. Hence a derivation

=(L

⇒

∗

(I\{P →C})

) exists such that D

≺ D. Now, if no ground

instance of P

→ C

is used in D

then D

is also a ((I\{P

→ C

}) \{P →

C})

-derivation, which proves (A.52). Otherwise, application of Lemma A.2.4

below to D

also proves (A.52).

Case 2: We have J = I∪{P

→ C

} for some new rule P

→ C

.By

deﬁnition of c-redundancy we have to show that whenever

D =(L

⇒

∗

((I∪{P

→C

})∪{P →C})

) (A.53)

and P → C is used in that derivation then a derivation

=(L

⇒

∗

((I∪{P

→C

})\{P →C})

) (A.54)

exists such that D

≺ D. Setting J = I∪{P

→ C

} in the deﬁnition of

c-redundancy (Def. 5.3.3) renders this case trivial.

The following lemma is needed in the proof of Lemma 5.4.3.

Lemma A.2.4. If

1. D =(L ⇒

∗

(I\{P →C})

), where P → C is a -c-redundant inference

rule in I, and

2. if in D some ground instance of P

→ C

is used, and

3. if I`I\{P

→ C

} =: J by deletion

A.2 Proofs for Chapter 5 — Linearizing Completion 247

then a derivation

=(L ⇒

∗

(J\{P →C})

)

exists with D

≺ D.

Proof. Informally: if P

→ C

is deleted in J then it must be c-redundant in

I. By redundancy, the use of P

→ C

in any derivation D

can be simulated

by the remaining rules of I. However, that simulating derivation, say D

might use P → C, which should not be used according to the lemma. On

the other hand, P → C itself is given as c-redundant in I and hence can be

simulated by the remaining rules. However, that derivation, say D

000

possibly

contains usages of P

→ C

again. Continuing this process will not fall into

a loop due to strictly reduced complexity (D

000

≺ D

) in every new

derivation and well-foundedness of .

Now the formal proof: if P → C/∈Ithen the lemma holds trivially by

the deﬁnition of -c-redundancy.

Otherwise we apply well-founded induction on derivation orderings.

With I\{P

→ C

}⊆Iit follows D =(L ⇒

∗

). With P

→ C

being deleted from I, P

→ C

must have been -c-redundant in I.Weare

given that a ground instance of P

→ C

is used in D. Hence by deﬁnition of

-c-redundancy a derivation

=(L ⇒

∗

(I\{P

→C

})

) (A.55)

exists with D

≺ D. Now we distinguish two cases:

Case 1: No ground instance of P → C is used in D

. But then by the

existence of D

we ﬁnd with (A.55) that D

=(L ⇒

∗

((I\{P →C})\{P

→C

})

which proves the lemma.

Case 2: A ground instance of P → C is used in D

. First note that from

I\{P

→ C

}⊆Iby (A.55) it follows D

=(L ⇒

∗

). We are given that

P → C is -c-redundant in I. By deﬁnition of -c-redundancy we conclude

that a derivation D

=(L ⇒

∗

(I\{P →C})

) exists such that D

≺ D

(≺ D).

Now apply the induction hypothesis to D

and conclude the result from

transitivity of .

Lemma 5.4.3. Let S be a transformation system with derivation ordering

.LetI

`··· be a S-deduction. If for some k, P → C is -c-redundant

in I

then P → C is -c-redundant in I

∞

Proof. In order to prove the lemma suppose that

D =(L ⇒

∗

∞

∪{P →C})

) (A.56)

which uses a ground instance of P → C. We have to show that a derivation

248 A. Appendix: Proofs

=(L ⇒

∗

∞

\{P →C})

) (A.57)

exists with D

≺ D. As a consequence of Proposition 5.4.1 some I

(m ≥ 0)

contains (at least) all those inference rules from I

∞

, the ground instances of

which are used in D. That is

D =(L ⇒

∗

∪{P →C})

) . (A.58)

We distinguish two cases:

Case 1: m>k. We are given that P → C is -c-redundant in I

. Applying

Lemma 5.4.1 m −k times we conclude that P → C is -c-redundant in I

well. Hence by deﬁnition of -c-redundancy we ﬁnd with (A.58) a derivation

=(L ⇒

∗

\{P →C})

) (A.59)

with D

≺ D.

Case 2: m ≤ k. By Lemma 5.4.2 every inference rule in I

is also con-

tained in I

. Thus with (A.58) D is also (I

∪{P → C})

-derivation.

We are given that P → C is -c-redundant in I

. Hence a derivation

=(L ⇒

∗

\{P →C})

with D

≺ D).

By taking n = max(m, k) in both cases a derivation

=(L ⇒

∗

\{P →C})

)

exists with D

≺ D.

We claim that for some l ≥ n a derivation D

=(L ⇒

∗

\{P →C})

)

exists with D

 D

, and the inference rules whose ground instances are used

in D

are never deleted afterwards, i.e. if (P

→ C

)γ ∈ (I

\{P → C})

is a

ground instance used in D

then P

→ C

∈I

\{P → C} for every j ≥ l.

This claim then proves (A.57) and thus the lemma by transitivity of 

and by the following line of reasoning: suppose P

→ C

∈I

\{P → C} for

every j ≥ l then

→ C

∈

j≥l

\{P → C})=(

j≥l

) \{P → C}

⊆ (

[

l≥0

j≥l

) \{P → C}

= I

∞

\{P → C} .

Hence if (P

→ C

)γ ∈ (I

\{P → C})

is a used ground instance in D

then

also (P

→ C

)γ ∈ (I

∞

\{P → C})

. Thus (A.57) follows.

It remains to prove the above claim. Starting with D

we construct a

sequence

n+1

n+2

,...

A.2 Proofs for Chapter 5 — Linearizing Completion 249

of derivations, where for i>nwe deﬁne

i+1











if I

i+1

is obtained from I

by deletion of an inference

rule P

→ C

, ground instances of which are used in

, where D

=(L ⇒

∗

i+1

\{P →C})

) and D

≺

. Such a derivation D

exists because with P → C

being -c-redundant in I

it follows by Lemma 5.4.1

that P → C is -c-redundant in I

, I

n+1

,... ,I

Now apply Lemma A.2.4.

else.

Note that in this sequence, deleting an inference rule P

→ C

, ground

instances of which are used, results in a strictly smaller derivation D

≺ D

Since  is a derivation ordering and hence well-founded, we arrive at the

chain D

n+1

,... , D

,.... Thus deletion of used inferences will not

be continued inﬁnitely. Stated positively, every inference system I

, I

l+1

, I

l+2

contains every inference rule, ground instances of which are used in D

.Thus

the claim above is proved, which concludes the proof of the lemma.

Lemma 5.4.5. Let S be a transformation system with derivation ordering

.LetI

`··· be an S-deduction. If there is a derivation

D =(L ⇒

∗

,M∪Punit (I

)

then there is also a derivation

=(L ⇒

∗

∞

,M∪Punit (I

∞

)

with D

 D.

Proof. The proof is similar to that of Lemma 5.4.3 above. As a consequence

of Lemma 5.4.4 every input literal from M ∪ Punit(I

) is also contained in

M ∪ Punit(I

∞

). Thus from the assumption of the lemma it follows D =

(L ⇒

∗

,M∪Punit (I

∞

)

). For ease of notation deﬁne N = M ∪ Punit(I

∞

We claim that for some l ≥ k a D

=(L ⇒

∗

) with D

 D exists,

and the inference rules whose ground instances are used in D

are never

deleted afterwards, i.e. if (P

→ C

)γ ∈I

is a ground instance used in D

then P

→ C

∈I

for every j ≥ l.

This claim then proves the lemma by the following line of reasoning:

suppose P

→ C

∈I

for every j ≥ l then

→ C

∈

j≥l

⊆

[

l≥0

j≥l

= I

∞

Hence if (P

→ C

)γ ∈I

is a used ground instance in D

then also (P

→

)γ ∈I

∞

. Thus the lemma follows.

250 A. Appendix: Proofs

It remains to prove the above claim. Starting with D

= D we construct

a sequence D

k+1

k+2

,... of derivations, where for i>kwe deﬁne

i+1











if I

i+1

is obtained from I

by deletion of an inference

rule P

→ C

, ground instances of which are used

in D

, where D

=(L ⇒

∗

i+1

) and D

≺ D

Such a derivation exists by deﬁnition of the deletion

operation.

else.

The rest of the proof is literally the same as in the proof of the previous

Lemma 5.4.3, and hence is omitted.

A.2.4 Section 5.5 — Complexity-Reducing Transformation

Systems

Proposition 5.5.1. The transformation system Lin is order-normalizing

wrt. LinG.

Proof. Let I be an inference system and D be a ground I

refutation of M

which is not linear, i.e. D/∈ LinG. We have to show that a (I

)

-derivation

≺

Lin

D of M exists, where I

= I or I

is obtained from I by application

of some mandatory transformation rule.

Since D is given as a non-linear derivation at least one side derivation is

not a sequence of trivial derivations. Thus D can be written as

D =(L

==⇒L

...

i−1

===⇒ L

=⇒L

i+1

| {z }

=:D

i+1

===⇒ ...L

n−1

===⇒L

) ,

where D

is that critical side derivation and D

= D|

λ,i,i+1

. More precisely,

the subderivation D

is of the form

=(L

Kγ

Mγ

======⇒

(L,K,M →L

)γ

i+1

) ,

where L

= Lγ, D

= D

Kγ

Mγ

, D

Kγ

is a non-trivial derivation of Kγ,

Mγ

is a sequence of derivations of Mγ and (L, K, M → L

)γ ∈I

is a

ground instance of L, K, M → L

∈I(cf. Figure A.2). We will show that

a(I

)

-derivation D

000

≺

Lin

exists, 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

]

λ,i,i+1

. By monotonicity of 

Lin

(Proposition 5.3.2) then

it follows D

≺

Lin

D, which was to be shown.

In general, the derivation D

Kγ

is of the form

Kγ

=(J

=⇒J

...J

m−1

====⇒J

| {z }

=:D

Jδ

Nδ

===⇒

(J,N →J

)δ

δ) ,

A.2 Proofs for Chapter 5 — Linearizing Completion 251

D :

i+1

R :

i+1

Kγ

R :

Deduce

Replace

Figure A.2. Illustration of proof of Proposition 5.5.1 (ground case).

252 A. Appendix: Proofs

where m ≥ 1, J

= Jδ, D

Nδ

is a (possibly empty) sequence of derivations of

Nδ, J

δ = Kγ and (J, N → J

)δ ∈I

is a ground instance of J, N → J

∈I.

Without loss of generality suppose that J, N → J

is variable disjoint from

L, K, M → L

. Consequently we may assume that the domains of δ and γ

are disjoint, too. Hence (J, N → J

)δγ =(J, N → J

)δ and (L, K, M →

)δγ =(L, K, M → L

)γ. Together with with J

δ = Kγ it follows that

δγ = Kδγ. In other words, δγ is a uniﬁer. Hence a MGU σ exists and

a substitution φ such that δγ = σφ. By the existence of this MGU, the

mandatory Deduce transformation rule can be applied to L, K, M → L

and

J, N → J

by unifying J

and K with σ. The result is the inference rule

R =(L, J, N, M → L

)σ.

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

deﬁne I

= I. Otherwise deﬁne I

= I∪{R}. Since Rφ is ground and D

Jδ

Nδ

and D

Mγ

are appropriate ground I

-derivations (and hence also (I

)

derivations) the (I

)

-derivation

000

=(L

Jδ

Nδ

Mγ

=========⇒

Rφ

i+1

)

exists. 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

. By deﬁnition of 

Lin

this is the same as to show compl(D

000

) ≺

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:

compl(D

)={|0, compl({|D

Kγ

|}∪D

Mγ

)|}

= {|0, compl(D

Kγ

) ∪ compl(D

Mγ

)|}

= {|0, {|0, compl(E

),... ,compl(E

m−1

), compl(D

Nγ

)|}

∪compl(D

Mγ

)|}

= {|0, compl(D

Jδ

) ∪{|compl(D

Nγ

)|}∪compl(D

Mγ

)|}



NMW

{|0, compl(D

Jδ

) ∪ compl(D

Nγ

) ∪ compl(D

Mγ

)|}

= {|0, compl(D

Jδ

Nγ

Mγ

)|}

= compl(D

000

)

The transition 

NMW

is justiﬁed by property of nested multiset ordering

(replacing a multiset by true subsets is decreasing). Since this remained to

be shown the proof is done.

Proposition 5.5.3. The transformation system Lin is Punit-normalizing

wrt. LinG.

Proof. Let I be an inference system and let

D =(T

==⇒T

...T

==⇒T

n+1

===⇒T

n+2

)

A.2 Proofs for Chapter 5 — Linearizing Completion 253

be the given non-trivial linear ground I

derivation from M ∪ Punit(I

)

such that Used(D) ∩ Punit(I

) 6= ∅. We have to show that a (I

)

-derivation

≺

Lin

D of M ∪ Punit((I

)

) exists, where I

= I or I

is obtained from

I by application of some mandatory transformation rule, and the top literal

of D

is T

or a literal from M ∪ Punit((I

)

). Since D is given as non-trivial

it holds n ≥ 0.

Let Lγ ∈ Used (D) ∩ Punit(I

) where Lγ is a ground instance of a literal

L ∈ Punit(I). Two cases apply: (1) Lγ occurs in some D

(i ∈{1 ...n+1})

or (2) Lγ = T

Case 1: (cf. Figure A.3) D contains an inference step of the form

= D|

λ,i,i+1

=(T

LγE

···E

=======⇒

,... ,E

→C)γ

Cγ

)(∗)

where (T

,... ,E

→ C)γ

∈I

is a ground instance of the rule

,... ,E

→ C ∈I, T

= T

, L

= Lγ, E

= E

(for

j =1...m

) and Cγ

= T

i+1

or Cγ

= F. The further reasoning holds

for both cases. We will show how to deduce a new inference rule by which

the application of Lγ in D

can be omitted.

Unit2

i+1

Lγ

D :

Replace

Used inference rule

Figure A.3. A case in the proof of Proposition 5.5.3 (ground case).

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

]

λ,i,i+1

. 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,

variable disjoint from the premise {|T

,... ,E

|} of the applied infer-

254 A. Appendix: Proofs

ence rule. Since Lγ = L

and L

is a variant of L a ground substitution γ

exists with L

= L

. Since L

is a new variant, γ

can be supposed not to

act upon the variables of L

. Hence L

= L

. Since γ

is a uniﬁer

for L

and L

a most general uniﬁer σ for L

and L

exists and substitution

δ such that σδ = γ

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

Unit2 transformation rule can be applied to T

,... ,E

→ C ∈Iand

→ F ∈I. The result is the new inference rule

R =(T

,... ,E

→ C)σ.

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

= I. Otherwise deﬁne I

= I∪{R}.

Let δ

be the restriction of γ

to the domain Var ({|T

,... ,E

,C|}) \

Var (L

). Together with (**) it follows

{|T

,... ,E

,C|}σδδ

= {|T

,... ,E

,C|}γ

{|T

,... ,E

,C|}γ

By these equalities we can build the desired derivation

000

=(T

···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

. By deﬁnition of 

Lin

this is the same as to show compl(D

000

) ≺

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:

compl(D

)={|0, compl(LγE

···E

)|}

= {|0, {|0|}∪compl(E

···E

)|}



NMW

{|0, compl(E

···E

)|}

= compl(D

000

)

Case 2: (Lγ = T

). We distinguish the cases (2.1) D

6= ε (i.e. D

is not

the empty sequence of derivations) and (2.2) D

= ε.

Case 2.1: D begins with the inference step

=(Lγ

···E

=======⇒

,... ,E

→C)γ

Cγ

)(∗)

where (L

,... ,E

)γ

→ Cγ

∈I

is a ground instance of the rule

,... ,E

→ C ∈I, L

= Lγ, K

= K, E

= E

(for j =

1 ...m

) and Cγ

= T

or Cγ

= F. The further reasoning holds for both

cases. It is in close analogy to the case Lγ ∈ D