Baumgartner P. Theory Reasoning in Connection Calculi

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

164 5. Linearizing Completion

2. i.j.r ∈ P (D)if

a) D is of the form L

==⇒L

...L

=⇒L

i+1

...L

==⇒L

n+1

where 1 ≤

i ≤ n,

b) and D

is a sequence of the form D

···D

j−1

j+1

···D

where

1 ≤ j ≤ k

c) and r ∈ P (D

)

Building on positions, subderivations can be introduced: let D be a deriva-

tion and p ∈ P (D). The (occurrence of a) subderivation of D at position p,

is deﬁned recursively as follows:











D if p = λ

if p = i.j.r and D is of the form

==⇒L

...L

=⇒L

i+1

...L

n−1

===⇒L

where D

= D

···D

For instance, take

X =(A

=⇒D

=⇒FG=⇒H

==============⇒ I)

then X|

1.1

=(B

=⇒ D

=⇒ F ), X|

1.2

=(G=⇒ H) and X|

1.1.2.1

= E.

For ease of notation we abbreviate the selection of an immediate sub-

derivation (D|

a,b

of a subderivation D|

to D|

p,a,b

. In words, ﬁrst p is

used to locate a subderivation in D and then this subderivation is returned

in between the indices a and b. For instance X|

1.1,2,3

=(D

=⇒ F ) and

1.2,1,1

= G.

Next we turn to replacement of derivations. Suppose D is an I-derivation

from M, and suppose E is an J -derivation from N. Furthermore suppose

that D|

p,a,b

and E have the same top literal and derived literal, respectively.

Then the sequence which results from replacing D|

p,a,b

in D by E, written

as D[E]

p,a,b

, evidently is an I∪J-derivation from M ∪ N with same top and

derived literal as in D.

For instance,

X[D

=⇒ M

=⇒ F ]

1.1,2,3

=(A

=⇒D

=⇒M

=⇒FG=⇒H

==================⇒ I)

More formally, replacement is deﬁned as follows:

D[E]

p,a,b











1,a

· E · D|

b,n

, if p = λ

1,i

· (L

=⇒

→C

,δ

i+1

) · D|

i+1,n

if p = i.j.r

where D

= D

···D

j−1

[E]

j+1

···D

5.3 Orderings and Redundancy 165

5.3 Orderings and Redundancy

The transformation systems deﬁned below allow for the deletion of redundant

inference rules. Redundancy in turn is based on orderings for derivations.

Hence these notions have to be introduced ﬁrst.

5.3.1 Orderings on Nested Multisets with Weight

Section 2.1 contains standard deﬁnitions concerning orderings. Here we are

concerned with a certain kind of multisets and orderings on them.

A multiset with weight over a set X is a tuple hN,wi, also written as

(or {|...|}

) where N is a multiset over X and w ∈ IN. Thus, a multiset

with weight is obtained from an ordinary multiset by attaching some integer

to it. As a recursive generalization, deﬁne a nested multiset with weight over

a set X as either an element from X or else as a multiset with weight over

a nested multiset with weights. For instance, {|a, {|b, c, {|d|}

,e|}

is such a

set over {a, b, c, d, e}. They will be used as a complexity measure for proofs

below.

Since multisets with weight are tuples, they can be compared lexicograph-

ically. The resulting ordering 

MW,

over multisets with weight over a set

X of terms, base ordering  on terms and the usual ordering > on integers

then reads as follows:



MW,

=(M 



N or else (M = N and v>w))

where M

, N

are multisets with weights over X. Thus we ﬁrst compare

the set-components; if these are equal then the weight gives the decision. It

is clear that with the well-founded orderings 



and > the lexicographic

extension 

MW,

also is well-founded.

Orderings on multisets can be generalized to nested multisets

[

Dershowitz

and Manna, 1979

]

. For our purposes we have to go a little further and to

compare nested multisets with weight over a set of constants C. This ordering

is nothing but a recursive path ordering with status (see e.g.

[

Steinbach,

1990

]

) where the multiset constructor “{|.|}” is given a multiset status, and

the tuple-constructor hN,wi (to attach weights to multisets) is given a left-

right status. The proof of proposition 5.3.1 below will make this more precise.

Deﬁnition 5.3.1 (Nested Multisets with Weight). Let C be a ﬁnite set

of constants, ordered by the well-founded ordering , and let W ⊂ IN be

a ﬁnite set of weights. Deﬁne the nested multiset ordering with weights,



NMW,

, recursively as follows:

166 5. Linearizing Completion

1.X= {|x

,... ,x



NMW,

{|y

,... ,y

= Y

if (1.1) x





NMW,

Y for some i =1...m,

or (1.2) X 

MW,

NMW,

Y and v, w ∈ W,

(i.e. 

MW,

NMW,

is the recursive extension

of 

NMW,

to multisets with weight).

2.X= {|x

,... ,x



NMW,

if y ∈ C and x





NMW,

y for some i =1...m

3.x

NMW,

if x, y ∈ C and x  y.

Most often we will write 

NMW

instead of 

NMW,

when  is clear from

the context.

Example 5.3.1. Let C = {a, b} with a  b, and W = {0,... ,10}. It holds

{|a, {|a, {|a|}



NMW,

{|b, {|a, a |}

This is, because with a 

NMW,

b (by 3.) and

{|a, {|a|}



NMW,

{|a, a|}

(5.1)

case 1.2. applies (we replaced in a multiset with weight two elements by

smaller ones, hence increasing the weight from 3 to 6 does not matter). We

still have to show Equation 5.1. It holds {|a|}



NMW,

a by 2., and hence

for the multiset extension,

{|a, {|a|}

|}



NMW,

{|a, a|}

and thus, after attaching the weights, also

{|a, {|a|}



MW,

NMW,

{|a, a|}

which is by 1.2. the same as Equation 5.1.

Fortunately, the ordering 

NMW

is monotonic and well-founded; this holds

by Theorem 2.1.1 and the following property:

Proposition 5.3.1. The ordering 

NMW

is a simpliﬁcation ordering.

Proof. Nested multisets with weights to be compared by 

NMW

are terms

built from the variadic constructor symbol {|.|}, the 2-ary sequence construc-

tor h., .i and a set C of constants. Furthermore a ﬁnite set W ⊂ IN is given.

Now consider the recursive path ordering with status >

RP OS

(see e.g.

[

Stein-

bach, 1990

]

), where {|.|} is assigned a multiset status and h., .i is assigned a

lexicographical left-to-right status. The precedence >

RP OS

on function sym-

bols uses the given well-founded ordering  on C; the set W is mapped

5.3 Orderings and Redundancy 167

isomorphically (say, by φ) to a set of new constants, and >

RP OS

is extended

order-isomorphically wrt. the ordering > on naturals. Finally, the construc-

tor symbols {|.|} and h., .i are given in >

RP OS

more weight than φ(max(W )).

This implies {|.|} >

RP OS

φ(w) for every multiset.

With this deﬁnition it can be veriﬁed by unfolding >

RP OS

according to

the cases of term structure, that 

NMW

satisﬁes >

RP OS

. In particular, the

condition that the constructor symbols {|.|} and h., .i is given in >

RP OS

weight than φ(max(W )) implies that we can obtain M

RP OS

in case

N is a true subset of M (because then M

RP OS

w holds, as is required by

RP OS

Thus, with >

RP OS

being a simpliﬁcation ordering (see

[

Steinbach,

1990

]

), 

NMW

is also.

5.3.2 Derivation Orderings

In order to be as general as possible we introduce the following notion:

Deﬁnition 5.3.2 (Derivation Ordering). A binary relation  on ground

derivations is called a derivation ordering iﬀ  is a well-founded and strict

ordering. Now let D be a derivation. A derivation ordering  is called mono-

tonic iﬀ D|

p,i,j

= G and G  F implies D  D[F ]

p,i,j

, where F is a deriva-

tion which agrees with G on top literal and derived literal.

Next we will design an appropriate derivation ordering for linearizing com-

pletion. For this let D be a derivation

D =(L

==⇒L

···L

==⇒L

n+1

and deﬁne the complexity of D, compl(D)as

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

),w

i,... ,hcompl(D

),w

i|} ,

where for a sequence D

···D

of derivations we deﬁne

compl(D

···D

[

i=1...m

compl(D

) .

Thus, compl(D) is a multiset whose elements are nested multisets with

weights over the set {0}. compl(D) contains structural information about

the derivation: it expresses the shape (when read as a tree) of the deriva-

tion encoded as multisets, and occurrences of input literals are mapped to

the dummy element 0 at the leaves. Furthermore, the weight of a used infer-

ence rule comes into the complexity measure as the weight of the multiset

corresponding to the rule application. For instance, the derivation D

in ex-

ample 5.2.1 has the complexity {|0, {||}

, {|0, {||}

|}.

We conjecture that even without the restriction to ﬁnite W a simpliﬁcation

ordering results. This proof, however, does not go through in that case.

168 5. Linearizing Completion

In order to compare two derivations D

and D

we attach the artiﬁcial

weight 0 to them and use the nested multiset ordering with weights. More

formally deﬁne



Lin

iﬀ hcompl(D

), 0i

NMW,⊥

hcompl(D

), 0i ,

where the base set X is {0} and its base ordering ⊥ is the empty order-

ing ∅ (this is trivially an ordering). Evidently, a derivation D is linear (cf.

Section 5.2) iﬀ its complexity compl(D) is of the form

{|0, {|0,... ,0|}

,... ,{|0,... ,0|}

|} ,

where the w

s are are the weights of the used inference rules. The ordering



Lin

is deﬁned in such a way that when weights are neglected smaller deriva-

tions are “more linear”. Even more, if D is linear and D 

Lin

then D

also linear (Lemma 5.5.1).

It holds:

Proposition 5.3.2. The relation 

Lin

is a monotonic derivation ordering.

5.3.3 Redundancy

Building on orderings we come to redundancy. In order to be as ﬂexible as

possibly the following deﬁnition is rather general and includes the notion of

redundancy presently used for the linearizing completion as a special case.

Deﬁnition 5.3.3 (-Redundancy). Let  be a derivation ordering, and

let I be an inference system. An inference rule P → C is called (-)redundant

in I for derivations (I need not necessarily contain P → C) iﬀ for every

inference system J with I⊆J and every ground derivation

D =(L

⇒

∗

(J∪{P →C})

)

which uses P → C there is also a ground derivation D

≺ D of the form

=(L

⇒

∗

(J\{P →C})

) .

The rule P → C is called (-)redundant in I for completion iﬀ (1) P → C is

not of the form ¬A → F, where A is an atom, and (2) P → C is -redundant

in I for derivations.

The short forms (-)c-redundant in I and (-)d-redundant in I used in

the sequel mean for completion and for derivations, respectively

An inference rule of the form ¬A → F is never -redundant due to (1).

The motivation for this comes from the use of such rules in the rˆole of input

literals during completion. It turns out that the deletion of a rule ¬A → F in

general does not provide a substitute for this purpose, even if the rule would

be redundant according to -redundancy for derivations.

5.3 Orderings and Redundancy 169

-redundancy for derivations means that any ground derivation in a pos-

sibly extended inference system J using the redundant inference rule can

be replaced by a smaller derivation wrt. , which uses at most the input

literals as given, and this derivation does not use the redundant rule. The

strict decreasing property is required since otherwise the redundancy of a rule

in a certain inference system would not carry over to the inference system

obtained as the limit of the completion process.

Notice that -redundancy for derivations quantiﬁes over derivations and

hence does not suggest a respective procedure for testing -redundancy. We

would thus like to have a more “local”, constructive way of characterizing

-redundancy for derivations. The following suﬃcient criterion achieves this

for the case of linearizing completion:

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.

The proof is by induction on the structure of a derivation, thereby making

use of the monotonicity property of 

Lin

in the induction step.

Informally, the condition hP \{|L|},wi

i means that the i-th

inference step either uses strictly fewer side literals (the set D

) than the side

literals P \{|L|} of an inference step carried out with P →

C, or else, the

side literals are the same, but an inference rule of less weight is used. This

check has to be done for every L ∈ P according to the potential applications

of the inference rule in a derivation.

Example 5.3.2. Consider the following ground inference system:

(1) A, B, C →

(2) A, B, C →

(3) E,C →

(4) C →

The rule (1) is 

Lin

-redundant for completion , because it is not of the form

¬A → F and it is redundant for derivations. Using Proposition 5.3.3 this is

checked as follows: for A as top literal consider the derivation A

==⇒

(1)

D.It

can be replaced by the derivation A

==⇒

(2)

=⇒

(3)

D; for the ﬁrst inference

step we have

170 5. Linearizing Completion

{|B, C|} =({|A, B, C|}\{|A|}) .

Hence the weights must be considered, which yields 3 < 4. Thus the ﬁrst

inference step satisﬁes the condition stated in the proposition. For the second

step we have {|C|}⊂{|B,C|}, hence the weights do not matter. The case for

B as top literal is similar, and for the top literal C rule (4) can be used.

Example 5.3.3. Consider the rule R =(x<x

→ x<z

)

which expresses a once unfolded transitivity rule Trans =(x<y,y<z→

x<z). We claim that R is 

Lin

-d-redundant in an inference system which

contains Trans. Using Proposition 5.3.3 this is checked as follows: for x<x

as top literal consider the derivation

x<x

========⇒

x<z

whose side literals are {|x

|}. It can be replaced by the derivation

x<x

===⇒

(Trans)

x<y

===⇒

(Trans)

x<z

Furthermore for the ﬁrst inference step it holds {|x

|}⊂{|x

and for the second step {|y

|}⊂{|x

|}. Similarly derivations

with top literals x

and y

exist. Weights are not needed for these

derivations.

The practical value of the stronger -redundancy for derivations alone is the

possibility to delete rules from an inference system I which are redundant for

derivations without losing completeness. In the search for derivations (and in

particular refutations) we will thus never have to consider rules of the form

¬A → F, provided they are redundant for derivations. Section 5.7.3 below

contains an example of a successful application of this idea.

The formal account is as follows:

Deﬁnition 5.3.4 (NonRed(I)). Let I be a possibly inﬁnite inference sys-

tem. Consider any possibly inﬁnite sequence

= I) ⊇I

⊇···⊇I

⊇···

of inference systems, where I

i+1

is obtained from I

(for i ≥ 0) by deletion

of an inference rule which is redundant in I

for derivations. Deﬁne the non-

redundant inference rules of this sequence as

NonRed(I)=

i≥0

That is, we stepwisely remove inference rules which are redundant for deriva-

tions. The limit NonRed(I) just consists of the rules which are persistent,

i.e. which are not deleted. Of course, NonRed(I) is not determined uniquely.

The next proposition justiﬁes this concept:

5.4 Transformation Systems 171

Proposition 5.3.4 (Completeness of NonRed(I)). For every ground de-

rivation D =(L

⇒

∗

) a ground derivation D

=(L

⇒

∗

NonRed (I)

) with D

 D exists.

Proof. It is clear from the deﬁnition of redundancy for derivations that

⇒

∗

for all i. Further, for some I

it must be the case that all infer-

ence rules I

⊆I

ground instances of which are used in D

= L

⇒

∗

are never deleted afterwards, i.e. I

⊆I

for all j ≥ i (*). Reason: otherwise

there would be an inﬁnite sequence (D

= D)  D

 ···  D

 ···

of derivations D

= L

⇒

∗

, which however, is impossible by well-

foundedness of the derivation ordering . Thus, from (*) it follows immedi-

ately that I

⊆ NonRed(I), and D

exist as claimed.

5.4 Transformation Systems

Transformation systems are the formal device for transformations of the in-

ference systems of the previous section. A transformation system transforms

an initial inference system in a fair way by application of certain transfor-

mation rules into a completed state. Completed inference systems in turn are

refutationally complete wrt. the desired restrictions (in our case “linearity”

and “unit-resulting”).

Deﬁnition 5.4.1 (Transformation system). A transformation rule with

premise P and conclusion C is an expression of the form

where P is a

multiset of inference rules and C is an inference rule. By applying a trans-

formation rule to a multiset of inference rules P

we mean the matching of P

to P

by some substitution µ. The result of such an application then is Cµ.

A transformation rule can be labeled as mandatory or optional.Atransfor-

mation system consists of a set of transformation rules and a well-founded

ordering  on derivations.

Let S be a transformation system. The relation I`

(deduction step)

on inference systems means that I

is obtained from I by either (1) adding the

result of an application of a transformation rule from S to variable disjoint

variants of rules in I, or else (2) by deleting a -c-redundant inference rule

from I. In case (1) the weight of the added inference rule can be chosen

arbitrarily. A S-deduction from an inference system I

is a sequence I

···`

···. Deductions may be of ﬁnite or inﬁnite length.

In this book we concentrate on the instance “linearizing completion”.

Therefore we deﬁne the transformation system Lin to consists of transfor-

mation rules given in Figure 5.7. The transformation rules Unit1, Unit2 and

Deduce are labeled as mandatory, and Contra is labeled as optional. As the

derivation ordering we use 

Lin

as deﬁned in Section 5.3.

172 5. Linearizing Completion

Unit1:

→ C ¬A

→ F

Cσ → F

If A

σ = A

σ by MGU σ.

Unit2:

,P → C ¬A

→ F

(P → C)σ

(

If (1) P 6= ∅, and

(2) A

σ = A

σ by MGU σ

Deduce:

→ C

)σ

(

If (1) P

6= ∅, and

(2) C

σ = L

σ by MGU σ

Contra (optional):

L, P → C

C,P → L

If C 6= F

For atoms A

, literals C, L, L

and literal multisets P ,P

and P

Figure 5.7. The transformation rules of the transformation system Lin.

5.4 Transformation Systems 173

Example 5.4.1. From the ground rules A → B and ¬A → F the rule ¬B → F

can be obtained by Unit1

. Consider the inference system I

(T ) of Exam-

ple 5.2.1 again. From B, D → F and ¬D → F we can obtain B → F by

Unit2. Unit1 and Unit2 share the same purpose: to eliminate in derivations

applications of literals from Punit(I) (these are initially needed, as stated

in Lemma 5.2.1). For instance, the set M

= {A, C} in Example 5.2.1 now

admits the I

(T ) ∪{B → F}-refutation

=(A=⇒

A→B

B=⇒

B→F

F) .

From the rules C → D and B, D → F in Example 5.2.1 the rule B, C → F

can be obtained by Deduce. Deduced rules are used to turn a refutation

stepwise into a “more linear” refutation. Again, using I

(T ) ∪{B, C → F}

the refutation D

from Example 5.2.1 of M

= {A, C} can be linearized with

the new rule. We have:

=(A=⇒

A→B

=⇒

B,C→F

F) .

If the new rule B, C → F is given the weight, say, 10, then the complexity of

is {|0, {||}

, {|0|}

|} and it can be veriﬁed that D



Lin

From the transitivity rule x<y,y<z→ x<zand a copy x

→ x

by Deduce with σ = {y ← x

,z ← z

} one obtains

x<x

→ x<z

From A, B → C by Contra ¬C, B →¬A can be obtained.

This Contra transformation rule is an optional rule and thus is not labeled as

mandatory. It is sometimes valuable in order to come to a ﬁnite system (see

Section 5.1.4 in the introduction for an example). However, the Contra rule

should be applied carefully since it increases the search space of the generated

inference systems; applying Contra exhaustively will produce every possible

contrapositive of a theory clause. This is clearly not intended. Surprisingly,

an application of the Contra rule may increase the deductive power of an in-

ference system: consider e.g. I = {A → B}. The only non-trivial I-derivation

is A=⇒B. However, when I is enriched with the contrapositive ¬B →¬A,

the derivation ¬B=⇒¬A also exists. However its application does not increase

the refutational power of inference systems.

We collect for later use the following lemma, which states that c-redundancy

persists along transformation steps:

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. If J is obtained by adding a new rule to I the lemma is trivial by

the property J⊇Iin the deﬁnition of c-redundancy (Def. 5.3.3). If J is

Weights are not considered in this example.