Baumgartner P. Theory Reasoning in Connection Calculi

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

174 5. Linearizing Completion

obtained from I by deletion of a redundant rule then well-founded induction

is used to eliminate every use of P → C and the deleted rule in derivations.

See the appendix for the full proof.

It should be remarked that the proof goes through even if d-redundancy

would be used instead of c-redundancy. This holds in other (but not all)

situations as well. But we do not need this here.

Note 5.4.1 (Soundness). We conclude this section with a note on soundness.

In order to achieve the soundness of the overall approach, one has ﬁrst to guar-

antee that all derivations obtainable from initial inference systems are sound.

This, however, is clear since they are nothing but Unit-Resulting refutations.

Secondly, one has to guarantee that derivations obtainable from transformed

inference systems are sound. The key to this result is the observation that

newly generated inference rules are just resolvents of present rules, and hence

are logical consequences of these.

5.4.1 Limit Inference Systems

The process of applying the transformation rules of a transformation system

may terminate or not. In order to treat both cases in a uniform way it is useful

to deﬁne the limit inference system I

∞

, which is ﬁnite if the transformation

system eventually does not produce new inference rules any more, and inﬁnite

otherwise.

Deﬁnition 5.4.2 (Limit,

[

Bachmair, 1991

]

). The limit of a deduction

`···`I

··· is deﬁned as

∞

