Baumgartner P. Theory Reasoning in Connection Calculi

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

A.1 Proofs for Chapter 4 — Theory Reasoning 235

selected branch in D in Q

. Since D is a refutation, at some stage j>i

the instance [p

···σ

j−1

] must be selected in D, where σ

···σ

j−1

are the

substitutions used in the intermediate inferences. By applying the Switching

Lemma (Lemma A.1.11) j − i times, the branch [p

···σ

j−1

] can stepwisely

be moved backwards until it is selected as [p

]inQ

Concerning the stated property of the computed answer recall that the

members of the computed answer consists of (1) the literals of the start

clause and (2) of the literals of the query used as extending clauses. Now,

the switching lemma gives us a δ

such that Q

= Q

, where Q

is the

concluding (closed) tableau in the switched refutation, say D

. Hence, in

particular Q

= Q

where Q

(resp. Q

is (without loss of generality) the

start clause in D (resp. D

). Concerning the usage of ← Q as extending

clauses we also learn from the switching lemma that the extending clauses in

are the same as those of D, and their ﬁnal instantiations along D

can be

mapped by δ into the respective ﬁnal instantiations in D (in fact, these are

variants). Hence, in particular {Q

,... ,Q

}δ

= {Q

,... ,Q

Notice that D

is one more step in accordance with c as D. Further, since

the Switching Lemma preserves the length of derivations, repeated applica-

tion of this procedure terminates and ﬁnally results in the desired refutation

wrt. c.

A.1.2 Ground Completeness of PTME-I

This section is devoted to the critical lemma in the proof of Theorem 4.5.3.

The crucial point is how to transform a single TTME-MSR-Ext step into a

sequence of PTME-I steps.

Lemma A.1.12. Let I be a ground complete inference system wrt. a theory

T (cf. Def. 4.5.6). Suppose a ground TTME-MSR-Ext inference

[q],K,{|C

,... ,C

as given, where P and P

are ground branch sets and C

,... ,C

are ground

clauses from M . Furthermore suppose there are continuations (cf. Def. A.1.1)

and C

wrt. M of P and P

, respectively, with C

C

Then there is a sequence (P

= P) `···`P

of ground branch sets such

that for j =1...l, P

is obtained by a PTME-I

step from P

j−1

, where I

consists of all ground instances of all inference rules in I.

The extending clauses in these steps are all taken from {C

,... ,C

}, and

furthermore there is a continuation C

of P

with C

C



C

It is possible that the branch set P

consists of more branches than the

corresponding P

, but every branch in P

is contained with possibly some

extra branch literals in P

236 A. Appendix: Proofs

Proof. Assume that C

= L

∨R

(for i =1,... ,n) and K = B∪{|Leaf ([q])|}∪

L, where L = {|L

,... ,L

|} and for some B⊆q \{|Leaf ([q])|}. Further, P and

are of the form

P =[q], Q

= Q

, Q where Q

=[q] ◦

∨···∨R

By deﬁnition of TTME-MSR-Ext the key set K is minimal T -unsatisﬁable

(recall that since everything is ground, no substitution is needed and T -

complementarity coincides with T -unsatisﬁability).

Since I is given as ground complete, there is a background refutation R

of K with top literal Leaf ([q]). It is of the form

= Leaf ([q]))

==⇒R

···R

l−1

==⇒2

where the side literals M

(1 ≤ j ≤ l) are taken from K.

In order to transform this background refutation into a model elimination

refutation starting from the branch [q], we have to split the M

’s into two

parts: let

= M

∩B,

= M

∩L .

Intuitively, B

is the subset of M

which stems from the ancestor context of

the key set K of the TTME-MSR-Ext step, and L

is the subset of M

which

stems from the extending literals of the TTME-MSR-Ext step; L

consists of

literals from L and can be written as

= {|L

,... ,L

|}. (A.44)

Let

= {|L

∨ R

,... ,L

∨ R

be the corresponding clauses from {C

,... ,C

}. Using these deﬁnitions and

rewriting [q]as[q]=[p ·R

], we can deﬁne the claimed sequence

[p ·R

], Q (=P

=P)

[p·R

],K

[p ·R

·R

], Q

, Q =:P

[p·R

·R

],K

[p ·R

·R

], Q

, Q

, Q =:P

[p·R

···R

l−2

],K

l−1

[p ·R

···R

l−1

], Q

l−1

,... ,Q

, Q

, Q =:P

l−1

[p·R

···R

l−1

],K

[p ·R

···R

l−1

]×, Q

,... ,Q

, Q

, Q =:P

A.1 Proofs for Chapter 4 — Theory Reasoning 237

where

=[p ·R

·R

···R

j−1

] ◦ (R

∨···∨R

)

= B

∪{|R

j−1

|}∪L

That is, the j-th PTME-I

step is based on the theory inference

∪{|R

j−1

|}∪L

⇒R

which, using the identity M

= B

∪L

, exists according to the background

refutation R.

It remains to prove the stated ordering property C

C



C

. Note

that the given continuations are of the form

= {|N

[q]

|}∪C

= C

∪C

according to the structure of P and P

, where C

is a continuation of Q.

Since C

C

we have by multiset ordering and the fact that {|N

[q]

|} is a

singleton

for every N

]

∈C

: N

[q]

 N

]

. (A.45)

Now consider a branch [q ·R

···R

j−1

· K] ∈Q

, where K ∈ R

∨ ··· ∨

. K stems from the Rest R

of some given clause L

∨ R

∈ M. For the

given TTME-MSR-Ext step we know [q · K] ∈Q

and there is a respective

continuation N

[q·K]

∈C

. Now deﬁne

[q·R

···R

j−1

·K]

= N

[q·K]

as a continuation of [q ·R

···R

j−1

·K] wrt. M (the additional residue literals

do not violate the continuation property). Note that with A.45 it holds that

[q]

 N

[q·R

···R

j−1

·K]

. (A.46)

Since no special assumptions about Q

were made we can generalize and ﬁnd

for every branch in (Q

,... ,Q

) a continuation in this way. Let C

,... ,Q

)

