Building Theories into Instantiation

1 Introduction

Instantiation orderings over formulas (the relation of one formula being an instance of another) have long been central to the study of automated deduction and logic programming, and are of rapidly-growing importance to the study of database systems and machine learn­ ing (e.g., in inductive logic programming). One com­ mon way-perhaps the most common way-to build a theory of background information into a computational system based on instantiation is to generalize the ordi­ nary definition of instantiation to take account of the theory. The earliest work of this kind was Plotkin's C. David Page Jr.t Oxford University Computing Laboratory Wolfson Building, Parks Road Oxford OXl 3QD United Kingdom

*Email: frisch@minster.york.ac.uk. World-Wide Web: http:/ /dcpul .cs.york.ac.uk:9876/isg/frisch/home.html.

tEmail: dpage@comlab.ox.ac.uk. Supported by Esprit Basic Research Action 6020 on Inductive Logic Programming.

[1972] method of building an equational theory into res­ olution merely by replacing unification with the more general operation of unification with respect to the the­ ory, an operation he called "T-uni.fication" and is today called "E-unification." E-unification can be thought of as an operation used to obtain the greatest lower bound in an instantiation ordering that is relative to the built-in equational theory. Sorted logics can be thought of as log­ ics that incorporate background information about sorts, which are sets of objects in the domain. All automated deduction systems for sort.ed logic (e.g., [Walther, 1987; Cohn, 1987; Schmidt-Schauss, 1989; Frisch, 1991]) per­ form sorted unification, which, once again, can be thought of as an operation used to obtain the greatest lower bound in an instantiation ordering with a built-in theory about sorts.

This paper presents an instantiation ordering for con­ straint logic, a logic that generalizes previous logics that incorporate background information, and proves that previous instantiation orderings are special cases of this ordering. Furthermore, Section 5 shows the utility of this generalized instantiation ordering by discussing ap­ plications to (1) induction and inductive logic program­ ming, (2) deduction and logic programming, and (3) knowledge-base vivification. We are currently investi­ gating applications to constraint databases and database query languages as well. The extension to constraint logic is vital for each of these applications.

After defining our generalized instantiation ordering, we identify two semantic properties that one should ex­ pect of instantiation orderings, properties that make in­ stantiation orderings useful. Theorem 2 establishes that our general instantiation ordering has these properties; consequently (because of the nature of these properties) all special cases of the general ordering must have these properties.

A major consequence of defining instantiation in such a general setting is that the traditional substitution­ based definitions are inadequate. The definition of in­ stantiation presented in this paper (Section 3) does not involve substitutions; it is primarily semantic. Two of the principle theorems of this paper, Theorems 3 and 6, each identify conditions under which an instanti­ ation ordering can be based on substitution. Examples are presented that show that substitution-based defini­ tions cannot be guaranteed to work when these conditions are not met. Thus, this paper demonstrates that substitution-based definitions, such as that embodied in E-unification, are not applicable in all generalized set­ tings, and the paper identifies some of the limits of ap­ plicability. For example, we see that the instantiation ordering for sorted logic can be generalized from sorts to arbitrary predicates provided that there are no built-in equations. However, if there are built-in equations, then additional conditions, which are identified in the paper, must be met.

By showing that sorted logic meets the conditions of Theorem 3, and that logic with built-in equations meets the conditions of Theorem 6, we are able to prove that the instantiation orderings associated with these two log­ ics are special cases of our general instantiation ordering. These proofs are simple, suggesting that it also may be simple to prove that other instantiation orderings are special cases of the general ordering. Other properties, such as the existence of least upper bounds and greatest lower bounds and the finiteness of antichains, ascending chains, and descending chains, hold only in some instan­ tiation orderings. Elsewhere sufficient conditions for ob­ taining these algebraic properties are presented [Page, 1993].

2 Constrained Formulas and Constraint Theories

A constrained formula is composed of two ordinary for­ mulas, one called the head and the other called the con­ straint. The constraint can be any formula whose pred­ icates are drawn from a distinguished set of predicates called constraint predicates. In addition, TRUE is a con­ straint and has the obvious interpretation. We stipulate that the interpreted equality predicate ( "=") is a con­ straint predicate. For clarity, constraint predicates (ex­ cept equality) are written in small capital letters, e.g. "ELEPHANT." The head of a constrained formula can be any formula that contains no constraint predicates. We require that every variable that has a free occurrence in the constraint also has a free occurrence in the head. Constraint formulas are written in the form ¢>/C, where ~ is the head and C is the constraint.

