Baumgartner P. Theory Reasoning in Connection Calculi

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

94 4. Theory Reasoning in Connection Calculi

a<b

b<c

a<b

b<c

a<e

a<b

b<c

a<e

a<b

b<c

∨c<d ∨

Residue: ha<e,i

Key set:

∨d<e ∨

a<e

∨e<a ∨

Partial Theory Extension Total Theory Extension

Key set:

Residue: h2,i

Figure 4.6. Two inference steps of TTCC-Link. The same setup is used as in

Figures 4.2 and 4.3.

TME-Ext

∨ R

Residue: hR,σi

···R

Figure 4.7. A partial theory model elimination extension step.

4.3 Theory Model Elimination — Semantical Version 95

elimination (TTME-Sem) only total TME-Sem-Ext steps are allowed. The

term partial theory model elimination (PTME-Sem) is used interchangeably

with TME-Sem in order to emphasize that partial steps are allowed.

In the weak version of this calculus, we do not insist on minimality of

T -residues and only require that in TME-Sem-Ext inferences hR,σi is a T -

residue for K.

Notice again that PTME-Sem includes TTME-Sem by the possibility of total

steps. Thus, in order to make the PTME-Sem framework meaningful, some

ways of restricting the total/partial inferences are necessary. To this end, we

will propose the device of “theory inference systems” in Section 4.5.

Notice that unlike in TTCC-Link-Ext inferences in the connection calculus,

the extending literals L

,... ,L

are absent in the subtree below the selected

branch. This change requires the case analysis in the TME-Sem-Ext inference

rule in order to obtain a proper literal tree.

The partial version “PTCC-Link” of TTCC-Link would be deﬁned in

much the same way as was carried out for TME-Sem. This could be done for

both, the connection calculus with link condition, and without link condition.

We feel, however, that no new insight would be gained from this. Hence it is

omitted.

Note 4.3.1 (Minimality). As for TTCC-Link above, the minimality require-

ment for T -residues is also motivated by lifting the link-condition of ME to

the theory case. Concerning the partial version, we can relax the minimality

requirement in a certain way (Section 4.5) and use the weak version. How-

ever, as the discussion in Note 4.4.3 below shows, this is not possible for the

total version.

4.3.3 Relation to TTCC-Link

We will now return to the issues addressed in the motivation section above

(Section 4.3.1). We start with characterizing the diﬀerences to its predecessor

TTCC.

Theorem 4.3.1 (TTCC-Link simulates TTME). For every TTME-Sem

derivation D of a clause set M there is a TTCC-Link refutation D

of M of

the same length which is a stepwise simulation of D. More precisely, if

D = P

`···`P

then a TTCC-Link derivation

= P

`···`P

exists, such that bijective functions exists f

(1 ≤ i ≤ n) from the open

branches of P

onto the open branches of P

(when read as branch sets) such

that for every [b] ∈P

we have

96 4. Theory Reasoning in Connection Calculi

1. f

([b]) ⊇ b, and

2. Leaf ([f

([b])]) = Leaf ([b]) .

The converse does not hold. More precisely, there is a theory T and a clause

set

M(n) such TTCC-Link admits a refutation of length O(n), and the

shortest TTME-Sem refutation is of length O(2

Proof. The TTCC-Link refutation starts with the same start clause, and

every TTME-Sem-Ext inference (with T -residue h2,σi) can be simulated by

a TTCC-Link-Ext inference using the same set of extending clauses, same

key set and T -refuter σ, applied to the open branch corresponding to the

selected branch in the TTME-Sem refutation. By a “corresponding branch”

in the TTCC-Link refutation we mean a branch which contains at inner node

positions the same or more literals than a branch in the correspondingly

derived TTME-Sem tableau.

More formally, suppose that f

is already deﬁned appropriately for P

and

, and suppose that

], Q

| {z }

],K

,σ

,{|L

∨R

,...L

∨R

(P, Q

)σ

| {z }

i+1

where

P =

(

]× if R

∨···∨R

= 2,

] ◦ (R

∨···∨R

) else,

The corresponding TTCC-Link-Ext inference then is

], Q

| {z }

,σ