be the thus existing continuation of the branch set (Q

,... ,Q

) consisting

of elements from C

With (A.46) it follows N

[q]

 N for every N ∈C

,... ,Q

)

, and by prop-

erty of multiset orderings thus ({|N

[q]

|} is a singleton)

{|N

[q]

|}C

,... ,Q

)

Finally deﬁne C

= C

,... ,Q

)

∪C

as the desired continuation of P

. Also

by property of multiset orderings it follows

= {|N

[q]

|}∪C

C

,... ,Q

)

∪C

= C

238 A. Appendix: Proofs

In order to see the other stated ordering property observe that every clause

∨ R

must be used at least once in the constructed partial derivation,

because otherwise the key set K of the given TTME-MSR-Ext step would be

not minimal T -valid. Hence R

is used in the construction of at least one Q

Thus every element in C

occurs at least once in C

,... ,Q

)

. From this it

follows

= C

,... ,Q

)

∪C



C

∪C

= C

This lemma can be applied to whole derivations:

Lemma A.1.13 (PTME-I simulates TTME-MSR). Let I

be a ground

complete inference system wrt. a theory T .LetD be a TTME-MSR refu-

tation of a ground clause set M with start clause G ∈ M . Suppose D is

constructed as ﬁgured out in the ground completeness proof for TTME-MSR

(Lemma A.1.2). Thus, D is of the form

D = P

`···`P

and there are respective continuations wrt. M

 ···  (C

= {||}).

Then there is a PTME −I

refutation

PTME−I

= P

`···`P

of M, stable wrt. minimality and with start clause G.

Proof. By deﬁnition, every TTME-MSR-Ext step in the refutation D employs

a minimal T -complementary (ground) key set K. By applying Lemma A.1.12

every such step can be replaced by a sequence of PTME-I-Ext extension

steps. However, a little care must be taken for the inductive argument. Since

Lemma A.1.12 possibly increases the number of branches, simple induction

on e.g. the number of occurrences of total extension steps does not work.

The lemma is shown by well-founded induction on the continuation C