[

j≥i

The elements of I

∞

are also called the persisting inference rules.

The limit I

∞

of a deduction is the set of inference rules generated eventually

and never deleted afterwards:

Lemma 5.4.2. Let I

` ... be a deduction and suppose (P → C) ∈

∞

. Then for some k, and for all i ≥ k: (P → C) ∈I

Proof. By contradiction. Assume P → C ∈I

∞

and suppose that for all k

an i ≥ k exists such that P → C/∈I

. Hence whenever P → C ∈I

then

P → C/∈

i≥k

.ThusP → C/∈

i≥k

and hence by deﬁnition of I

∞

P → C/∈I

∞

. This however contradicts the assumption of the lemma.

This result can be extended for derivations:

Proposition 5.4.1. Let I

` ... be a deduction and let D be a I

∞

derivation (resp. I

∞

derivation). Then for some k, D is also a I

-derivation

(resp. I

derivation).

5.4 Transformation Systems 175

Proof. Let {r

,... ,r

}⊆I

∞

be the (ﬁnite) inference system used in the

given derivation. For every r

(j =1...n) by Lemma 5.4.2 it holds that for

some k

, all i ≥ k

: r

∈I

. Now take k = max({k

,... ,k

}) and observe

that {r

,... ,r

}⊆I

The next lemma extends Lemma 5.4.1 to the limit I

∞

, i.e. c-redundant in-

ference rules remain redundant in the limit:

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

∞

Also the Punit-literals persist:

Lemma 5.4.4. Let I

` ··· be a deduction. If A ∈ Punit(I

)

then

also A ∈ Punit(I

∞

)

Proof. A is a ground instance of some atom A

, where ¬A

→ F ∈I

.By

deﬁnition of -c-redundancy, a rule ¬A → F ∈I

is never -c-redundant

and thus is never deleted. Hence ¬A → F ∈I

for every i ≥ k.Thus

(¬A → F) ∈

i≥k

⊆

[

k≥0

i≥k

= I

∞

By this the claim follows.

Lemma 5.4.3 and Lemma 5.4.4 imply the following central property:

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.

5.4.2 Fairness and Completion

Deductions must be fair, which roughly means that no application of a

mandatory transformation rule is deferred inﬁnitely long. Fairness is impor-

tant since it entails that “enough” inference rules to obtain normal derivations

are generated. Our deﬁnition of fairness is an adaption of standard deﬁnitions

in the term-rewriting literature (see e.g.

[

Bachmair, 1991

]

176 5. Linearizing Completion

Deﬁnition 5.4.3 (Fairness). Let S be a transformation system with deriva-

tion ordering .AnS-deduction I

`···`I

··· is called fair iﬀ

whenever I

∞

∪{P → C} for some application of a mandatory trans-

formation rule from S, then for some k, P → C ∈I

up to renaming, or

P → C is -c-redundant in I

Fairness states that it is suﬃcient either to generate an inference rule or

to prove it c-redundant from persisting inference rules only. This notion of

fairness enables the use of a “delete as many inference rules as possible”

strategy in implementations, since a rule once shown to be c-redundant is

redundant in all subsequent stages (Lemma 5.4.3) and thus need not persist.

The next central concept is that of a completed inference system, which

means that only c-redundant new inference rules can be generated. Com-

pletion is a useful concept since it allows us to characterize refutationally

complete inference systems, which is a semantic concept, in a more syntacti-

cal way

Deﬁnition 5.4.4 (Completed Inference System). Let S be a transfor-

mation system with derivation ordering . An inference system I is com-

pleted (wrt. S) iﬀ whenever I`

I∪{P → C} by application of a mandatory

transformation rule from S then P → C ∈Iup to renaming or P → C is

-c-redundant in I.

Fairness, deductions and completion relate as follows:

Theorem 5.4.1. Let S be a transformation system and I

be an inference

system. The limit I

∞

of a fair S-deduction I

` ··· is completed wrt.

Proof. By contradiction. Suppose I

∞

is not completed. Then, for some appli-

cation of a mandatory transformation rule from L we have I

∞

∪{P →

C} such that P → C/∈I

∞

and P → C is not -c-redundant in I

∞

(*).

However, by fairness, for some k, P → C ∈I

or P → C is c-redundant in

. This suggests the following case analysis:

Case 1: Suppose P → C ∈I

.IfP → C is not deleted afterwards, i.e. for

all i ≥ k, P → C ∈I

, then P → C ∈

i≥k

and thus also P → C ∈I

∞

Contradiction to (*).

Otherwise, if P → C is deleted in some I

, P → C must have been -c-

redundant in I

j−1

. But then by Lemma 5.4.3 P → C is -c-redundant in

∞

. Contradiction to (*).

Case 2: If P → C is -c-redundant in I

then by Lemma 5.4.3, P → C is

-c-redundant in I

∞

. Contradiction to (*).

Note that the term “complete” has two distinct technical meanings here, and

the refutational completeness of a completed system depends additionally on

how the inference rules are used (unit-resulting linear hyper resolution, in this

case), and what deduction rules are used to complete the system.

5.5 Complexity-Reducing Transformation Systems 177

5.5 Complexity-Reducing Transformation Systems

Up to now we have seen that the inference systems generated along a deduc-

tion never increase the complexity of a once obtained derivation. However,

in order to obtain completeness wrt. normal-form derivations (linear deriva-

tions) more is required: the transformation system has to eventually gener-

ate inference rules that will strictly decrease the complexity of a non-normal

derivation.

Deﬁnition 5.5.1 (Normal Derivations, Order-Normalizing System).

A set N of ground derivations is called normal iﬀ N is downward closed wrt.

a given derivation ordering , i.e. if D ∈N and D

 D for some ground

derivation D

then D

∈N. In the sequel N always denotes a set of normal

derivations.

Now let I be an inference system and let S be a transformation system

with derivation ordering . Then S is called order-normalizing wrt. N iﬀ

whenever there is a ground derivation D =(L ⇒

∗

) such that D/∈N

then there is a derivation D

=(L ⇒

∗

)

) with D

≺ D, where I

= I

or I`

by one single application of some mandatory transformation rule.

The normal derivations are the ones to be achieved by the completion process.

In the case of linearizing completion we thus target the set LinG of all linear

ground derivations.

From downward closure we can always conclude that if ground deriva-

tion D is normal and D

 D then also D

is normal. This is important

because if D

replaces a normal derivation D according to the deﬁnition of

-c-redundancy (Def. 5.3.3), then also D

will be normal.

For the case of linearizing completion it is therefore important to have:

Lemma 5.5.1. The set LinG of all linear ground derivations is normal wrt.

the derivation ordering 

Lin

. That is, if ground derivation D is linear and

D 

Lin

then D

is also linear.

Proof. Suppose, to the contrary, there is a linear ground derivation D and

a ground derivation D

such that D 

Lin

but D

is not linear. Hence

compl(D

) is of the form (weights omitted)

compl(D

)={|0,c

,...|}, where c

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

whereas

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

Suppose compl(D) contains n multisets as indicated. Let c be a maximal of

those. Clearly, by property of nested multiset ordering it holds c



NMW

Next let c

be obtained from compl(D

) by replacing c

by n + 1 occurrences

of c. It follows compl(D

) 

NMW

. On the other hand also c



NMW

compl(D). Thus, together compl(D

) 

NMW

compl(D), which is a contra-

diction to the assumption D 

Lin

(i.e. compl(D) 

NMW

compl(D

)).

178 5. Linearizing Completion

An order-normalizing transformation system enables the generation of a new

inference rule (if not present already) that allows a decrease in complexity of

a given non-normal ground derivation. Note that not necessarily D

∈N in

Deﬁnition 5.5.1. Such a property is not required, because the derivation order-

ing  is well-founded. So we will eventually end up with a normal derivation

∈N for any given derivation D (see Proposition 5.5.2 below).

As an example for an order-normalizing transformation system take “lin-

earizing completion”, which is order-normalizing wrt. linear ground deriva-

tions:

Proposition 5.5.1. The transformation system Lin is order-normalizing

wrt. LinG.

In essence, the proof uses the facts that the Deduce transformation rule is la-

beled as mandatory and furthermore works towards strictly decreasing deriva-

tions wrt. the well-founded ordering 

Lin

Returning to the general level, we ﬁnd that a completed inference system

in conjunction with order-normalizing transformation systems yields normal

derivations:

Proposition 5.5.2. Let S be an order-normalizing transformation system

wrt. N and let I be a completed inference system wrt. S with derivation

ordering . Whenever there a ground derivation D =(L ⇒

∗

) exists

then a ground derivation D

=(L ⇒

∗

) with D

∈N and D

 D also

exists.

Proof. By well-founded induction on the derivation ordering : either D ∈N

and we are done by taking D

= D, or else by deﬁnition of order-normalizing

transformation systems there is a derivation D

=(L ⇒

∗

)

) with

