Baumgartner P. Theory Reasoning in Connection Calculi

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

154 5. Linearizing Completion

1. x<y, y<x → x<z

2. ¬x<z, y<x →¬x<y

3. x<y, ¬x<z →¬y<x .

However, there are cases where not all contrapositives are needed. For ex-

ample, one of contrapositive 2 or 3 can safely be deleted without aﬀect-

ing completeness. Such restrictions are expressible in our more ﬁne-grained

framework, while they are not in traditional unit-resulting resolution frame-

work. This motivated us not to use the traditional formalism but to deﬁne a

new one.

Hyper Resolution. Hyper resolution

[

Robinson, 1965a

]

is a complete calcu-

lus for Horn clause logic. It implements a bottom-up evaluation by starting

from the given positive unit clauses and deriving new unit clauses in a unit-

resulting way. In our terminology, only the “natural” contrapositives, such as

1, in the last example are needed for this. However, hyper resolution alone

does not suggest any completion procedure and yields inherently non-linear

refutations. But hyper resolution refutations will serve as a starting point for

the completeness proof of linearizing completion.

Binary Resolution. As mentioned above, the Unit1 and Unit2 rules are in-

stances of unit resolution. Similarly, the Deduce rule works much like the

traditional binary resolution inference rule (see e.g.

[

Chang and Lee, 1973

]

In fact, short of implicit factoring due to set notation, it is merely a suggestive

notation for it which seems appropriate for the purposes here. So the ques-

tion might come up where linearizing completion is diﬀerent from ordinary

resolution.

First, ordinary resolution does not have a restriction to certain contra-

positives, as just explained.

Second, every refutation in the linearizing completion paradigm can be

simulated stepwise by an ordinary resolution refutation in the following way,

but the other direction does not hold. Let T

be the Horn clause theory

subject to linearizing completion, M be a T

-unsatisﬁable literal set, and

∈ M be the desired top literal of the refutation.

Then a refutation in the linearizing completion framework can be written

as a resolution refutation

, T

,... ,T

,... ,G

, F ,

where (1) the T

’s are obtained from the T

i−1

’s by application of binary res-

olution, corresponding to the transformation rules of linearizing completion,

and (2) the G

’s are obtained from the G

j−1

’s and literals from M by unit-

resulting resolution, using a nucleus clause from T

. These unit-resulting steps

could be simulated by sequences of ordinary resolution steps, of course.

It is apparent that this refutation is a highly structured one; evidently not

every ordinary resolution refutation is structured in that way. Thus, stepwise

simulation in the other direction does not hold.

5.1 Introduction 155

Third, linearizing completion uses powerful redundancy criteria which are

usually not applied in ordinary resolution.

Fourth (connected with three), linearizing completion functions as a com-

piler, which allows for careful analysis of the input clause set independent of

the proof task to be given later. This means that T

can be computed once

and for all. This is not done to that extent in ordinary resolution.

Linked Inference Principle. The linked inference principle

[

Wos et al., 1984;

Veroﬀ and Wos, 1992

]

,orlinked resolution, is related to linearizing comple-

tion. According to

[

Kunen, 1991

]

, linked resolution is a general technique for

doing several binary resolution steps at once, keeping the ﬁnal clause, and

discarding the intermediate clauses. This technique diminishes the number

of clauses stored in the database. The most unlimited version of linked reso-

lution is trivially complete, but is also not feasible to implement because of

the large number of sequences of binary resolutions which must be examined

at each stage of the deduction.

[

Kunen, 1991

]

a rather general completeness result was obtained. In this

setup, linking clauses are written as φ k ψ where φ and ψ are disjunctions of

literals. Semantically, k stands for “or”. Thus, by k a clause is devided in two

parts. In pure linking clauses ψ = 2 (the empty clause), and in pure standard

clauses φ = 2. The following inference rules are needed:

1. linking (ground case): from center clause α

∨ ...∨ α

k ψ and n pure

standard clauses

∨ ψ

(i =1,... ,n) derive 2 k ψ ∨ ψ

∨ ...∨ ψ

. This

rule lifts as usual to the ﬁrst order case by taking new variants.

2. left resolution: “standard” resolution among linking clauses using com-

plementary literals both to the left of k.

3. left factoring: “standard” factoring, analogously to 2.

4. right resolution: “standard” resolution among linking clauses using com-

plementary literals both to the right of k.

5. right factoring: “standard” factoring, analogously to 4.

A refutation is found if 2 k 2 is derived. As a pruning technique, tautologies

can be deleted except “right tautologies” which contain A and ¬A on the

right of k (for some literal A).

The question arises whether linked resolution can simulate linearizing

completion, or vice versa. In order to make linked resolution simulate lineariz-

ing completion for given Horn theory T one can write every clause C ∈T as

C k 2. For instance, the theory S and literals set M

= {A, C} from above

become

= {¬A ∨ B k 2, ¬C ∨ D k 2, ¬B ∨¬D k 2}

Now, application of the transformation rules of linearizing completion can

be simulated by linked resolution in such a way that for every new derived

inference rule there is an equivalent clause derivable by linked resolution:

the Unit1, Unit2 and Deduce are nothing but standard resolution inferences,

156 5. Linearizing Completion

and hence can be simulated by left resolution. The Contra transformation rule

only reorders an inference rule, but as a clause it remains the same. The same

holds when applying transformation steps to the inference rules A, ¬A → F

from I

(T ).

For instance, the new inference rule C, B → F would be obtained as the

clause ¬C ∨¬B k 2 by left resolution of ¬C ∨ D k 2 and ¬B ∨¬D k 2.

Now let a T -unsatisﬁable literal set L as given. It seems natural to write

every literal L ∈Las 2 k L (writing it as L k 2 would reduce linked

resolution to ordinary binary resolution).

Now, the linear and unit-resulting refutation of L and the completed

theory (cf. Def 4.5.6) would not be exactly simulated by linked resolution

because only one link inference is necessary to obtain the empty clause 2 k 2.

The price to be paid for this is a possible much larger completed theory (e.g.

a transitivity clause ¬(X<Y) ∨¬(Y<Z) ∨ (X<Z) k 2 would lead to

nontermination). Thus, in this setting linked resolution is much like Murray

and Rosenthal’s method

[

Murray and Rosenthal, 1987

]

, which was discussed

above.

On the other side, since linked resolution is not restricted to Horn theories,

linked resolution could possibly be used as a generalisation of linearizing

completion towards the non-Horn case (this is future work).

An alternative approach: linked resolution has hyper resolution as an

instance. To obtain this, clauses are divided such that the negative literals

come the left of k and positive literals come to the right of k. Writing a

theory T in this way has a similar eﬀect as using the initial inference system

(T ). It was argued above that I

T does not suﬃce for the purpose of

theory reasoning. Application of the transformation rules can in general not

be simulated by linked resolution. For instance, from A → B and B → C one

can Deduce A → C, but there is no inference possible beween ¬A k B and

¬B k C. This is not intended to argue that one approach is better than the

other. Instead it shows us that the calculi are diﬀerent.

In sum, although linked resolution and linearising completion have similar

motivation and inference rules, there seems to be no perfect simulation of one

approach using the other.

The rest of this chapter is organized as follows: after recalling some pre-

liminaries in Section 5.1.6, we extend in Section 5.2 the deﬁnition of inference

systems (Def. 4.5.1) towards non-linear derivations; it also contains the com-

pleteness of initial inference systems for non-linear refutations. As mentioned,

deletion of redundant inference rules is tightly coupled with associated or-

derings of derivations. Section 5.3 describes orderings and redundancy. Then

we are prepared for the transformation systems of Section 5.4. This section

introduces the related important notions of limit and fairness of a deduction,

and also that of a completed inference system. There it will be shown that the

deﬁned transformation rules and redundancy criterion preserve refutational

completeness. In Section 5.5 we build on Section 5.4 and show that the trans-

5.2 Inference Systems 157

formation systems have the complexity-reducing property, which means that

eventually a normal-form refutation will be reached. In Section 5.7 we will ap-

ply the material developed so far to two non-trivial examples (one is equality

extended by strict orderings, and the other is concerned with modal logic).

Then, in Section 5.6 the material developed so far will be assembled into

various completeness results; notably, ﬁrst-order results are also contained.

5.1.6 Preliminaries

Concerning multisets we refer to Section 2.1. If a set is used below where a

multiset is required, then the type conversion is done in the obvious way.

Furthermore we make heavy use of the data structure ‘sequence’. If in

the computations below a sequence appears where a multiset is required, the

transformation from sequences to multisets is done in the obvious way.

We are dealing with clause logic and Herbrand interpretations. See Sec-

tion 2.4 for the deﬁnition of clause logic; concerning the semantics of clause

logic we recall Lemma 2.4.1. In particular, Lemma 2.4.1.4 justiﬁes the interest

in Herbrand-interpretations.

A Horn theory T is a satisﬁable set of Horn clauses

. For the model-

theoretic notions (satisﬁability etc.) see Deﬁnition 2.5.6.

5.2 Inference Systems

Inference systems play the same role as sets of rewrite rules in Knuth-Bendix

completion: they are used for inferences on the object-level. Inference systems

are the objects of computation by transformation systems which are intro-

duced in the next section.

We will slightly generalize the previous deﬁnition of inference rules

(Def. 4.5.1) in that inference rules may be labeled by weights. Further, the

notion of a background refutation (Def. 4.5.5) will be generalized towards

non-linear refutations.

Deﬁnition 5.2.1 (Theory Inference System). A theory inference rule

with weight over a given signature Σ

(Σ

is deﬁned in Section 4.5.1) is

a triple P →

C, where P is a nonempty multiset of Σ-literals, w is a non-

negative integer (called weight) and C is either a nonempty set of Σ-literals

or the singleton {|F|}. Quite often, we will drop the weight index if not relevant

in the context. The short forms inference rule or simply rule will be used as

well.

The notions premise, conclusion, (ground) instance, (theory) inference

system, as well as the notational conventions are adapted from Def. 4.5.1

To be precise, we would have to speak of “theories which are axiomatized by

a ﬁnite set of Horn clauses”; however, for simplicity we will prefer the shorter

expression. See also Section 2.5.

158 5. Linearizing Completion

accordingly. Unless otherwise noted, in this chapter always theory inference

rules with weight are considered.

Obviously, an inference rule in the old sense is obtained by forgetting about

the weight. Weights are motivated by extended redundancy checks (cf. Ex-

ample 5.3.2 below).

Deﬁnition 5.2.2 (Matching Theory Inference Step). We say that a lit-

eral C

is inferred from a literal multiset P

by means of a matching theory

inference step with inference rule P →

C and substitution δ, written as

⇒

P →

C, δ

iﬀ P

= Pδ and C

= Cδ.

The notions of premise, conclusion, ground inference, used inference rule,

as well as the abbreviated notation are taken from Deﬁnition 4.5.2.

Unless otherwise noted, in this chapter the term “inference step” always

refers to matching theory inference steps, but not to the minimal ﬁrst-order

theory inferences of Deﬁnition 4.5.2.

This deﬁnition diﬀers from the minimal ﬁrst-order theory inferences of Def-

inition 4.5.2 in two respects: ﬁrstly, instead of a uniﬁer now matching sub-

stitution is used. Matching based inferences will be used for the major part

of this chapter. Secondly, the premise minimality and the attached notion

of ampliﬁcation is dropped. This makes the proof in this chapter technically

simpler. The lifting to the ﬁrst-order level, as well as the premise minimality

will be recovered below in Section 5.6.

Next we are going to inductively deﬁne I-derivations based on this notion

of inference:

Deﬁnition 5.2.3 (I-derivation). Let M be a ﬁnite set of literals, also

cal led input literals and I be a not necessarily ﬁnite inference system.

1. The literal L

(not necessarily from M )isanI-derivation of L

from M

with top literal L

and length 1. Such a derivation is also called trivial.

2. If

a) D

