Baumgartner P. Theory Reasoning in Connection Calculi
Подождите немного. Документ загружается.
A.1 Proofs for Chapter 4 — Theory Reasoning 225
Suppose E
0
l
= {L
0
1
∨ R
0
1
,... ,L
0
n
∨ R
0
n
} are the new variants of clauses
from M
0
used as extending clauses in the concluding step of D
0
l+1
with L
0
=
{|L
0
1
,... ,L
0
n
|} being the extending literals. Suppose K
0
l
= B
0
∪{|Leaf ([p
0
l
])|}∪L
0
,
for some B
0
⊆ [p
l
] \{|Leaf ([p
0
l
])|}. This setup can be taken for both calculus
variants. However, there are some differences in further argumentation.
In case of TTME-MSR, by definition, K
0
l
σ
0
l
is minimal T -complementary
(we need not insist that σ
0
l
is a T -MGR).
In case of PTME-I
0
, the PTME-I-Ext step is based on the theory inference
K
0
l
⇒
P
0
l
→C
0
l
,σ
0
l
R
0
l
σ
0
l
(A.15)
for some new variant P
0
l
→ C
0
l
of a rule from I
0
. In both versions the resulting
branch set Q
0
l+1
can be written as
Q
0
l+1
=([p
0
l
] ◦
×
(R
0
l
∨ R
0
1
∨···∨R
0
n
) ∪ (Q
0
l
\{|[p
0
l
]|}))σ
0
l
,
where for TTME-MSR we set R
0
l
= 2.
By the induction hypothesis A.9 there is in particular (both versions) a
branch [p
l
] ∈ Q
l
with [p
l
]δ
l
=[p
0
l
]. Thus also a subsetB⊆[p
l
] \{|Leaf ([p
l
])|}
with Bδ
l
= B
0
exists.
Next we are going to set up a corresponding set E
l
of extending clauses.
By the fact we can find for every clause (L
0
i
∨ R
0
i
) ∈ E
0
l
(i =1,... ,n)a
new variant L
i
∨ R
i
of a clause from M and a substitution γ
L
i
∨R
i
such
that (L
i
∨ R
i
)γ
L
i
∨R
i
= L
0
i
∨ R
0
i
. Hence let E
l
= {L
1
∨ R
1
,... ,L
n
∨ R
n
},
L = {|L
1
,... ,L
n
|} and define the key set to be used in the lifted inference
as K
l
= B∪{|Leaf ([p
l
])|}∪L. We have to show that E
l
and K
l
are suitably
defined.
All the clauses L
i
∨ R
i
are new variants, and hence are variable disjoint.
So without loss of generality we can assume that γ
L
i
∨R
i
acts on the variables
of L
i
∨ R
i
only, that is Dom(γ
L
i
∨R
i
) ⊆ Var (L
i
∨ R
i
). But then we can define
γ
l
= γ
L
1
∨R
1
···γ
L
n
∨R
n
and it holds
(L
i
∨ R
i
)γ
l
= L
0
i
∨ R
0
i
, (A.16)
which implies
Lγ
l
= L
0
. (A.17)
Since E
l
consists of new variants we can assume that δ
l
does not act on the
variables of L
i
∨ R
i
. Hence
L
i
∨ R
i
=(L
i
∨ R
i
)δ
l
, (A.18)
which implies
L = Lδ
l
. (A.19)
226 A. Appendix: Proofs
Recall that γ
l
acts on the variables of E
l
only. But with E
l
consisting of new
variants we find that E
l
is variable disjoint from Q
l
δ
l
, and hence
Q
l
δ
l
= Q
l
δ
l
γ
l
. (A.20)
We continue
K
0
l
σ
0
l
=(B
0
∪{|Leaf ([p
0
l
])|}∪L
0
)σ
0
l
=(Bδ
l
∪{|Leaf ([p
l
])δ
l
|}∪Lγ
l
)σ
0
l
(by (A.9) for l and (A.17))
=(Bδ
l
γ
l
∪{|Leaf ([p
l
])δ
l
γ
l
|}∪Lδ
l
γ
l
)σ
0
l
(by (A.19) and (A.20))
=(B∪{|Leaf ([p
l
])|}∪L)δ
l
γ
l
σ
0
l
= K
l
δ
l
γ
l
σ
0
l
.
(A.21)
This setup holds for both variants.
Now we have to distinguish. In case of TTME-sem, (A.21) tells us that
δ
l
γ
l
σ
0
l
is a, although minimal, not necessarily most general T -refuter for K
l
.
We conclude with Proposition 4.4.1 that there is a T -MGR σ
l
∈ MSR
T
(K
l
)
and a substitution δ
l+1
such that
δ
l
γ
l
σ
0
l
= σ
l
δ
l+1
[W ], where
W =
l
[
j=1
(Var (Q
j
σ
j
···σ
l−1
) ∪ Var (K
j
σ
j
···σ
l−1
) ∪ Var (E
j
σ
j
···σ
l−1
)) .
(A.22)
By construction of K
j
it holds that Var (K
j
) ⊆ Var (Q
j
)∪Var (E
j
), and hence
the Var (K
j
) term could be omitted in the definition of W .
By Proposition 4.2.1.2 we have that if δ
l
γ
l
σ
0
l
is a minimal T -refuter, then
so must be σ
l
. Hence, a TTME-MSR-Ext step based on σ
l
and using extending
clauses E
l
and key set K
l
can be carried out to Q
l
.
For PTME-I
0
we need the following reasoning: recall that we demand that
the used theory inference rule (in D
0
l+1
) P
0
→ C
0
is a new variant. Hence
neither δ
l
nor γ
l
will act on P
0
→ C
0
and we will thus have
(P
0
→ C
0
)δ
l
γ
l
= P
0
→ C
0
. (A.23)
But then, using this fact and Equation A.21, the theory inference A.15) is
the same as
K
l
⇒
P
0
l
→C
0
l
,δ
l
γ
l
σ
0
l
R
0
l
δ
l
γ
l
σ
0
l
. (A.24)
With A.23 it trivially follows that δ
l
γ
l
does not affect R
0
l
. Hence
A.1 Proofs for Chapter 4 — Theory Reasoning 227
R
0
l
δ
l
γ
l
σ
0
l
= R
0
l
σ
0
l
. (A.25)
This trivially also holds for the TTME-MSR-Ext case, where R
0
l
= 2.
The inference rule (P
0
l
→ C
0
l
) ∈I
0
must be a new variant of some instance
of some inference rule (P
base
→ C
base
) ∈I. Let P
l
→ C
l
be any new variant
of P
base
→ C
base
, and consider the set W from A.22. With P
l
→ C
l
being a
new variant, it will clearly hold Var (P
l
→ C
l
) ∩ (W ∪ Var (K
l
)) = ∅.Thuswe
can apply Lemma A.1.10, which gives us the following theory inference step
with multiset-MGU σ
l
:
K
l
⇒
P
l
→C
l
,σ
l
R
l
σ
l
. (A.26)
Hence, a PTME-I-Ext step based on K
l
, P
l
→ C
l
, σ
l
and extending clauses
E
l
, yielding residue hR
l
,σ
l
i can be carried out to Q
l
.
Further, Lemma A.1.10 also gives us a substitution δ
l+1
such that
δ
l
γ
l
σ
0
l
= σ
l
δ
l+1
[W ] (A.27)
R
0
l
δ
l
γ
l
σ
0
l
= R
l
σ
l
δ
l+1
. (A.28)
This will be needed below.
In both cases (TTME-MSR and PTME-I), the resulting branch set Q
l+1
is
Q
l+1
=([p
l
] ◦
×
(R
l
∨ R
1
∨···∨R
n
) ∪ (Q
l
\{|[p
l
]|}))σ
l
. (A.29)
In order to prove Equation A.9 for l + 1 we have to show Q
0
l+1
= Q
l+1
δ
l+1
:
Q
0
l+1
=([p
0
l
] ◦
×
(R
0
l
∨ R
0
1
∨···∨R
0
n
) ∪ (Q
0
l
\{|[p
0
l
]|}))σ
0
l
=([p
l
δ
l
] ◦
×
(R
0
l
∨ R
1
γ
l
∨···∨R
n
γ
l
) ∪ (Q
l
δ
l
\{|[p
l
δ
l
]|}))σ
0
l
(by A.9 for l and (A.16))
=([p
l
δ
l
γ
l
] ◦
×
(R
0
l
∨ R
1
δ
l
γ
l
∨···∨R
n
δ
l
γ
l
) ∪ (Q
l
δ
l
γ
l
\{|[p
l
δ
l
γ
l
]|}))σ
0
l
(by (A.18) and (A.20))
=[p
l
δ
l
γ
l
σ
0
l
] ◦
×
(R
0
l
δ
l
γ
l
σ
0
l
∨ R
1
δ
l
γ
l
σ
0
l
∨···∨R
n
δ
l
γ
l
σ
0
l
)
∪ (Q
l
δ
l
γ
l
σ
0
l
\{|[p
l
δ
l
γ
l
σ
0
l
]|})
(by distributing σ
0
l
and (A.25))
=[p
l
σ
l
δ
l+1
] ◦
×
(R
l
σ
l
δ
l+1
∨ R
1
σ
l
δ
l+1
∨···∨R
n
σ
l
δ
l+1
)
∪ (Q
l
σ
l
δ
l+1
\{|[p
l
σ
l
δ
l+1
]|})
(by (A.22) (TTME-MSR), resp.
by (A.27) and (A.28) (PTME-I))
= Q
l+1
δ
l+1
by (A.29)
We have to prove Equation A.10 for l + 1, i.e. for j =1,... ,l:
228 A. Appendix: Proofs
K
0
j
σ
0
j
···σ
0
l−1
σ
0
l
= K
j
σ
j
···σ
l−1
σ
l
δ
l+1
. (A.30)
We distinguish two cases:
j = l: K
0
l
σ
0
l
(A.21)
= K
l
δ
l
γ
l
σ
0
l
(A.22,A.27)
= K
l
σ
l
δ
l+1
.
1 ≤ j ≤ l − 1: By construction, γ
l
acts on the new variants E
l
only, and
hence does not affect K
0
j
σ
0
j
···σ
0
l−1
.Thus
(K
0
j
σ
0
j
···σ
0
l−1
)σ
0
l
=(K
0
j
σ
0
j
···σ
0
l−1
γ
l
)σ
0
l
(A.10)
=(K
j
σ
j
···σ
l−1
)δ
l
γ
l
σ
0
l
(A.22,A.27)
=(K
j
σ
j
···σ
l−1
)σ
l
δ
l+1
= K
j
σ
j
···σ
l
δ
l+1
.
Thus, in both cases, A.10 holds for l + 1. The proof of property A.11 for l +1
is analogue and hence is omitted.
It remains to prove preservation of stability wrt. minimality and preser-
vation of regularity. Concerning the stability wrt. minimality we use the
just derived result, Equation A.10, and conclude with the given minimal
T -complementarity of K
0
j
σ
0
j
···σ
0
l
and Proposition 4.2.1.2 that K
j
σ
j
···σ
l
is
minimal T -complementary as well.
Concerning regularity, we have to show that every occurrence of a branch
[p] ∈Q
l+1
is regular. From Q
0
l+1
= Q
l+1
δ
l+1
it follows that there is a cor-
responding occurrence of branch [p
0
] ∈ Q
0
l+1
such that [p
0
]=[pδ
l+1
]. Now,
regularity of [p] holds by Proposition 3.3.1 and regularity of [p
0
], which holds
if D
0
is given as regular.
Independence of the Computation Rule The “next” subgoal to be pro-
cessed in model elimination derivations may be chosen in a don’t-care nonde-
terministical way. This result is known as the “independence of the compu-
tation rule” (cf. also Section 3.3). The proof works by developing a switching
lemma which says that two subsequent selected subgoals may be extended in
exchanged order. When applied repeatedly, this shows us that any refutation
can be reordered until it is in accordance with a given computation rule.
There are basically two approaches: the easier approach operates on the
ground-level (recall that we use a ground-proof-and-lifting technique). This,
however, has the disadvantage that the computation rule must be demanded
to be “stable under lifting”, i.e. that if a computation rule selects a literal
Lγ within a clause Cγ, then it has to selected L in C.
Since such a restriction would be poorly motivated, and is not even neces-
sary, we will develop the result directly on the first-order level. The same ap-
proach was taken in
[
Lloyd, 1987
]
for SLD-resolution. However, a non-trivial
complication comes in by the “stability wrt. minimality” (cf. Definitions 4.4.4
and 4.5.7) which trivially holds in the non-theory case.
The “independence of the computation rule” holds for both, TTME-MSR
and PTME-I. Since the argumentation of the proof has much in common with
A.1 Proofs for Chapter 4 — Theory Reasoning 229
the preceding lifting lemma, we will adopt the conventions A.1.1 here, too.
The key to the desired result is the following lemma:
Lemma A.1.11 (Switching Lemma). Suppose a refutation D, stable wrt.
minimality,
D = Q
1
`···`Q
i−1
` [p
i
], [p
i+1
], Q =: Q
i
`
[p
i
],K
i
,P
i
→C
i
,hR
i
,σ
i
i,E
i
(P
i
, [p
i+1
], Q)σ
i
=: Q
i+1
`
[p
i+1
σ
i
],K
i+1
,P
i+1
→C
i+1
,hR
i+1
,σ
i+1
i,E
i+1
(P
i
, P
i+1
, Q)σ
i
σ
i+1
=: Q
i+2
`Q
i+3
`···`Q
l
)
with answer substitution σ
1
···σ
i−1
σ
i
···σ
l−1
as given, where
E
i
= {|L
i
1
∨ R
i
1
,... ,L
i
m
i
∨ R
i
m
i
|}
P
i
=[p
i
] ◦
×
(R
i
∨ R
i
1
∨···∨R
i
m
i
)
E
i+1
= {|L
i+1
1
∨ R
i+1
1
,... ,L
i+1
m
i+1
∨ R
i+1
m
i+1
|}
P
i+1
=[p
i+1
] ◦
×
(R
i+1
∨ R
i+1
1
∨···∨R
i+1
m
i+1
) .
Then also a refutation D
0
of the same clause set exists, with the same start
clause, stable wrt. minimality, where the extension steps yielding Q
i+1
and
Q
i+2
are swapped. More precisely, D
0
takes the form
D
0
= Q
1
`···`Q
i−1
` [p
i
], [p
i+1
], Q
`
[p
i+1
],K
0
i
,P
i+1
→C
i+1
,hR
i+1
,σ
0
i
i,E
i+1
([p
i
], P
i+1
, Q)σ
0
i
=: Q
0
i+1
`
[p
i
σ
i
],K
0
i+1
,P
i
→C
i
,hR
i
,σ
0
i+1
i,E
i
(P
i
, P
i+1
, Q)σ
0
i
σ
0
i+1
=: Q
0
i+2
`Q
0
i+3
`···`Q
0
l
)
with computed substitution σ
1
···σ
i−1
σ
0
i
···σ
0
l−1
, and there is a substitution
δ
0
l
such that
Q
l
= Q
0
l
δ
l
, (A.31)
E
j
σ
j
···σ
i−1
σ
i
···σ
l−1
= E
j
σ
j
···σ
i−1
σ
0
i
···σ
0
l−1
δ
0
l
(for j =1,... ,i− 1, with E
j
as extending clauses)
E
i
σ
i
···σ
l−1
= E
i
σ
0
i+1
···σ
0
l−1
δ
0
l
E
i+1
σ
i+1
···σ
l−1
= E
i+1
σ
0
i
···σ
0
l−1
δ
0
l
E
j
σ
j
···σ
l−1
= E
j
σ
0
j
···σ
0
l−1
δ
0
l
(for j = i +2,... ,l− 1, with E
j
as extending clauses)
(A.32)
Furthermore, regularity is preserved (that is, if D is regular, then so is D
0
).
230 A. Appendix: Proofs
Both the statement and the proof of the lemma are an extension towards
theory-reasoning of the respective lemma for SLD-resolution in
[
Lloyd, 1987
]
,
with the additional complication that stability wrt. minimality is invariant.
Interestingly, the proof will not go through if stability wrt. minimality would
not hold for the given derivation.
Proof. Let L
i
= {|L
i
1
,... ,L
i
m
i
|} denote the extending literals of the “first
given” extension step. That is, K
i
= B
i
∪{|Leaf ([p
i
])|}∪L
i
, for some
B
i
⊆ p
i
\{|Leaf ([p
i
])|}. Analogously, let L
i+1
= {|L
i+1
1
,... ,L
i+1
m
i+1
|} de-
note the extending literals of the “second given” extension step. That is,
K
i+1
= B
i+1
σ
i
∪{|Leaf ([p
i+1
σ
i
])|}∪L
i+1
, for some B
i+1
⊆ p
i+1
\{|Leaf ([p
i+1
])|}.
We note that since L
i+1
stems from new variants we can assume that σ
i
does not act on L
i+1
, i.e.
L
i+1
= L
i+1
σ
i
. (A.33)
For both calculi variants this gives us
K
i+1
σ
i+1
= B
i+1
σ
i
σ
i+1
∪{|Leaf ([p
i+1
σ
i
σ
i+1
])|}∪L
i+1
σ
i+1
(A.33)
= B
i+1
σ
i
σ
i+1
∪{|Leaf ([p
i+1
σ
i
σ
i+1
])|}∪L
i+1
σ
i
σ
i+1
=(B
i+1
∪{|Leaf ([p
i+1
])|}∪L
i+1
| {z }
=:K
0
i
)σ
i
σ
i+1
.
(A.34)
We will swap the given two extension steps now, starting with the PTME-I
version. The second given extension step is based on the theory inference
K
i+1
⇒
P
i+1
→C
i+1
,σ
i+1
R
i+1
σ
i+1
. (A.35)
Since always new variants of inference rules are used, σ
i
will not act on the
new variant P
i+1
→ C
i+1
used in the given second step (and hence trivially
does not act on R
i+1
). In other words, P
i+1
→ C
i+1
=(P
i+1
→ C
i+1
)σ
i
.
Together with A.34 the theory inference A.35 can be reformulated as follows:
K
0
i
σ
i
⇒
(P
i+1
→C
i+1
)σ
i
,σ
i+1
R
i+1
σ
i
σ
i+1
.
This, however, is the same inference as
K
0
i
⇒
P
i+1
→C
i+1
,σ
i
σ
i+1
R
i+1
σ
i
σ
i+1
.
Now let
X =
i−1
[
j=1
(Var (K
j
σ
j
···σ
i−1
) ∪ Var (E
j
σ
j
···σ
i−1
))
W
i
= Var (p
i
) ∪ Var (p
i+1
) ∪ Var (E
i
) ∪ Var (E
i+1
) ∪ Var (Q) ∪
Var (R
i
) ∪ X
A.1 Proofs for Chapter 4 — Theory Reasoning 231
and apply Lemma A.1.10 (it is easily verified that the preconditions are met).
It gives us the theory inference
K
0
i
⇒
P
i+1
→C
i+1
,σ
0
i
R
i+1
σ
0
i
with multiset-MGU σ
0
i
, and a substitution γ
0
i
such that
σ
i
σ
i+1
= σ
0
i
γ
0
i
[W
i
] (A.36)
R
i+1
σ
i
σ
i+1
= R
i+1
σ
0
i
γ
0
i
. (A.37)
Hence, a PTME-I-Ext step can be carried out to Q
i
, yielding Q
i+1
, as sug-
gested.
In case of TTME-MSR, by definition of TTME-MSR-Ext, σ
i+1
is a minimal
T -MGR for K
i+1
. From A.34 we learn that σ
i
σ
i+1
is a, although minimal,
not necessarily most general T -refuter for K
0
i
. However, with Proposition 4.4.1
we conclude that there is a T -MGR σ
0
i
∈ MSR
T
(K
0
i
), and that there is a
substitution γ
0
i
such that
σ
i
σ
i+1
= σ
0
i
γ
0
i
[W
i
] . (A.38)
By Proposition 4.2.1.2 we know that with σ
i
σ
i+1
being a minimal T -MGR,
the more general σ
0
i
is a minimal T -MGR for K
0
i
, too. Hence, a TTME-MSR-
Ext step can be carried to Q
i
, yielding Q
i+1
as suggested.
For both variants recall that the extending clauses always are new vari-
ants; hence we clearly have Var (E
i
) ∩ Var (K
0
i
)=∅. For TTME-MSR, by
definition of MSR
T
we know that Dom(σ
0
i
) ⊆ Var (K
0
i
). Thus, Dom(σ
0
i
) ∩
Var (E
i
)=∅, and in particular, σ
0
i
will not act on the variables of L
i
.For
PTME-I, we can assume that Dom(σ
0
i
) ⊆ Var (K
0
i
)∪Var (P
i+1
→ C
i+1
). With
P
i+1
→ C
i+1
being a new variant, we can further assume that σ
0
i
does not
act on the variables of L
i
, and that σ
0
i
will not act on the variables of the
new variant P
i
→ C
i
. The latter fact implies in particular
R
i
= R
i
σ
0
i
. (A.39)
For both variants, let
W
i+1
= Var (p
i
σ
0
i
) ∪ Var (p
i+1
σ
0
i
) ∪ Var (E
i
σ
0
i
) ∪ Var (E
i+1
σ
0
i
)
∪ Var (Qσ
0
i
) ∪ Var (R
i+1
σ
0
i
) ∪ Var (Xσ
0
i
).
Next we will show how to append the given first inference step to Q
0
i+1
.
Again, we start with PTME-I: the given first PTME-I-Ext step is based on
the following theory inference:
K
i
⇒
P
i
→C
i
,σ
i
R
i
σ
i
.
Clearly, we can instantiate with σ
i+1
, yielding
232 A. Appendix: Proofs
K
i
⇒
P
i
→C
i
,σ
i
σ
i+1
R
i
σ
i
σ
i+1
. (A.40)
We know by minimality requirement of theory inferences that K
i
σ
i
contains
no duplicates. By the given stability wrt. minimality of D, it holds even the
stronger result that K
i
σ
i
σ
i+1
contains no duplicates. Thus A.40 is a minimal
theory inference (although σ
i
σ
i+1
need not be a multiset-MGU).
Recall from above that σ
0
i
will not act on the variables of L
i
. Hence we
have
K
i
σ
i
σ
i+1
(A.36)
= K
i
σ
0
i
γ
0
i
=(B
i
∪{|Leaf ([p
i
])|}∪L
i
)σ
0
i
γ
0
i
=(B
i
σ
0
i
∪{|Leaf ([p
i
σ
0
i
])|}∪L
i
| {z }
=:K
0
i+1
)γ
0
i
.
Recall further from above that σ
0
i
will not act on the variables of P
i
→ C
i
.
Hence we have
(P
i
→ C
i
)σ
i
σ
i+1
(A.36)
=(P
i
→ C
i
)σ
0
i
γ
0
i
=(P
i
→ C
i
)γ
0
i
.
Altogether, A.40 can be rewritten to the minimal theory inference
K
0
i+1
⇒
P
i
→C
i
,γ
0
i
R
i
γ
0
i
.
Now we can apply Lemma A.1.10 (again, it is easily verified that the precon-
ditions are met), which gives us the theory inference
K
0
i+1
⇒
P
i
→C
i
,σ
0
i+1
R
i
σ
0
i+1
with multiset-MGU σ
0
i+1
and a substitution γ
0
i+1
such that
γ
0
i
= σ
0
i+1
γ
0
i+1
[W
i+1
] (A.41)
R
i
γ
0
i
= R
i
σ
0
i+1
γ
0
i+1
. (A.42)
Hence, a PTME-I-Ext step can be carried out to Q
0
i+1
, yielding Q
0
i+2
,as
suggested.
Now we turn to TTME-MSR. From the given first extension step we know
that K
i
σ
i
is minimal T -complementary. By Proposition 4.2.1.1 we know that
K
i
σ
i
σ
i+1
also is T -complementary. We need the stronger result that σ
i
σ
i+1
is even a minimal T -refuter for K
i
, which holds because D is given as stable
wrt. minimality. Thus
K
i
σ
i
σ
i+1
(A.38)
= K
i
σ
0
i
γ
0
i
is minimal T -complementary. Recall from above that σ
i
will not act on the
variables of L
i
. Hence we continue
A.1 Proofs for Chapter 4 — Theory Reasoning 233
K
i
σ
0
i
γ
0
i
=(B
i
∪{|Leaf ([p
i
])|}∪L
i
)σ
0
i
γ
0
i
=(B
i
σ
i
∪{|Leaf ([p
i
σ
i
])|}∪L
i
| {z }
=:K
0
i+1
)γ
0
i
.
Hence, with σ
i
σ
i+1
being a minimal T -refuter for K
i
, γ
0
i
is also a minimal
T -refuter for K
0
i+1
. By Proposition 4.4.1 we conclude that a T -MGR σ
0
i+1
∈
MSR
T
(K
0
i+1
) exists, and that a substitution γ
0
i+1
exists such that
γ
0
i
= σ
0
i+1
γ
0
i+1
[W
i+1
] . (A.43)
By Proposition 4.2.1.2 we know that with γ
0
i
being a minimal T -MGR for
K
0
i+1
, the more general σ
0
i+1
also is a minimal T -MGR for K
0
i+1
. Hence, a
TTME-MSR-Ext step can be carried to Q
0
i+1
, yielding Q
0
i+2
as suggested.
This shows us that the first and second extension step can be swapped.
We are going to show now Q
i+2
= Q
0
i+2
γ
0
i+1
4
. As an abbreviation we use
R
i
= R
i
1
∨···∨R
i
m
i
:
Q
i+2
=(P
i
, P
i+1
, Q)σ
i
σ
i+1
=([p
i
] ◦
×
(R
i
∨ R
i
), [p
i+1
] ◦
×
(R
i+1
∨ R
i+1
), Q)σ
i
σ
i+1
=([p
i
] ◦
×
(R
i
∨ R
i
), [p
i+1
] ◦
×
(R
i+1
∨ R
i+1
), Q)σ
0
i
γ
0
i
(by A.36 and A.37 (PTME-I),
by A.38 (TTME-MSR))
=([p
i
] ◦
×
(R
i
∨ R
i
), [p
i+1
] ◦
×
(R
i+1
∨ R
i+1
), Q)σ
0
i
σ
0
i+1
γ
0
i+1
(by A.41, A.42 (PTME-I),
by A.43 (TTME-MSR))
=(P
i
, P
i+1
, Q)σ
0
i
σ
0
i+1
γ
0
i+1
= Q
0
i+2
γ
0
i+1
.
Hence we can write the rest of the given derivation D as
D
R
= Q
0
i+2
γ
0
i+1
`Q
i+3
`···`Q
n
.
We wish to lift D
R
to a derivation D
0
R
starting with Q
0
i+2
, which would yield
the tail of the desired refutation D
0
. This requires a slight generalization
of the lifting lemma (Lemma A.1.9) by allowing to start derivations with
any instantiated branch set, instead of a branch set corresponding to a start
clause. In this case, Q
0
i+2
γ
0
i+1
will be lifted to a refutation
D
0
R
= Q
0
i+2
`Q
0
i+3
`···`Q
0
n
.
Further, this lifting preserves regularity which implies the regularity of D
0
,
provided that D is regular.
4
It can even be shown that for some γ
i+1
it holds Q
0
i+2
= Q
i+2
γ
i+1
. That is, Q
0
i+2
and Q
i+2
are variants. However, as the further proof shows, this argumentation
is not necessary.
234 A. Appendix: Proofs
We still have to show that in D
0
is stable wrt. minimality. By the identities
derived so far we can obtain the following (j =1,... ,i− 1):
K
j
σ
j
···σ
i−1
σ
0
i
σ
0
i+1
γ
0
i+1
= K
j
σ
j
···σ
i−1
σ
i
σ
i+1
K
0
i
σ
0
i
σ
0
i+1
γ
0
i+1
= K
i+1
σ
i+1
(by A.34, A.36 and A.41 (PTME-I),
by A.34, A.38 and A.43 (TTME-MSR))
K
0
i+1
σ
0
i+1
γ
0
i+1
= K
i
σ
i
σ
i+1
(by Def. of K
0
i+1
and A.41 (PTME-I),
resp. A.43 (TTME-MSR)) .
In words, the left sides of the equations are just the key sets in D
0
up to Q
0
i+2
,
instantiated by the computed answer substitution derived so far and γ
0
i+1
.
Now consider, for instance, K
0
i
σ
0
i
σ
0
i+1
γ
0
i+1
(for the other listed key sets
the following argumentation is the same). In D
R
, this set is further instanti-
ated towards K
0
i
σ
0
i
σ
0
i+1
γ
0
i+1
σ
i+2
···σ
l−1
. Again slightly generalizing the lifting
lemma, the computed answer in D
0
R
,sayσ
0
i+2
···σ
0
l−1
, leaves us more general
key sets. The lifting lemma also gives us a substitution δ
0
l
such that
K
0
i
σ
0
i
σ
0
i+1
σ
0
i+2
···σ
0
l−1
δ
0
l
= K
0
i
σ
0
i
σ
0
i+1
γ
0
i+1
σ
i+2
···σ
l−1
= K
i+1
σ
i+1
σ
i+2
···σ
l−1
.
Now, the given stability wrt. minimality of D means in particular that
K
i+1
σ
i+1
σ
i+2
···σ
l−1
contains no duplicates. But then K
0
i
σ
0
i
σ
0
i+1
σ
0
i+2
···σ
0
l−1
trivially cannot contain duplicates either. Using this argumentation for all
the key sets listed above convinces us that D
0
is stable wrt. minimality, too.
For the other properties A.31 and A.32 the same argumentation as for
the key sets applies and hence is omitted.
Proposition A.1.3 (Independence of the Computation Rule). Let P
be a program, ← Q be a query (cf. Def. 3.2.5) and D be a PTME-I refuta-
tion (resp. TTME-MSR refutation) of P and ← Q with computed answer
{Q
1
,... ,Q
l
}. Assume that D is stable wrt. minimality (Def. 4.5.7, resp.
Def. 4.4.4).
Then, for any computation rule c, a PTME-I refutation (resp. TTME-
MSR refutation) D
0
of P and ← Q exists with computed answer {Q
0
1
,... ,Q
0
l
}
via c, and, for some substitution δ
0
, it holds that {Q
0
1
,... ,Q
0
l
}δ
0
= {Q
1
,... ,Q
l
}.
Furthermore, regularity is preserved. That is, if D is strictly regular, then
so is D
0
.
Proof. Let
D = Q
1
`···`Q
i−1
`Q
i
`··· ` (2 = Q
l
)
be the given refutation, and suppose that D is in accordance with c up to
inclusive i − 1. That is, c selects a branch [p
i
] ∈Q
i
different from the actual