≺ D, where I

= I or I`

by application of some mandatory trans-

formation rule. If I

= I we can immediately apply the induction hypothesis

to D

to obtain the desired derivation D

. Otherwise, I

= I∪{P → C}.

Since I is completed either (a) a variant of P → C is contained in I,or(b)

P → C is -c-redundant in I. In case (a) we can replace in D

every use of

P → C by its variant from I and obtain a I-derivation alone (to which the

induction hypothesis can be applied). Now for case (b): either P → C is not

used and thus D

is a I-derivation alone (to which the induction hypothesis

can be applied), or else, by deﬁnition of c-redundancy (Def. 5.3.3) there is a

-derivation D

000

≺ D

of the same kind as D

. By applying the induction

hypothesis to D

000

this concluding case is done.

Chaining ground completeness (Lemma 5.2.1), the completion property

of limits (Theorem 5.4.1) with Proposition 5.5.2 we can obtain normal refu-

tations of M ∪ Punit(I), where M is some T -unsatisﬁable literal set. Thus, a

refutation might still use unit inference rules being turned via Punit(I)into

input literals. However, every use of a literal from Punit(I) represents a com-

putation among the inference rules and should be avoided. In order to admit

5.5 Complexity-Reducing Transformation Systems 179

normal refutations with input literals M alone, we will compile the literals

Punit(I) into the inference system. The situation is much like normalizing

above, but now “normal” means “free of usages of elements of Punit(I)”.

In order to obtain termination when eliminating these cases we require the

respective mandatory transformation rules to work strictly decreasing wrt.

. This is captured in the next deﬁnition.

Deﬁnition 5.5.2 (Punit-Normalizing Transformation System).

The multiset of used input literals of a derivation D is deﬁned as

Used(D)={|L | L is the top literal of D|

, where p ∈ P (D)|} .

The function used is extended homomorphically to sequences and multisets

of derivations as expected.

Let S be a transformation system with derivation ordering  and let N

be a set of normal derivations. Then S is called Punit-normalizing wrt. N

iﬀ whenever there is a non-trivial ground derivation

D =(L ⇒

∗

,M∪Punit (I

)

with D ∈N such that Used (D) ∩ Punit(I

) 6= ∅ then there is a derivation

=(K ⇒

∗

)

,M∪Punit ((I

)

with D

≺ D where K ∈ M ∪ Punit((I

)

) ∪{L} and I

= I or I`