,{|L

∨R

,...L

∨R

([p

] ◦ R

, [p

· L

] ◦ R

, ... ,[p

· L

···L

n−1

] ◦ R

, [p

· L

···L

n−1

· L

]×, Q

)σ

| {z }

i+1

where [p

]=f

([p

]). Obviously, because of f

([p

]) ⊇ p

and Leaf ([f

([p

])]) =

Leaf ([p

]) the key set K of the TTME-Sem-Ext inference can be used in the

TTCC-Link-Ext as well. Hence, this inference exists. Finally deﬁne

i+1

([b]) =











([b]) for [b] ∈Q

· L

···L

j−1

· X] for [b]=[p

· X] ∈P , where

X ∈ R

with R

6= 2 (i ≤ j ≤ n).

Thus, it is only the extending literals which are missing in the TTME-Sem

derivation.

By M(n) a function is meant which gives a clause set depending on n.

4.3 Theory Model Elimination — Semantical Version 97

It is due to this observation that the converse of the theorem does not

hold. The presence of an extending literal in a branch can be used in the

subtree below it. We construct a clause set in such a way that the usage of

such a literal, say L, in TTCC-Link has to be replaced by extending with

clause L∨R, where R contains at least two literals. This will cause exponential

growth when applied recursively.

The clause set is as follows:

R(a) ←

)

R(f(a)) ← (R

)

R(f(f(x))) ← R(f(x)),R(x) (R

)

Q(f(x)) ← P (f (x)),R(f(x)),R(x) (Q)

P (f

(a)) ← (P

)

← P (f(a)) (G)

The notation “f

(x)” means the term for n-fold application of f to x.Of

course, the clauses (R

),(R

) and (R

) encode the recursion scheme of the

Fibonacci function, which is of exponential complexity wrt. its argument.

As theory we choose:

∀x (R(f(x)) ∧ Q(f (x)) → P (x)) .

We start the refutations with start clause (G). The TTME-Sem refutation is

completely deterministic, in the sense that for any open branch there exists

exactly one set of extending clauses with exactly one key set such that a

TTME-Sem-Ext step is applicable.

For TTCC-Link the situation is a bit diﬀerent. The set of extending

clauses and key sets is determined as in the TTME-Sem case. However, there

is a choice concerning the order in which the extending clauses are fanned

below the extended branch. Figure 4.8 contains a snapshot.

Consider the tableau

1 .Inoneoptimal policy, which we chose to prove

the theorem, extension of branches with leaf ¬P (f

(a)) is carried out with

clauses (R

) and (Q) in that order. This results in a tree shaped as indicated

2 . Notice that all underlined R-literals can be closed by reduction steps,