is an I-derivation of L

from input literals M with top literal L

and length n, and

b) D

,... ,D

≥ 0)areI-derivations (called side derivations in

this context) of side literals L

,... ,L

, respectively, from M,all

respective top literals are contained in M, and

c) P

→

is an inference rule from I, and

d) δ

is a substitution, such that

,... ,L

⇒

→

,δ

n+1

5.2 Inference Systems 159

then

n+1

=(D

···D

======⇒

→

,δ

n+1

)

is an I-derivation of L

n+1

from input literals M with top literal L

and

length n +1.

If context allows, the involved inference rule and/or the substitution δ

shall be omitted.

The symbol ε denotes the empty sequence of I-derivations. Often we use the

term derivation instead of I-derivation.

Note that derivations are nothing but syntactically sugared terms over a

respective signature, and thus can be subject to structural induction. In non-

trivial derivations the principal (4-ary) construct symbol is “⇒”, which takes

as arguments the derivation D

derived so far, the sequence D

···D

side derivations, the inference rule and the substitution involved. We will

often omit parenthesis and write derivations like

n+1

=(L

···D

======⇒

→

,δ

···L

···D

======⇒

→

,δ

n+1

)

Some more terminology is convenient: if D is a derivation of L we also

say that L is the derived literal of D; the derivation D is called ground iﬀ