application of some mandatory transformation rule.

“Punit-normalization” means that whenever an inference rule ¬A → F is

used as an input literal A then a strictly smaller derivation exists. That

derivation, however, need not start with the same top literal L, but may as

well start with a top literal from M ∪ Punit((I

)

). Note that according to

this deﬁnition it suﬃces for a Punit-normalizing transformation system to

work on normal-form derivations only.

Fortunately it holds:

Proposition 5.5.3. The transformation system Lin is Punit-normalizing

wrt. LinG.

This is essentially due to the transformation rules Unit1 and Unit2.

Example 5.5.1. Consider the inference system I

(T ) in Example 5.2.1 again.

It holds Used(D

)={A, C}. Since I

(T ) includes a rule ¬D → F,wehave

= M

∪ Punit(I

(T )) = {A, C, D} ,

and we can ﬁnd a I

(T )-derivation

=(A=⇒

A→B

=⇒

B,D→F

180 5. Linearizing Completion

from M

. It holds that

Used(D

) ∩ Punit(I

(T )) = {A, D}∩{D}6= ∅ .

By the previous proposition we should be able to ﬁnd a smaller derivation wrt.



Lin

after application of some mandatory inference rule from Lin. Indeed, the

Unit2 rule applied to B, D → F and ¬D → F, gives the new rule B → F and

allows for a smaller derivation. This derivation is just D

in Example 5.4.1.

Completed inference systems in conjunction with Punit-normalizing trans-

formation systems yield derivations that are free of applications of inference

rules ¬A → F as input literals A. This result is similar to Proposition 5.5.2

for order-normal derivations:

Proposition 5.5.4. Let S be a Punit-normalizing transformation system

wrt. N , and let I be a completed inference system wrt. S. Whenever there

is a ground derivation D =(L ⇒

∗

,M∪Punit (I

)

) with D ∈N then there

is also a ground derivation D

=(K ⇒

∗

) with D

 D, D

∈N and

some K ∈ M ∪{L}.

Since we are interested in both properties — Punit-normalization and order-

normalization — we deﬁne:

Deﬁnition 5.5.3 (Normalizing Transformation System). A transforma-

tion system S is called normalizing wrt. N iﬀ S is both order-normalizing

wrt. N and Punit-normalizing wrt. N .

Combining Propositions 5.5.1 and 5.5.3 we then obtain:

Theorem 5.5.1. The Transformation system Lin is normalizing wrt. the set

LinG of linear ground derivations.

5.6 Completeness

The goal of this section is to assemble the material of the previous sections

into several completeness results. A soundness result for linearizing comple-

tion shall not be formally established. Soundness can easily be shown by

observing that all derivations and deductions can be simulated by resolution.

Hence, if a refutation of a T -satisﬁable set M would exist, it could also be

found by resolution, which is impossible by soundness of resolution.

We ﬁrst establish a general ground completeness result which does not

refer to a special derivation ordering. This result will then be instantiated

for the case of linearizing completion, and it will be shown that linearizing

completion yields suitable background reasoners for the intended application

within both total and partial theory reasoning.

5.6 Completeness 181

5.6.1 Ground Completeness

In purely equational logic and Knuth-Bendix completion, Birkhoﬀ’s theorem

links model theory and proof theory: two ground terms are equal in an equa-

tional theory T — i.e. a set of equations — iﬀ they can be made identical by

replacement operations using the equations from T . Since we deal with more

general theories we proved in Section 5.2 a corresponding result (ground com-

pleteness, Lemma 5.2.1). In order to apply it we ﬁnd it helpful to introduce

the following notion:

Deﬁnition 5.6.1 (Relative Completeness). Inference system I is called

relatively complete wrt. an inference system J iﬀ whenever L ⇒

∗

,M∪Punit (J

)

then also L ⇒

∗

,M∪Punit (I

)

Now we can turn towards completeness. Notice that quite often we will use

an inference system NonRed(I) and not just I. That is, during “refutation

time” there is no need to keep inference rules of the form ¬A → F which are

redundant for derivations.

We start with a general result:

Theorem 5.6.1 (General Ground Completeness Theorem). Let T be

a theory and let S be a normalizing transformation system wrt. some set N

of normal derivations. Suppose an inference system I is completed wrt. S,

and also suppose that I is relatively complete wrt. I

(T ). Then for every T -

unsatisﬁable ground literal set M there is a NonRed(I)

-refutation D ∈N

of M with some top literal from M .

Proof. It holds that M is T -unsatisﬁable iﬀ M

∪T

is unsatisﬁable for some

ﬁnite subsets M

⊆ M and T

⊆T

(apply Proposition 2.5.1.3, equivalence

(a)-(e), and the Skolem, Herbrand, L¨owenheim Theorem, Theorem 2.4.3). By

ground completeness, Lemma 5.2.1, then

L ⇒

∗

),M