But what does a constrained formula mean? In all the applications of constrained formulas that we know about, the variables in the formulas are either all univer­ sally quantified or all existentially quantified.1 Where ¢> is any formula (ordinary or constrained), we say that the universal closure of ¢> is the result of universally quanti­ fying all free v~iables in ¢>, and we denote the universal closure of ¢> by V¢>. Similarly, the existential closure of ¢> is the result of existentially _guantifying all free variables in ~' and it is denoted by 3¢>. If ¢>/C is a constrained formula, then we define V(¢>/C) to be logically equiva­ lent to V(C -t ¢>),and 3(¢>/C) to be logically equivalent to 3(C 1\ ¢>).

Operations on constrained formulas act with respect to background information about the constraint predi­ cates. This background information takes the form of a

1 In fact, substantial difficulties confront attempts to mix the quantifiers on constrained formulas .

• :Et = {Vx UNIV(x), ELEPHANT(clyde) V IN-CIRCUS(clyde), ELEPHANT{jumbo) V IN-CIRCUS{jumbo), GRAY(mom(clyde)), GRAY(mom(jumbo)) , 'lx ELEPHANT(x) -t ELEPHANT(mom(x)}, 'lx ELEPHANT(x) -t MAMMAL(x)}.
• :E2 = {party( arnold) = republican, spou.!e( maria) = arnold, .!powe( arnold) = maria, BIGGER( arnold, maria), KENNEDY( maria), Vx KENNEDY(x) -t (party(x) = democratic), LEGISLATURE( U.!-house), LEGISLATURE( us-senate)}.

:E3 = {VxVy (f(x, y) = f(y, x)), (c =a) V (c =b)}.

Figure 1: Three Constraint Theories

constraint theory. A constraint theory is any (possibly infinite) satisfiable set of sentences all of whose pred­ icates are constraint predicates. Figure 1 gives three examples of constraint theories, called :E1, :E2 and :E3. Notice that :E1 contains monadic constraint predicates only. Therefore, we also call it a sort theory. 2

The following definitions are used throughout the pa­ per. A value assignment is an assignment of individuals from the domain of a given model to all free variables. Let :E be a constraint theory, and let M be a model. We say that M is a :E-model if and only if M satisfies :E. We say that a constraint that is satisfied by some :E-model and some value assignment is :E-satisfiable. Where :E is, more generally, any (possibly infinite) first-order theory, and 1/J1 and 1/J2 are logical sentences, we say that 1/J1 :E­ entails 1/J2 if and only if :E U { 1/J1 } I= 1jJ2, and we write 1/J1 F:E 1/J2- More generally, where ¢>1 and ¢>2 are logi­ cal formulas, we say that ¢>1 :E-entails ¢>2 if and only if any :E-model and value assignment that satisfy ¢>1 also satisfy ¢>2. A quasi-ordering, or preorder, is a relation that is reflexive and transitive. Alternatively, a quasi­ ordering may be thought of as a relation that partitions a set into equivalence classes and partially orders those equivalence classes. It is straightforward to verify that F:E is a quasi-ordering on constraints.

A constrained formula is admissible with respect to constraint theory :E, or :E-admissible, if its constraint is :E-satisfiable. Otherwise, it is :E-inadmissible. The remainder of the paper considers only constrained for­ mulas that are admissible with respect to the constraint theory under consideration. Thus "constrained formula" always means ":E-admissible constrained formula."

Let ¢> be any formula with n top-level term occur­ rences, that is, n occurrences of terms as arguments to predicates. Number the occurrences from 1 to n in left-to-right order, as they appear in ¢>. We use ¢>[t1, ... , tn] to denote a formula whose ith top-level term occurrence is ti, for all 1 :5 i :5 n. Sub­ sequently we use ¢>[t~, ... , t~] to denote the formula that results from replacing the ith top-level term oc­ currence in ¢>[ t1, ... , tn] with t~, for all 1 :5 i :5 n. For example, if ¢>[/ (a), f (a), g ( c, x)] denotes the formula p(f(a)) 1\ q(f(a), g(c, x)) then ¢>[g(a, b), c, f(x)] denotes p(g(a, b)) 1\ q(c, f(x)).