every of its inferences is ground; D is called a refutation iﬀ D is a derivation

of F. An inference rule is said to be used in D iﬀ (some instance of) it is used

in some inference in D. D is called linear iﬀ every side derivation occurring

in it is a trivial derivation. Otherwise D is called non-linear. We will write

⇒

∗

I,M

to denote the fact that a I-derivation of L

from M with top literal L

exists;

similarly the notation

D =(L

⇒

∗

I,M

)

means that D is such a derivation.

Note that a derivation does not instantiate the input literals. This is the

same as in a “rewriting” proof in the term rewriting paradigm. Carrying on

this analogy, a derivation relates to a ﬁrst-order derivation (to be deﬁned in

Section 5.6) much like “rewriting” relates to “narrowing”

[

Hullot, 1980

]

The top literal plays the rˆole of a goal to be proved. We are interested in

arbitrary goal literals, not just negative literals as usually deﬁned for SLD-

resolution. Positive goal literals arise naturally: think e.g. of an inference

system for strict orderings, containing a rule X<X→ F for irreﬂexivity. A

provable query is then for example (in Prolog notation) ?−¬(a<a).

160 5. Linearizing Completion

5.2.1 Initial Inference Systems

As the ﬁrst step of linearizing completion a given Horn theory T is re-written

in a straightforward way as a set of inference rules:

Deﬁnition 5.2.4 (Initial Inference Systems). Let T be Horn theory and

let W ⊂ IN be a ﬁnite set of weights. The initial inference system of T , I

(T ),

is the inference system consisting of the rules

1. ¬A → F for every positive unit clause A ∈T, and

2. A

,... ,A

→ F for every purely negative Horn clause ¬A

∨ ...∨¬A

∈

T (k ≥ 1), and

3. A

,... ,A

→ B for every deﬁnite clause ¬A

∨ ... ∨¬A

∨ B ∈T

(k ≥ 1), and

4. Q(x

,... ,x

), ¬Q(x

,... ,x

) → F for every n-ary predicate symbol Q

in T .

Furthermore, some arbitrary chosen weight w ∈ W is attached to every rule

in I

(T ). Note that with the theory being satisﬁable, the empty clause is not

contained in T . Thus for every clause in T exactly one case applies.

Example 5.2.1. Let T = {¬A ∨ B, ¬C ∨ D, ¬B ∨¬D, D} be a ground Horn

theory (it was also given as S

in the introduction). Then an initial inference

(T ) system is

(T ) A →

BA,¬A →

C →

DB,¬B →

B,D →

F C, ¬C →

¬D →

F D, ¬D →

Next let M

= {A, C}. This is a derivation of F from M

with top literal A

(weights are omitted, as not needed here):