∪Punit (I

))

F ,

for some L ∈ M

∪ Punit(I

)). With I

) ⊆I

(T )

and M

⊆ M it

follows

L ⇒

∗

(T )

,M∪Punit (I

(T )

)

F .

Since I is given as relatively complete wrt. I

(T ) we ﬁnd by deﬁnition

L ⇒

∗

,M∪Punit (I

)

F .

With S being given as normalizing wrt. N we can ﬁrst ﬁnd (by Proposi-

tion 5.5.2) an order-normal refutation

(L ⇒

∗

,M∪Punit (I

)

F) ∈N ,

and then we can ﬁnd (by Proposition 5.5.4) a Punit-normal refutation

182 5. Linearizing Completion

(K ⇒

∗

F) ∈N ,

for some K ∈ M. Finally apply Proposition 5.3.4.

This theorem requires the existence of a completed and relatively complete

inference system wrt. I

(T ). Such a system can be obtained in a constructive

way as the limit of a fair deduction:

Theorem 5.6.2. The limit I

∞

of an S-deduction I

(T ) `

... is

relatively complete wrt. I

(T ), where T is a theory.

Proof. Use Lemma 5.4.5, setting there I

= I

(T ) and k =0.

Thus we can instantiate the general ground completeness theorem:

Corollary 5.6.1. (to Theorem 5.6.1) Let T , S and N as in Theorem 5.6.1,

and let I

∞

be the limit of a fair S-deduction I

(T ) `

.... Then for

every T -unsatisﬁable ground literal set M there is a NonRed(I

∞

)

-refutation

D ∈N of M with some top literal from M.

Proof. By Theorem 5.6.2 I

∞

is relatively complete wrt. I

(T ), and by The-

orem 5.4.1 I

∞

is completed wrt. S. Hence the corollary follows from the

theorem.