or at the top of the tree by extension with the unit clauses (R

) and (R

To summarize, in this policy there is no fanning below the R-literals, which

gives us constant breadth (namely 3 or 4) in every level. Since the depth is of

order O(n) we conclude that in sum there are O(n) extension steps necessary

to ﬁnd a refutation.

The situation becomes entirely diﬀerent if a diﬀerent policy for extension

steps is used. This is depicted in tree

3 , where extension of branches with leaf

¬P (f

(a)) is carried out with clauses (Q) and (R

) in that order. Notice that

98 4. Theory Reasoning in Connection Calculi

Extension

Strategies

Key set

Closes without

extending clause

R(f

i+1

(a)) ¬R(f

i−1

(a))

(Q)(R

)

(Q)(R

)

¬P (f

(a))

¬P (f

i+1

(a)) ¬R(f

(a))¬R(f

i+1

(a))Q(f

i+1

(a))

¬P (f

i−1

(a))

¬P (f

(a))

R(f

(a))

R(f

i+1

(a)) ¬R(f

i−1

(a))

¬P (f

i+1

(a)) ¬R(f

(a))¬R(f

i+1

(a))

Q(f

i+1

(a))

¬P (f

(a))?

Figure 4.8. A snapshot from the refutation constructed in the proof of Theo-

rem 4.3.1. Starting from tableau

1 two diﬀerent tableau can be obtained, depend-

ing from the order of fanning the extended clauses.

4.3 Theory Model Elimination — Semantical Version 99

this policy leaves us with negative R literals

which cannot be closed using

ancestor literals, because no positive R literals are present. Hence, every such

negative R literal has to be “solved” by the clauses (R

), (R

) and (R

) which

is well-known to be of exponential complexity. In particular, the subproof of

the upcoming leaf ¬R(f

(a)) alone requires O(2

) extension steps.

Since, furthermore, in this policy no extension steps using the Q literals

are possible, the refutation behaves as if these Q literals were not present at

all. In other words, TTME-Sem will construct precisely the same refutation,

except for the absence of these irrelevant Q literals. Thus, a TTME-Sem

refutation will also require O(2

) extension steps.

It is obvious that the proof of this theorem does not depend on whether total

or partial extension steps are considered. The crucial point is the diﬀering

ancestor context of TTCC-Link and TTME-Sem. Hence we take it for granted

that a respective theorem for the partial variants of the theory connection

calculus could be established after proper deﬁnition.

Note 4.3.2 (Combining TTCC-Link and TME-Sem). As the previous theo-

rem reveals, there is a tradeoﬀ between TTCC-Link and TME-Sem: TME-

Sem needs fewer ancestor literals (recall that wrt. TTCC-Link the extending

literals in inference steps are absent) and hence has less local search space

than TTCC-Link. On the other side, proofs may become shorter with addi-

tional branch literals. This can overweigh the additional local search space.

As a drastic example of this, recall the example contrived in the proof of

counter direction of Theorem 4.3.1.

As a conclusion I propose a “best of both worlds” approach and to base

a proof procedure on a combination of both calculi: from TME-Sem one

learns that in inferences the order of extending clauses plays no rˆole, giving

us a don’t-care non-determinism instead of the don’t-know nondeterminism

of TTCC-Link.

Also from TME-Sem we learn that the extending literals need not be

included in extended tableau. On the other hand, from TTCC-Link we learn

that they sometimes result in shorter refutations. An approach somewhere in

the middle would be to include them, but to restrict the use as substitutes for

otherwise equal extending literals in subsequent extension steps. By this, the

local search space is not even increased yet saving some extending clauses.

On the other side, however, in experiments with our PROTEIN prover it

was my impression that in practice no signiﬁcant diﬀerence arises for most

examples.

We are now in a good position to judge whether TME-Sem marks any

progress in solving the issues addressed in the beginning of this section.

Here, by an “X literal” we mean a literal of the form X(f

(a)) (or its negation),

for some j.

100 4. Theory Reasoning in Connection Calculi

Order of Extending Clauses. Using Theorem 4.3.1 the sample TTCC-Link-Ext

inferences on page 91 correspond to the following two TTME-Sem-Ext steps:

[¬A] `

[¬A],{|¬A,B,C|},{|B∨E, C∨¬D|}

[¬A · E], [¬A ·¬D]

vs. [¬A] `

[¬A],{|¬A,B,C|},{|C∨¬D, B∨E|}

[¬A ·¬D], [¬A · E].

Notice that the resulting TME tableau are the same, because the resulting

branch sets, when appropriately ordered (cf. Def. 3.2.1) are the same. It is

obvious from the deﬁnition of TME-Sem-Ext that this property holds on the

general level.

The practical relevance of this observation is that a proof procedure need

never backtrack on the ordering of the extending clauses. Again, this is not

obvious for TTCC-Link, as switching the order of extending clauses results

in branch sets with diﬀerent ancestor contexts. However, in combination with

the simulation result of Theorem 4.3.1, we now learn that also for TTCC-Link

the ordering of extending clauses plays no rˆole.

Deﬁnite Theories. Consider again the example on Page 90 concerning deﬁnite

theories. The total step given there corresponds to a TTME-Sem-Ext step

[¬A] `

[¬A],{|B,C|},{|B, C∨¬D|}

[¬A ·¬D] .

Notice that now the extending literals are no longer contained as labels of

nodes in the resulting TME tableau. We will show that this is not by coin-

cidence. For this, recall that TME-Sem-Ext inferences are based on minimal

T -complementary key sets; their structure is characterized by the next propo-

sition:

Proposition 4.3.1. Let T be deﬁnite theory. Then any minimal T -comple-

mentary literal set (or multiset) contains exactly one negative literal.

Proof: See Appendix A, page 212. The practical relevance of this Proposition

is that the search for key sets in TTME-Sem-Ext inferences can be syntacti-

cally guided to some degree, even if the input clause set is non-Horn. For the

Horn case we can further restrict syntactically:

Proposition 4.3.2. Let T be a deﬁnite theory, and D be a PTME-Sem

derivation from a Horn clause set M with some negative clause from M

as start clause. Then the key set K in every TME-Sem-Ext inference step in

D satisﬁes the following properties (in terms of Def. 4.3.2):

1. The leaf K of the extended branch [p · K] is a negative literal (as well as

all other literals in p), and

2. B = {||}, i.e. no ancestor literals from [p] are used, and

3. L

,... ,L

are positive literals, and

4. R = 2 or R consists of negative literals only.

4.4 Total Theory Model Elimination — MSR-Version 101

Thus the search for appropriate key sets is limited to positive literals and one

single negative literal, which is given as the leaf; further, as B = {||}, these

positive literals are entirely taken from the extending clauses, but not from

the selected branch. Notice that this is indeed the result which was desired

above.

As a further consequence, “reduction steps” are not possible in case of

the empty theory (which is trivially a deﬁnite theory). Thus we have a gen-

eralization of the corresponding well-known property of non-theory ME.

Proof. Any TME-Sem-Ext step for deﬁnite theories applied to a branch with

negative leaf must have properties 2, 3 and 4, because otherwise Proposi-

tion 4.3.1 would be violated. For the same reason all branch literals B must

be positive. Thus, in order to show that B = {||} it suﬃces to show that along

D for every branch set P

the following invariant holds: every branch in P

is purely negative, i.e. it is of the form [¬A

···¬A

]. Further, this invariant

also gives us that Leaf ([P ]) is negative, as desired.

The invariant is certainly true for the ﬁrst branch set P

corresponding

to the the start clause.

Now suppose a TME-Sem-Ext step is applied to some branch [¬A

···¬A

By Proposition 4.3.1 the key set of a theory extension step contains exactly

one negative literal, which must be the extended literal ¬A

. The remaining

literals L

are positive and must hence be drawn from input clauses L

∨ R

With every literal L

being the sole positive literal in the clause (we are given

that M is Horn) it follows that [¬A

···¬A

] is extended only with negative

literals. Hence the invariant follows, and thus also the proposition follows.

Regularity. In Section 4.3.1 we motivated the transition from TTCC-Link

to TTME-Sem also by the possibility of obtaining a complete calculus with

regularity restriction (more precisely, the completeness of TTCC-Link with

regularity is still open). Indeed, complete versions of TTME and PTME with

regularity exist. For TTME, we will give a direct completeness proof below,

which will be used as a base for the completeness proof of a speciﬁc version

of PTME.

These versions shall be introduced in the next two sections.

4.4 Total Theory Model Elimination — MSR-Version

Following standard results for non-theory model elimination, we would like

to carry out derivations employing most general substitutions. This is not yet

achieved with TME-Sem and thus will be subject of this section. We will con-

sider the total version of TME-Sem for this, and the resulting calculus will be

called TTME-MSR (standing for Total T heory M odel E limination — M ost

general Set of Refuters). The necessary changes can essentially be restricted

to ﬁltering out non-most general elements from the set of T -refuters for a

102 4. Theory Reasoning in Connection Calculi

given key set. The underlying concept is called a complete set of T -refuters

and will be treated next. After that, the deﬁnition of TTME-MSR will be

stated and its answer completeness will be proven. Finally, the approach

is illustrated by instantiating the background reasoner with “terminological

reasoning”.

4.4.1 Complete and Most General Sets of T -Refuters

In non-theory calculi, complementarity of literals is usually established by

means of a MGU (most general uniﬁer, cf. Def. 2.4.5). For the sake of eﬃ-

ciency, computing at the most general level is also a desirable goal within

theory reasoning. However, in the theory case uniﬁers need no longer be

unique; the concept of an MGU has to be replaced by a more general con-

cept. In the case of purely equational theories the concept of “complete set

of uniﬁers” is well-known

[

Siekmann, 1989; Snyder, 1991

]

Since we deal with arbitrary universal theories and not just equational the-

ories we still have to be a bit more general. This concept, which is formulated

in a dual way, builds on the concept of T -refuters (Def. 4.2.2) and is called a

complete set of T -refuters. Further, care must be taken for T -refuters in that

they shall not introduce variables which are bound in the context where they

are applied. The next deﬁnition accounts for this by means of “protected”

variables.

Deﬁnition 4.4.1 (Complete Set of T -refuters). A set U of substitutions

is a complete set of T -refuters for M away from a set of variables V with

Var (M) ∩ V = ∅ iﬀ

1. for all σ ∈ U, Mσ is T -complementary, i.e., σ is a T -refuter for M

(Correctness), and

2. for all σ ∈ U, Dom(σ) ⊆ Var (M) and VCod(σ) ∩ (V ∪ Dom(σ)) = {}

(Purity), and

3. for all T -refuters σ

for M there is a σ ∈ U such that σ ≤ σ

[Var (M)]

(Completeness).

The set U is denoted by CSR

(M)[V ]; V is referred to as the set of protected

variables.

By a complete T -uniﬁcation procedure mean an eﬀective procedure which

enumerates a set CSR

(M)[V ] for any ﬁnite M and V with Var(M)∩V = ∅.

The necessity for the correctness item is obvious. The ﬁrst conjunct of purity

restricts the domain of σ to the variables occurring in the problem. This is

obviously no real restriction for any T -uniﬁcation procedure, as assignments

of σ outside the scope of the problem M can always be discarded without

modifying its eﬀect on M. The second conjunct of purity means that σ will

neither introduce variables which are protected by V nor variables which are

from the domain of σ. The latter property just characterizes idempotency (see

e.g.

[

Lloyd, 1987

]

). Thus, we have for any x ∈ VCod (σ) either x ∈ Var (M)

4.4 Total Theory Model Elimination — MSR-Version 103

or otherwise x/∈ V . In the latter case we will say that x is an extra variable

introduced by σ .

Concerning the completeness item, it should be noted that the restriction

to Var (M)

is crucial for the theory-case (again, it is not needed in the

non-theory case). For instance, let the theory be given by the clause set

{¬p(f(x))}. Consider M = {|p(z)|}. Clearly, σ = {z ← f(a)} is a T -refuter

for M. A most general T -refuter is σ

= {z ← f(y)}. However, it does not

hold that σ

≤ σ, because we would have to have δ = {y ← a} in order to

have p(z)σ

δ = p(z)σ. But then, clearly, yσ

δ 6= yσ which gives us σ

δ 6= σ

and, more generally, σ

6≤ σ. However it holds σ

≤ σ [Var (M)] as expected.

Note 4.4.1 (Need for Protected Variables.). We will argue here for the need

to protect variables and prove a calculus not using it as incomplete.

Protected variables are not needed in the case of syntactical uniﬁcation.

The reason is, that the usual uniﬁcation algorithm will not introduce extra

variables. In order to see the importance of protected variables in the theory

case consider M = {|p(x)|}, and suppose that p(x) occurs in a derivation which

has also q(x, z) in its context. Further suppose that a T -refuter σ

= {x ←

f(a)} is applied in this derivation. This yields p(f(a)) and q(f(a),z) wrt.

context. For lifting purposes suppose now that σ = {x ← f(z)} is a more

general T -refuter. However, then we have to ﬁnd δ = {z ← a} in order to

obtain σ

= σδ [{x}]. Although p(x)σδ = p(f(a)) = p(x)σ

, we have, with

regard to the context,

q(x, z)σδ = q(f (a),a) 6= q(f(a),z)=q(x, z)σ

. (4.2)

Thus, we would have had to set the protected variables V = {z} and to ﬁnd

a T -refuter from CSR

({|p(x)|})[{z}].

Note our demand that the variables from Var (M) must — by deﬁnition

— never be protected. Such a restriction is not present e.g. in

[

Snyder, 1991

]

The advantage of our approach is that the T -refuters are allowed to introduce

variables already contained in the problem statement; it relieves the uniﬁca-

tion algorithm of always unnecessarily inventing new variables. Sometimes

this would result in very “unnatural” and unexpected results. For instance,

if p(x) and ¬p(f(y)) are to be uniﬁed syntactically, we would like to have

σ = {x ← f(y)} as a T -refuter. However, this would not be possible if y is

protected. In this case, a suitable T -refuter would be σ

= {x ← f(z),y ← z}

(provided that z is not protected). Note that the usual uniﬁcation algorithm

(see e.g.

[

Lloyd, 1987

]

)isnot capable of computing such a substitution and

thus cannot be used in applications which need to protect variables in the

problem statement.

Substantial problems arise when protection of variables is not used. More

speciﬁcally, the lifting proof below needs at its very heart equivalences of the

form stated in (4.2) and will thus not work with the proposed substitution σ.

Alternatively, the restriction to Var (σ

) should do as well.