=(A=⇒

A→B

C=⇒

C→D

=======⇒

B,D→F

is non-linear, since the second inference step violates linearity. Figure 5.1.4

in the introduction depicts the same derivation in an alternative notation

which emphasizes the tree character of derivations.

Example 5.2.2. As a non-trivial example consider the joint theory ES of

equality and strict orderings (Figure 5.5). The predicate symbol = is inter-

preted as an equivalence relation and the predicate symbol < is interpreted

as a strict ordering (i.e. as a transitive and irreﬂexive relation). Furthermore

we have included a single function symbol f of arity 1, which gives rise to

the substitution axiom ∀xx= x

→ f (x)=f(x

). The extension to a richer

signature is straightforward.

The corresponding initial system is given in Figure 5.6.

5.2 Inference Systems 161

Equivalence:

→ x = x (Ref=)

x = y → y = x (Sym=)

x = y, y = z → x = z (Trans=)

Strict Order:

x<x→ (IRef<)

x<y, y<z→ x<z (Trans<)

f-Substitution:

x = x

→ f(x)=f (x

) (Subf )

<-Substitution:

x = x

,x<y→ x

<y (Sub<-1)

y = y

,x<y→ x<y

(Sub<-2)

Figure 5.5. The theory ES of equality and strict orderings with unary function

symbol f. Here, and below the usual “→” notation is used for clauses.

Equivalence:

x = y, ¬(x = y) → F (Syn=)

¬(x = x) → F (Ref=)

x = y → y = x (Sym=-1)

x = y, y = z → x = z (Trans=)

Strict Order:

x<y, ¬(x<y) → F (Syn<)

x<x→ (IRef<)

x<y, y<z→ x<z (Trans<)

f-Substitution:

x = x

→ f(x)=f (x

) (Subf )

<-Substitution:

x = x

,x<y→ x

<y (Sub<-1)

y = y

,x<y→ x<y

(Sub<-2)

Figure 5.6. The inference system I

(ES).

162 5. Linearizing Completion

5.2.2 Completeness of Initial Inference Systems

The completeness result (wrt. unit-resulting refutations) of initial inference

systems is needed as a starting point for the proof of the completeness result

(wrt. unit-resulting and linear refutations) of the generated inference systems.

More precisely, the following line of reasoning applies: given a T -unsatisﬁable

literal set, by ground completenessa—possible nonlinear — refutation exists

in the initial inference system. By repeated generation of new inference rules

in a fair way (see the introduction) eventually an inference system is generated

that admits a linear refutation. Furthermore, deletion of redundant inference

rules does not destroy linearity.

Thus, ground completeness is the initial link between semantics and syn-

tax and plays much the same role as Birkhoﬀ’s completeness theorem (see

[

Huet and Oppen, 1980

]

) in Knuth-Bendix completion.

As explained in the informal presentation in the introduction, initial in-

ference systems constitute an “almost complete” calculus for the underlying

theory (cf. the example of the clause set S

there again). As was previously

stated, in order to obtain completeness it is necessary to access all positive

literals, no matter whether they are contained in the input set or contained

in the theory. Regarding this, we will slightly diﬀer from the introduction

in that we will not immediately compile away the “hidden” positive literals

A into a rule ¬A → F. Instead it is more convenient for us to deﬁne for an

inference system I the set

Punit(I)={A |¬A → F ∈I}

as the set of positive unit clauses from I. For example, Punit(I

(ES)) = {x =

x}, and in Example 5.2.1 we ﬁnd Punit(I

(T )) = {D}.

The set Punit(I) shall temporarily be accessible for derivations as addi-

tional input literals (later their usage will be compiled away by respective

transformation rules). But then it is clear that the present formalism is just

a reformulation of traditional Unit-Resulting resolution (which is biased to-

wards our completion application). Taking the soundness and completeness

of traditional Unit-Resulting resolution for granted, it is thus not surprising

that respective results can be obtained for our formulation. Nevertheless we

will state the precise ground completeness result here, since it will be needed

below.

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 ))).

For instance, it is easily veriﬁed that in Example 5.2.1 a I

(T )-refutation of

{A}∪Punit(I

(T )) = {A, D} exists, but a I

(T )-refutation of {A} alone

does not exist.

5.2 Inference Systems 163

Proof. By deﬁnition of T -unsatisﬁability, M is T -unsatisﬁable iﬀ M ∪T is

unsatisﬁable, where M is considered as a set of unit clauses. Since the unit-

clauses of T can be used as input literals (via Punit(I

(T ))) an existing

Hyper-resolution refutation of M ∪T can be reﬂected in our framework. For

an explicit proof from scratch see Appendix A, SectionA.2.1

We cannot be content with this completeness result because (1) the literals

from Punit(I

(T )) are needed, and (2) a linear derivation may not always

exist. For instance, there is no linear refutation of M

= {A, C} in Exam-

ple 5.2.1, either with top literal A or with top literal C.

5.2.3 Subderivations

We will have to access and replace subderivations within derivations. For this

let D be a I-derivation

D =(L

==⇒L

···L

==⇒L

n+1

)

It is apparent that

=⇒L

i+1

···L

j−1

===⇒L

for 1 ≤ i ≤ j ≤ n + 1 is a I-derivation of L

with top literal L

, called an im-

mediate subderivation of D; it is denoted by D|

i,j

. Immediate subderivations

with j = i + 1 are also called derivation steps.

Derivations may be concatenated. If E is a J -derivation of the form

E =(K

=⇒K

···K

==⇒K

m+1

)

and L

n+1

= K

then the concatenation of D and E, denoted by D · E,is

deﬁned as

D · E =(L

==⇒L

···L

==⇒K

=⇒K

···K

==⇒K

m+1

)

Evidently, D · E exists as I∪J-derivation from M ∪ N, where D (resp. E)

is a derivation from M (resp. N ). It is easily veriﬁed that this concatenation

is associative. Hence we can omit parenthesis when writing expressions as

D · E · F .

In order to recursively access subderivations we need the positions of

derivations. A position is a ﬁnite string over nonnegative integers and is

written in Dewey decimal notation. The empty string is denoted by λ. The

set of positions of D, P (D) is the smallest set satisfying:

1. λ ∈ P (D).

In the sequel the proofs can often be found in the appendix.

Inference rules and substitutions being omitted for brevity; the D

s stand for

sequences of derivations.