Next we are going to instantiate this corollary towards “linearizing com-

pletion”. Before we do so, observe that the corollary (as well as the theorem)

states completeness for some top literal chosen from the input literal set. How-

ever, as motivated in the discussion following Deﬁnition 4.5.6 (page 125), the

intended application of completed inference systems as background reasoners

within theory reasoning calculi demands that we insist on a completeness

result with respect to every literal as top literal. This “independence of the

goal” property corresponds to e.g. linear resolution for Horn theories where

it suﬃces to start derivations with a negative clause. In practice, this means

that the top literal need not be guessed in a don’t-know nondeterministic

way, but can be chosen a priori.

Fortunately, the transformation system Lin is powerful enough to generate

inference rules that allow rearrangement of a given linear derivation such that

any literal used inside a derivation can be switched to the top position. This

is expressed in the following lemma:

Lemma 5.6.1 (Top Literal Lemma). Let I be a completed inference sys-

tem wrt. the transformation system Lin. Suppose there is a linear ground

derivation D =(L

⇒

∗

) with L

∈ M.LetT ∈ M such that

T ∈ Used(D). Then there is a linear ground derivation D

=(T ⇒

∗

Example 5.6.1. The inference system I

in Example 4.5.3 is completed wrt.

Lin. Let D be the refutation stated there (the current notation is a bit dif-

ferent, but that does not matter). Since c<d∈ Used (D) a refutation with

top literal c<dexists, which is as follows:

5.6 Completeness 183

c<d

d<e

=⇒ c<e

e<a

=⇒ c<a

a<b

=⇒ c<b

b<c

=⇒ c<c=⇒ F .

Note that the top literal lemma is not formulated within the general unin-

stantiated completion theory, since in general it may be not useful to demand

the completeness for arbitrary chosen top literals for arbitrary transformation

systems.

Now with the top literal lemma we can obtain the desired completeness

result for linearizing completion.

Theorem 5.6.3 (Ground Completeness of Linearizing Completion).

Let I be an inference system completed wrt. the transformation system Lin.

Let T be a theory and suppose I is relatively complete wrt. I

(T ). Then for

every minimal T -unsatisﬁable ground literal set M and every literal L ∈ M

there is a linear refutation

L ⇒

∗

NonRed (I)

F .

Note that a relatively complete inference system as assumed in the theorem

can be obtained by application of Theorem 5.6.2.

Proof. By the general ground completeness theorem (Theorem 5.6.1) there

is a linear I

-refutation D

∈ LinG of M. Since M is given as minimal T -

unsatisﬁable, the intended top literal L must be used at least once in the

refutation, because otherwise the refutation of M \{L} implies by soundness

a contradiction to the minimality assumption about M. Next apply the top

literal lemma (Lemma 5.6.1) to D

and obtain a linear refutation D

with top

literal L. Finally, from Proposition 5.3.4 we learn that a refutation D ≺

Lin

using NonRed(I) exists. Further, by Lemma 5.5.1 we know that D is thus a

linear refutation as desired.

5.6.2 The Link to Theory Model Elimination

Now the link between linearizing completion and its intended application

within PTME-I and PRTME-I is made:

Corollary 5.6.2 (Ground Complete Background Reasoners).

Let T and I as in Theorem 5.6.3. Then NonRed(I)

−

is ground complete wrt.

T (Def. 4.5.6), where NonRed(I)

−

is obtained from NonRed(I) by removing

the weight from each inference rule.

Further, if T is a deﬁnite theory, then the inference system obtained from

NonRed(I)

−

by deleting all inference rules which are not contra-deﬁnite is

still ground complete for negative top literals (cf. Def. 4.5.6 again).

Proof. For the ﬁrst part, let M be a minimal ground T -complementary literal

set and let T ∈ M . We have to show that a background refutation as deﬁned

in Def. 4.5.6 exists.

By Theorem 5.6.3 there is a ground, linear NonRed(I)-refutation