2 Monadic constraint predicates are often referred to as .!orts.

3 The General Instantiation Ordering

The ordinary instantiation ordering on ordinary formu­ las is particularly useful for three reasons. First, if ¢11 ~ ¢12 then the set of ground instances of </11 is a superset of the se_!. of gro_!!nd inst~ces of .!/?2· Second, if ¢11 ~ ¢12 then V¢11 F V¢12 and 3¢12 F 3¢11· Third, for atomic formulas (atoms), this second statement is an if and only if; that is, the follow_!!lg thre~ statements are equivalent: (1) </11 ~ ¢12, (2) V¢11 F V¢12, and (3) 3¢12 F 3¢~1 . We seek an instantiation ordering for con­ strained formulas that has analogous properties, where we replace entailment with 'E-entailment and ground in­ stances with ground "'E-instances", or ground instances under the new ordering.

Definition 1 ('E-more general) Let 'E be a constraint theory. Let <Pt/C1 and <P2IC2 be constrained formulas and let v be the free variables of ¢11· Let <P~Iq be a variant of ¢12IC2 that shares no free variables with ¢11. We say that <PtfC1 is 'E-more general than <P2IC2 (written <Pt/C1 ~E <P2IC2) if and only if </11 is of the form <fo[t1, ... , tn], <P~ is of the form <P[t~, ... , t~] and C2 FE 3v tt = t~ 1\ ... 1\ tn = t~ 1\ c1.

As an example, the constrained formula

controls(party(spouse( arnold)), x, 1993)/LEGISLATURE(x)

is 1::2-more general than the constrained formula

controls( democratic, y, 1993)/(y = us-house)

because

y = us-house FE 2 3x party(spouse(arnold)) =democratic 1\ x = y 1\ 1993 = 1993 1\ LEGISLATURE(x).

For another example, observe that p(f(c, x)) ~E3 p(f(a, b)) because FE 3 3x f(c, x) = f(a, b). This ex­ ample illustrates the difficulty with using a substitution­ based definition of instantiation in this general setting. For example, under the standard instantiation order­ ing associated with E-unification p(f(a, b)) is not an instance of p(f(c, x)); there exists no substitution that maps f(c, x) to a term that is equal to f(a, b) according to the equational theory 'E3.

Like the usual instantiation ordering for formulas of FOPC, the ~E ordering on constrained formulas is not a partial ordering but a quasi-ordering, or preorder, for any choice of 'E. Because ~E is a quasi-ordering, if </11 I C1 ~ E ¢12 I c2 then every ground instance of ¢12 I c2 is also a ground instance of <Pt/C1. Thus the ~E ordering is analogous to the ~ ordering on ordinary atoms in at least one of the three ways we wanted it to be. What about the other two? Theorem 2, which follows, reveals that the ordering ~E for constrained formulas is analogous to the ordering ~ for ordinary formulas in these ways as well.

Theorem 2 Let <PtfC1 and <P2IC2 be constrained for­ mulas, and let 'E be a constraint theory. If <Pt/C1 ~E <P2IC2 then V(<PtfCt) FE V(¢12IC2) and 3(¢121C2) FE

3(¢1tfC1). Furthermore, if</11 and </12 are atoms then the following three statements are equivalent: {1} <Pt/C1 ~E ¢12IC2, {2} V(<PtfCt) FE V(¢12IC2), {3} 3(¢12/C2) PE 3(¢1t/Ct) . 3

If we wanted to extend the 'E-more general ordering to include 'E-inadmissible constrained formulas as well, all three of the desired properties of the ordering are re­ tained if we specify that the 'E-inadmissible constrained formulas are the least formulas in the ordering. In other words, we retain the properties if for any constrained formulas <Pt/C1 and <P2IC2, if <P2IC2 is 'E-inadmissible then <fot/C1 ~E </12IC2.

4 The Relationship to Substitution-based Orderings

This section shows that other, established instantiation orderings for various restricted classes of constrained formulas and constraint theories are equivalent to the 'E-more general ordering (given the appropriate restric­ tions). Our analysis is based on Theorem 3 and Theo­ rem 6, which under specified conditions provide alterna­ tive, substitution-based characterizations of the ~E or­ dering. Using these theorems it is easy to equate the ~E ordering with various established orderings. For brevity, we consider only two of the best-known orderings.

The following theorem gives a substitution-based char­ acterization of the instantiation ordering when neither the constraints nor the constraint theory contains equal­ ity.

Theorem 3 Let <PtfC1 and <P2IC2 be constrained for­ mulas and let 'E be a constraint theory, none of which contains the equality predicate. Then <Pt/C1 ~E <P2IC2 if and only if there exists a substitution () such that ¢118 = ¢12 and c2 FE (Cl8).

The following is an example of this characterization.

To see this consider any substitution () that maps x to z andy to mom(z).

This characterization of ~E is in fact the instantiation ordering for a restricted class of equality-free constrained formulas that Page and Frisch [1992] used in their study of constrained generalization. Thus this theorem tell us that the ordering used by Page and Frisch is a special case of the ordering defined in this paper.

To see why equality is forbidden, consider an ex­ ample where 'E = {VxVy(f(x,y) = f(y,x))} . Then p(f(b, x)) ~E p(f(a, b)), but not according to the char­ acterization. Similarly, consider a case where 'E is empty but equality appears in a constraint: p(a) ~E p(b)l(a = b), but not according to the characterization.

Taking a hint from the definition of E-unification, it appears that the above examples could be handled if the characterization in the above theorem were to test not for simple equality, but rather for equality according to the theory E. We now formulate a substitution-based characterization motivated by this idea, prove that it is correct under certain conditions, and show by example that this approach cannot always work. The characteri­ zation allows equality in the constraint theory, E, though not in the constrained formulas.

3 All proofs are omitted from this paper, but appear in a longer, unpublished version of this paper. The proofs of The­ orems 2, 3 and 6 are long and involved. Theorems 9 and 10 follow straightforwardly from Theorems 3 and 6, respectively.

We now provide several additional definitions that are needed. The definition of homomorphism between mod­ els, which follows, is standard. The definition of initial model, taking into account the truth values of predicates, is taken from Goguen and Meseguer [1986].

Definition 4 (Homomorphism between models) Let M and M' be models with domains D M and DM, respectively. Then a function h : D M -+ D M' is a ho­ momorphism from M to M' if and only if:

• for every function symbol f of arity n 2: 0, M M' h((J] · (d1, ... , dn)) = [!] (h(di), ... , h(dn)) and
• for every predicate symbol p of arity n 2: 0, if [p]M(db···,dn) = 17-ue then we also have M' [p] (h(di), ... , h(dn)) = 17-ue,

where (d1, ... , dn) is a;..y n-tuple of individuals in D M.

Definition 5 (Initial Model) Let E be any theory of first-order logic with equality. A E-model M is an initial model of E if and only if there exists a unique homomor­ phism from M to any other E-model.

The reader can confirm that E2 has an initial model, but that neither E1 nor E3 do. To see that E1 has no initial model observe that there is no homomorphism in either direction between any E1-model that satisfies ELEPHANT (jumbo) and falsifies IN-CIRCUS(jumbo) and any E1-model that falsifies ELEPHANT (jumbo) and satis­ fies IN-CIRCUS(jumbo ).

Theorem 6 Let E be a constraint theory in Skolem Normal Form that has an initial model. Let ¢>[tb ... , tn]/C1 and </>[t~, ... , t~]/C2 be constrained for­ mulas, where cl and c2 a~ conjunctions of atoms. Then </>[h, ... , tn]/Cl 2::E </>[t~, ... , t~]/C2 if and only if there exists a substitution o such that c2 P:E ( c1 O) and c2 FE ti(} = ti, 1 ~ i ~ n. 4

Let's return to an earlier example to illustrate this characterization. Recall the constraint theory E2 , and consider the following pair of constrained formulas.

In the notation of Theorem 6, t 1 is party(spouse(x)), t 2 is y, t3 is 1993, t~ is party(z), t~ is us-house, and t; is 1993. In addition, C1 is (BIGGER( X, maria) t\ LEGISLATURE(y)) and C2 is KENNEDY(z). Let (} map x to arnold and y to us-house. Clearly c2 P:E2 (CIO), c2 P:E2 (t2(} = t~), and C2 P:E2 (t30 = t;); these would hold even if C2 were simply TRUE. The interesting part of this example is that c2 P:E2 ( t1 o = tU; note that both c2 and o are involved nontrivially.

4 We found it quite surprising that this last condition (C2 FE ti(} = tD had to involve c2 even though c2 is non­ equational. An example illustrating the need for this will be presented.

The following examples show that without the addi­ tional restrictions the characterization of Theorem 6 is incomplete. The examples are similar; in the first exam­ ple, the constraint theory does not have an initial model, because of the disjunction, and in the second, the con­ straint of one constrained formula contains disjunction. For the first example, let E be

Then

but not according to the characterization. For the second example, let E be the theory {VxVy(f(x,y) = f(y,x))}. Then

but not according to the characterization.

We are now prepared to relate the 2::E ordering to two established orderings.

4.1 The Instantiation Ordering for Sorted Logic

As noted in the Section 1, if the predicates in a constraint theory are monadic, the theory is called a sort theory. In sorted logic, the constraint theory is a sort theory, and the formulas are sorted formulas. A sorted formula is a constrained formula whose constraint is a conjunction of atoms built from monadic constraint predicates and vari­ ables that appear in the head, such that each variable occurs at most once in the constraint. Because of these additional restrictions on the constraints of sorted formu­ las, sorted formulas are often represented in an alterna­ tive, in-line syntax, in which the constraints are attached directly to the variables. Thus, for example, the sorted formula eats(x,y)jELEPHANT(x) t\ VEGETABLE(y) may be expressed as eats(x:ELEPHANT,y:VEGETABLE).

Definition 7 (In-line Representation) Let <1>/(rl(xl) t\ ... t\ Tn(xn)) be a sorted formula. Then a is the in-line representation of </>/C if and only if a re­ sults from replacing every occurrence of the variable Xi in </> with an occurrence of the sorted variable Xi:Ti, for all1 ~ i ~ n.

The additional restrictions on sorted formulas make possible another definition of an instantiation ordering on sorted formulas (called S-more general, or 2:s, in Def­ inition 8), in which substitutions are central; this is the established instantiation ordering for sorted formulas. Theorem 9 states that this established ordering on sorted formulas is the same as the 2::E ordering, provided a small additional assumption is made. The assumption is that every sort contains at least one individual, and it is made for the established ordering anyway [Frisch, 1991]. The definition of the established ordering for sorted formulas, given below, is based on the alternative syntax for sorted formulas.

Definition 8 (S-more general) Let S be a sort the­ ory such that for every sort T we have S f= 3x r(x) (according to S every sort contains some individual). A substitution 9 is well-sorted with respect to S if and only if for any variable x:r, x :r9 = t where S f= Vr(t). A sorted formula a 1 is S -more general than another, a 2 , if and only if a18 = a2 for some substitution 9 that is well-sorted with respect to S. If a 1 is S -more general than a2, we write a1 ~s a2.

It is worth noting that because we require that S f= 3x r(x) for each sort r, every sorted formula is E­ admissible.

Theorem 9 Let a 1 and a 2 be the in-line representa­ tions of sorted formulas </JI/C1 and <P2/C2, respectively. Let S = E be a sort theory such that for every sort T, S f= 3x r(x). Then </JI/C1 ~E </J2/C2 if and only if a1 ~s a2.

4.2 E-Unification

E-unification is a form of unification that takes into ac­ count a set of equations (universally closed atomic for­ mulas formed with the equalitl predicate symbol), E.'> Following standard definitions, if sands' are terms, we say that s = E s' if and only if the pair (s s') is a member of the finest congruence_ on the term algebra containing all pairs (tB t'B), where V(t = t') is a member of E and 9 is a substitution. We say that 9 is an E-unifier of s and t if and only if s9 = E tB. Associated with this notion of E­ unifier, is an instantiation ordering over the set of terms: s ~E t if and only if s9 =e t for some substitution 9. We can straightforwardly extend these standard definitions to generate an ordering over formulas: </J[ t1, . . . , tn] ~ E 1/J if and only if 1/J is of the form </J[t~, ... , t~] and for some 0, ti() =e ti for every 1 ~ i ~ n.

Observe that t = E t' if and only if E f= t = t'. Also observe that any set of equations is in Skolem Normal Form and has an initial model . From these observations and Theorem 6, the correspondence between ~E and ~E follows immediately.

Theorem 10 Let E = E be a set of equations and </J and 1/J be formulas. Then <P ~E 1/J if and only if </J/TRUE ~E 1/J/TRUE.

5 Applications

The introduction to this paper mentioned many appli­ cations of the instantiation orderings for ordinary first­ order logic, for logic with built-in equational theories and for sorted logic. This section extends the discus­ sion to applications that employ the generalized order­ ings characterized by Definition 1 and by Theorems 3 and 6. The application areas discussed are (1) induc­ tion and inductive logic programming, (2) deduction and logic programming, and (3) knowledge-base vivification.

5 Jaffar, Lassez, and Maher [Jaffar et al., 1986) relax this restriction to allow E to be any set of definite clauses whose only predicate is the equality predicate.

6 For example, see the survey by Siekmann [1989] .

Inductive Logic Programming: ILP focuses on inductive learning using a first-order representation, specifically a definite clause representation [Muggleton, 1992]. At the foundation of ILP is the work of Plotkin [1970] and Reynolds [1970] on the computation of least upper bounds for ordinary logic. This foundational work has been extended by Frisch and Page to cover sorted logic (based on Theorem 9) [Frisch and Page, 1990], and then further to constraint logic (using a special case of the characterizations of Theorem 3 and Theorem 6) [Page and Frisch, 1992]. The extension to constraint logic can also be viewed as an extension of Buntine's [1988] definition of generalized subsumption.

One active area of ILP research over the last four years has been the study of PAC-learnability of restricted classes of definite clause concepts, relative to various classes of definite clause background theories; this work is summarized in [Cohen and Page, 1995]. The earliest results (both positive and negative) within this area ac­ tually were proven using the aforementioned extensions of the work of Plotkin and Reynolds based on special cases of the orderings developed in this paper [Page and Frisch, 1992]. Crucial to these results are the semantic properties of these orderings, as provided in the theo­ rems of this paper.

These early results on learnability in ILP have been extended significantly to yield a positive result that ap­ plies to structural domains, such as molecular biology or blocks world problem solving [Page, 1993]. The foun­ dation of this extended result is the characterization of instantiation in Theorem 6, which allows equality in the background theory. The extended result general­ izes Haussler's [1989] learnability result for structural do­ mains with subset queries in a number of ways, the most significant of which are: (1) the ability to learn disjunc­ tive concepts, and (2) the use of much richer background theories (for example, background theories that are not restricted to use only unary predicates). FUrthermore, it can be shown that this result subsumes i:nost of the positive PAC-learnability results for ILP (though not the positive PAC-prediction results). 7

Deductive Systems: Constraint logic has been used as the basis of constraint logic programming [Jaffar and Lassez, 1987; Hohfeld and Smolka, 1988] and in gener­ alizations of certain deductive systems [Biirckert, 1991; Frisch, 1994]. Such systems typically employ a resolu­ tion inference rule that generalizes the ordinary rule of resolution. Let us first observe how the ordinary rule of resolution is based on the ordinary instantiation or­ dering, and then consider how this inference rule can be generalized to constraint logic by basing it on our instan­ tiation ordering for constraint logic.

The ordinary rule of resolution operates by tak­ ing most-general instances of the two parent clauses such that the two literals being resolved upon become complements (that is, identical but opposite in sign).

7 For PAC-predictability as opposed to PAC-learnability, the final hypothesis need not have any particular form (e.g., a logic program or a propositional DNF formula) .

This is accomplished by computing the most-general unifier and applying it to the clauses being resolved. This idea can be generalized to obtain a resolution rule for constrained clauses. To resolve constrained clauses P(tt, . . . , tn) V </J/C and -,P(t~, ... , t~) V </J' /C' we need to find the most general common instance of P(t17 ··· , tn)/C and -,P(t~, . .. ,t~)/C'. Using Defini­ tion 1 it can be confirmed that P(t1, ... , tn)/C (or, equiv­ alently, P(t~, . . . , t~)/C), where Cis lt = t~ 1\ ···A tn = t~ !\C 1\C', is a most-general common instance, provided C is 1:-satisfiable. Consequently, the desired resolvent is cpVq/jC.

In some simple constraint logics, such as some sorted logics, a most general common instance may not exist, in which case the above resolution rule must generate many resolvents to take account of the multiple maximally­ general, but incomparable, common instances. The longer version of this paper identifies conditions suffi­ cient for the existence of greatest lower bounds.

The completeness of resolution and similar inference systems is usually proved by a Herbrand Theorem, which relates the satisfiability of non-ground clauses to the satisfiability of their ground instances, and a Lifting Theorem, which relates non-ground derivations to their ground instances. In a series of papers, Frisch has shown how, under certain conditions, the proofs of these theorems can be systematically transformed to obtain proofs of the corresponding theorems for inference sys­ tems based on instantiation with built-in theories. These results have been formulated for sorted logic based on the characterization of Theorem 9 [Frisch, 1991], for modal logic based on the characterization of Theorem 3 [Frisch and Scherl, 1991], and for arbitrary constraint logic based on a characterization equivalent to that of Definition 1 [Frisch, 1994].

Though not immediately obvious, the preceding dis­ cussion applies equally to many systems for automated deduction in modal logic. As is well-known, modal logic often can be viewed as implicit discourse about possible worlds and, therefore, can be translated to non-modal logic that explicitly discusses possible worlds. Frisch and Scherl [1991] show that for many modal logics the sentences resulting from this translation can be trans­ formed into constrainted formulas in which the accessi­ bility conditions among possible worlds appear solely in the constraints. From this point of view, the path uni­ fication algorithms employed by many modal deduction systems [Ohlbach, 1988; Jackson and Reichgelt, 1989; Wallen, 1990] can be seen to be solvers for such con­ straints. In other words, these path unification algo­ rithms compute the greatest lower bounds in the instan­ tiation ordering.

Knowledge Base Vivification: The premise of viv­ ification is that much of the complexity of automated deduction arises from incomplete knowledge in knowl­ edge bases (KBs), in particular from disjunctions leading to reasoning by cases [Borgida and Etherington, 1989; Etherington et al., 1989; Levesque, 1988]. To use an ex­ ample from Levesque [1988], suppose our KB includes age(fred, 71) V age(fred, 72). Many of the interesting consequences of this fact follow from Fred being in his early seventies or, even more generally, being a senior citizen. If we know that 71 and 72 belong to the category low­ seventies, we might replace age(fred, 71) V age(fred, 72) with 3x (age(jred, x)/LOW-SEVENTIES(x)). Of course, examples that involve binary predicates in the back­ ground information (rather than just categories such as low-seventies) or function symbols require more care.

Based on the characterization of instantiation in The­ orem 3, an efficient vivification algorithm can be de­ fined that handles higher-arity predicates and function­ symbols [Page, 1993]. As a simple example of the algo­ rithm's behavior, suppose our KB contains the following sentence.

intimidates(son(iumbo), son( clyde)) V intimidates( son(Jred) , son(ioe))

Suppose our knowledge base also tells us that Jumbo is bigger than Clyde, Jumbo's son is bigger than Clyde's son, Fred is bigger than Joe, and Fred's son is bigger than Joe's son. Then the vivification algorithm replaces the preceding sentence with the following existentially­ closed constrained formula.

3x3y (intimidates(son(x), son(y))/ BIGGER(x, y) !\ BIGGER(son(x ), son(y)))

While some information is lost in the replacement, much of the useful information is retained and the disjunction is eliminated.

6 Conclusion

This paper has presented a general instantiation order­ ing for constrained formulas to which the established in­ stantiation orderings for various restricted classes of con­ strained formulas are equivalent. This ordering allows us to prove, at once, semantic properties of all these instan­ tiation orderings. The utility of building theories into instantiation has been established by a long history of applications in automated deduction and a short history of applications in automated induction. We anticipate that instantiation with built-in theories will continue its key role in deductive reasoning and will play an increas­ ing role in non-deductive reasoning.