the ﬁrst tableau of derivations of the given form, which are compared by the

multiset ordering “” on complexities of continuations.

The induction start with C

= {||} being trivial (take P

= P

which

must be a closed tableau according to the deﬁnition of continuation) we turn

immediately to the induction step: we have C

6= {||}. Hence at least one

TTME-MSR-Ext step is applied in D. Next we apply Lemma A.1.12 to P

and P

and replace the underlying TTME-MSR-Ext step by a sequence of

-extension steps. Let (P

= P

) `P

···P

be the resulting sequence.

Notice that Lemma A.1.12 also gives us C

P

(*). Also by that lemma

there is a continuation C

of P

. Hence we can apply Lemma A.1.8 and

obtain a TTME-MSR refutation D

starting with P

A.2 Proofs for Chapter 5 — Linearizing Completion 239

is of the same form as the given D, in that respective decreasing con-

tinuations corresponding to the tableaux along D

exist. Furthermore since

(*) holds, the induction hypothesis can be applied to D

, which yields a

PTME−I

refutation D

. Now prepend D

with P

`···`P

l−1

to obtain

the desired derivation D

PTME−I

Further, D

PTME−I

is trivially stable wrt. minimality, because every un-

derlying theory inference uses, by deﬁnition, key sets without duplicates, and

this status cannot change along the derivation as all key sets are ground.

A.2 Proofs for Chapter 5 — Linearizing Completion

A.2.1 Section 5.2 — Inference Systems

Lemma 5.2.1 (Ground completeness of I

(T )). Let T be a ground the-

ory (i.e. a theory consisting of ground clauses only) and M be a set of ground

literals. If M is T -unsatisﬁable then L ⇒

∗

(T ),M∪Punit (I

(T ))

F for some

L ∈ (M ∪ Punit(I

(T ))).

Proof. By Proposition 2.5.1.3, equivalence (a)–(e), M is T -unsatisﬁable iﬀ

M ∪T is unsatisﬁable, where M is considered as a set of unit clauses. We

apply induction on the size n of the atom set of M ∪T (the atom set of a

Horn clause set consists of all atoms occurring in clauses in it).

Induction start (n = 1): M ∪T must contain a positive literal A and a

purely negative clause ¬A

∨ ...∨¬A

with k ≥ 1 occurrences of ¬A (the

superscripts denote the distinct occurrences of the same literal ¬A).

The literal A and the clause ¬A

∨ ...∨¬A

may be contained in M or

in T , which results in the following cases:

If k = 1 then ¬A ∈T or ¬A ∈ M .If¬A ∈T then the same refutation as

in case k>1 below exists. Therefore suppose now ¬A ∈ M.WehaveA ∈ M

or A ∈T.IfA ∈ M then a refutation

¬A

==⇒

A,¬A→F

exists. If A ∈T then by deﬁnition of I

, ¬A → F ∈I

(T ). In this case a

refutation

¬A

=⇒

¬A→F

exists.

If k>1 then ¬A

∨...∨¬A

∈T follows. By deﬁnition of I

···A

→

F ∈I

(T ). We have A ∈ M or A ∈T. However, since a theory is satisﬁable

by deﬁnition, A ∈T is not possible. Hence A ∈ M. Thus a refutation

···A

=====⇒

,... ,A

→F

240 A. Appendix: Proofs

from M ∪ Punit(I

(T )) exists.

Induction step (n>1): M ∪T must contain at least one positive unit

clause. (proof: if not, then every clause contains at least one negative literal.

But then an interpretation that assigns trueto every negative literal is a model

for M ∪T. Contradiction). Thus let A ∈ M ∪T be a positive unit clause. If

A ∈ M then clearly A ∈ M ∪ Punit(I

(T )). If A ∈T then ¬A → F ∈I

(T )

and thus A ∈ Punit(I

(T )). Thus always A ∈ M ∪ Punit(I

(T )). This fact

will be used below.

If M ∪T contains a clause ¬A ∨ ...∨¬A the same argument as for n =1

applies. This check guarantees that the following processing does not yield

the empty clause.

Let T

, resp. M

, be obtained from T , resp. M, by deleting every clause

of the form A ∨ R (R may be empty), and then by replacing every clause of

the form ¬A

∨ ...∨¬A

∨ R (where ¬A does not occur in R, and R cannot

be empty) by R.InT

∪ M

neither A nor ¬A occurs. Thus the atom size of

∪T

is n−1. Furthermore M

∪T

must be unsatisﬁable, because otherwise

a model for M

∪T

can be extended to a model that assigns trueto A, which

would be in turn a model for M ∪T , and thus M would be T -satisﬁable. Hence

we can apply the induction hypothesis and assume that a I

)-refutation

of M

∪ Punit(I

)) exists. Let D

be that refutation. We show how to

transform D

into a I

(T )-refutation of M ∪ Punit(I

(T )). For this, every

inference step involving a positive literal B ∈ M

∪ Punit(I

)) which is

not contained in M ∪Punit(I

(T )) has to be eliminated from D

(subcase 1),

and every inference step involving an inference rule P → C ∈I

) which

is not contained in I

(T ) has to be eliminated from D

(subcase 1)

Subcase 1: We conclude from M

⊆ M that B/∈ Punit(I

(T )). From B ∈

Punit(I

)) it follows B ∈T

. Since B/∈ Punit(I

(T )) it follows B/∈T.

Hence B ∈T

is obtained from ¬A

∨ ...∨¬A

∨ B ∈T by the replacement

operation described above. With A ∈ M ∪ Punit(I

(T )) and A

,... ,A

→

B ∈I

(T )aI

(T )-derivation

=(A

···A

=====⇒

,... ,A

→B

of B from M ∪ Punit(I

(T )) exists. Hence a I

)-derivation B from M

∪

Punit(I

)) occurring in D

can be replaced by the I

(T )-derivation D

from M ∪ Punit(I

(T )).

Subcase 2: We have P → C ∈I

) but P → C/∈I

(T ). Here we dis-

tinguish two cases: in the ﬁrst case, P → C is of the form ¬B → F.Thus

B ∈T

was obtained from ¬A

∨ ...∨¬A

∨ B ∈T by the replacement

operation above. Hence A

,... ,A

→ B ∈I

(T ) and we can again ﬁnd the

(T )-derivation D

of B from M ∪ Punit(I

(T )). D

is of the form

=(L

==⇒

...L

==⇒

¬B

=⇒

¬B→F

F) .

To be completely formal, this requires induction on the number of applications

of the rule P → C and the literal B in D

A.2 Proofs for Chapter 5 — Linearizing Completion 241

Now replace the last inference with ¬B → F by an inference with ¬B, B →

F ∈I

(T ) to obtain the refutation

==⇒

...L

==⇒

¬B

==⇒

¬B,B→F

F .

In the second case P → C is not of the form ¬B → F. By deﬁnition of I

P → C then must be of the form B

,... ,B

→ C, where the B

s are positive

literals and C is either a positive literal or F.ThusT

contains a clause ¬B

∨

...∨¬B

∨C or ¬B

∨...∨¬B

, respectively. The further argumentation holds

for both cases. Let us therefore consider only the ﬁrst case. ¬B

∨...∨¬B

∨C

is obtained from the clause ¬A

∨ ...¬A

∨¬B

∨ ...∨¬B

∨ C ∈T by the

replacement operation above. So A

,... ,A

,... ,B

→ C ∈I

(T ). Since

A ∈ M ∪ Punit(I

(T )) every inference step

···D

=====⇒

,... ,B

→C

in D

with B

,... ,B

→ C ∈I

) can be replaced by an inference with

,... ,A

,... ,B

→ C ∈I

(T ) to obtain

···A

···D

==========⇒

,... ,A

,... ,B

→C

A.2.2 Section 5.3 — Orderings and Redundancy

Proposition 5.3.2. The relation 

Lin

is a monotonic derivation ordering.

Proof. By deﬁnition D 

Lin

E iﬀ compl(D) 

NMW

compl(E). By Proposi-

tion 5.3.1, 

NMW

is a simpliﬁcation ordering and hence by Theorem 2.1.1

well-founded.

Monotonicity is proven by simple structural induction on the derivation,

using in the induction step the fact that 

NMW

is monotonic. More formally,

let D be a derivation and suppose D|

p,i,j

= G, F is a derivation which agrees

with G on top literal and derived literal and G 

Lin

F . We have to show

D 

Lin

D[F ]

p,i,j

Induction start: if p = λ then D = D|

is of the form

D =(L

==⇒L

...L

=⇒L

i+1

...L

j−1

===⇒L

| {z }

==⇒L

j+1

...L

n−1

===⇒L

) ,

where 1 ≤ i<j≤ n (the case i = j is impossible since then G would be

a trivial derivation, whose complexity is a bottom element wrt. 

Lin

). The

complexities of G and D can be written as

compl(G)={|0|}∪R

, where

= {|compl(D

)

,... ,compl(D

j−1

)

j−1

|} (A.47)

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

)

,... ,compl(D

i−1

)

i−1

|}∪R

∪{|compl(D

)

,... ,compl(D

n−1

)

n−1

|} . (A.48)

242 A. Appendix: Proofs

Concerning the derivation F , compl(F ) can be written as

compl(F )={|0|}∪R

. (A.49)

By deﬁnition, G 

Lin

F iﬀ compl(G) 

NMW

compl(F ). But then it follows

with (A.47) and (A.49) by monotonicity property (Theorem 2.1.1) of 

NMW

(deleting identical elements does not change the relationship among multisets

with weights) R



NMW

(*).

Now consider the derivation D[F ]

λ,i,j

; its complexity is

compl(D[F ]

λ,i,j

)={|0, compl(D

)

,... ,compl(D

i−1

)

i−1

|}∪

∪{|compl(D

)

,... ,compl(D

n−1

)

n−1

|} .

From (*) it follows again by monotonicity property of 

NMW

(replacing

a subset by a smaller set makes the whole set smaller) compl(D) 

NMW

compl(D[F ]

λ,i,j

) and thus also D 

Lin

D[F ]

λ,i,j

Induction step: p is of the form k.l.r and thus D is of the form

D =(L

==⇒L

...L

==⇒L

k+1

...L

n−1

===⇒L

), where

= D

···D

Hence compl(D) is of the form

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

),... ,compl(D

k−1

compl(D

) ∪···∪compl(D

compl(D

k+1

),... ,compl(D

)|} ,

with D|

k.l

= D

. In order to build D[F ]

k.l.r,i,j

we have to replace D

[F ]

. This means for the complexity of the new derivation

compl(D[F ]

k.l.r,i,j

)={|0, compl(D

),... ,compl(D

k−1

compl(D

) ∪···∪compl(D

[F ]

) ∪···∪

compl(D

k+1

),... ,compl(D

)|}

By the induction hypothesis D



Lin

[F ]

Thus by deﬁnition compl(D

) 

NMW

compl(D

[F ]

). Thus by monotonic-

ity of 

NMW

compl(D) 

NMW

compl(D[F ]

k.l.r,i,j

) and hence D 

Lin

D[F ]

k.l.r,i,j

The following lemma is needed in the proof of Proposition 5.3.3:

Lemma A.2.2 (Instantiation Lemma for Linear Derivations). Suppose

a linear I-derivation

D =(L

==⇒L

...L

n−1

===⇒L

)

Weights omitted.

A.2 Proofs for Chapter 5 — Linearizing Completion 243

as given, and let γ be a ground substitution for L

, M and L

. Then a linear

ground I

-derivation

==⇒L

...L

n−1

====⇒L

exists, where each γ

is some ground substitution for L

Thus, derivations may be ground instantiated; the additional (ground) sub-

stitutions γ

come in due to extra variables in the conclusion of inference

rules, and these variables have to be grounded in order to match the ground

literal in the premise of the subsequent inference step.

Proof. Induction on the length n of the derivation.

Induction start (n = 1) trivial, simply take L

γ as the desired derivation.

Induction step (n − 1 → n): assume n>1 and assume the result holds

for derivations of length n − 1. The concluding inference step of the given

derivation D is more precisely

n−1

===⇒

n−1

→C

n−1

,σ

n−1

where {|L

n−1

|}∪D

n−1

= P

n−1

(*) and C

n−1

= L

Next consider the preﬁx L

==⇒L

...L

n−2

===⇒L

n−1

of D. Let γ

be a

ground substitution for L

n−1

γ. γγ

a ground substitution for L

, M and L

n−1

(because γ alone is a ground substitution, as given). Hence, by the induction

hypothesis exists a I

-derivation

= L

γγ

====⇒L

...L

n−2

γγ

======⇒L

n−1

γγ

Since L

γ being ground it follows L

γ = L

γγ

. Similarly, since Mγ is ground

and all literals in the sequence D

are taken from M it follows that D

γ is

also ground. But then D

γ = D

γγ

. By these considerations D

is a I

derivation of L

n−1

γγ

from Mγ with top literal L

γ.

With P

n−1

= {|L

n−1

|}∪D

n−1

, as given, it follows that D

can be ex-

tended by means of the substitution γγ

with one inference step to a deriva-

tion

=(D

· (L

n−1

γγ

n−1

γγ

======⇒

n−1

→C

n−1

)γγ

n−1

γγ

)) .

By the same arguments as for D

above it holds D

n−1

γ = D

n−1

γγ

; fur-

thermore, with L

γ being ground and with L

= C

n−1

σ it follows that

γ = C

n−1

σγ = C

n−1

σγγ

.ThusD

is a derivation of L

γ from Mγ.

We have to show that D

is c I

-derivation, i.e. that the used inference

rule in the last step is contained in I

. Since D

n−1

γ is ground (as concluded

above) and L

n−1

γγ

is ground (by deﬁnition of γ

) and C

n−1

σγγ

is ground

(because C

n−1

σγγ

= L

γ) it follows with (*) that (P → C)γγ

is also

ground. Hence from P → C ∈I it follows (P → C)γγ

∈I

, and so D

is a

-derivation. Setting γ

n−1

= γγ

shows that D

is the desired derivation.

244 A. Appendix: Proofs

Proposition 5.3.3 (Suﬃcient 

Lin

-Redundancy Criterion). Let I be

an inference system and P →

C be an inference rule. Suppose that for

every L ∈ P there is a linear I\{P →

C}-derivation from P

(L =

)

==⇒

→

==⇒

→

···L

n−1

===⇒

n−1

→

n−1

= C)

with n ≥ 1 and such that for i =1,... ,n− 1 it holds hP \{|L|},wi

i In this comparison the sequence D

of literals is to be read as a

multiset. Then P →

C is 

Lin

-redundant in I for derivations.

Proof. By contradiction. Hence suppose the assumptions of the proposition

hold and P → C is not 

Lin

-d-redundant in I. Then for some inference

system J⊇I, some ground literal L

, some ground literal set M and some

ground literal L

a derivation D =(L

⇒

∗

(J∪{P →C})

) exists but a

derivation D

−

=(L

⇒

∗

(J\{P →C})

) with D

−

≺

Lin

D (*) does not

exist.

We are given that at least one ground instance of P →

C is used in some

inference step G = D|

p,i,i+1

in D. W.l.o.g assume that no further ground

instance of P →

C is used in G (by tracing into D and its subderivations

such a “bottommost” derivation can always be located).

We will show that a (J\{P →

C})

-derivation F with F ≺

Lin

which can replace G in D, i.e. we build D

−

= D[F ]

p,i,i+1

. Since 

Lin

monotonic (Proposition 5.3.2) it then holds D

−

≺

Lin

D. Since F does not

use a ground instance of P →

C the number of usages of ground instances

of P →

C in D

−

is 1 less than in D. Hence repeated application of this

procedure terminates and thus yields a (J\{P →

C})

-derivation. But

then by transitivity of 

Lin

we obtain a contradiction to (*).

Replace

γ :

G :

F :

γ :

n−1

γ :

Figure A.1. Illustration of proof of Proposition 5.3.3.