A Semantic Theory of Abstractions

1 Introduction

Abstractions and approximations are pervasive in hu­ man common-sense reasoning and problem-solving. Ab­ stractions have been used in a variety of problem­ solving settings including planning [Sacerdoti, 197 4], theorem proving [Plaisted, 1981], diagnosis [Davis, 1984; Genesereth, 1984; Struss, 1992], compositional model­ ing [Falkenhainer and Forbus, 1991], constraint satisfac­ tion [Ellman, 1993], and automatic programming [Lowry, 1989]. Until recently there has been no unifying account of these disparate forms of abstractions. However, in the last few years, there has been an explosion of interest in understanding the underlying principles of abstrac­ tions and approximations [Ellman, 1992; Lowry, 1992; van Baalen, 1994].

A comprehensive theory of the principles underlying abstractions is useful for a number of reasons. Such a

Alon Y. Levy

AT&T Bell Laboratories AI Principles Research Department 600 Mountain A venue, Room 2C-406 Murray Hill, NJ 07974. levy@research. att. com

theory can provide the means for clearly undertJtanding the different types of abstractions and approximations used in past work. It can provide semantic and com­ putational jutJtification!J for using abstractions and ap­ proximations. Furthermore, such justifications can be used to automatically contJtruct useful abstractions and approximations. Finally, an understanding of different abstractions within a common framework can allow the trantJfer of techniques between disparate domains.

Recently, Giunchiglia and Walsh have presented an el­ egant theory of abstractions that unifies past work and provides a vocabulary to discuss different types of ab­ stractions [Giunchiglia and Walsh, 1992]. Their the­ ory characterizes abstractions as syntactic mappings be­ tween formulas of formal systems. They classify abstrac­ tions according to whether the set of theorems of the abstract theory are a subset, superset, or equal to the set of theorems of the base theory (TD, Tl, and TC abstractions, respectively). Their theory is very good at capturing an important aspect of many abstractions, viz., many abstractions result directly from syntactically manipulating formulas. Moreover, problem solvers ulti­ mately reason by applying inference rules to formulas, and hence understanding the properties of abstractions as mappings between formulas is essential.

However, viewing abstractions as syntactic mappings captures only one aspect of abstractions. Consider the following example.

Example 1 Predicate abtJtraction!J [Plaisted, 1981; Tenenberg, 1990] are a class of abstractions based on the observation that the distinctions between a set of predicates P1 , ... , Pn in a theory are often irrelevant. An abstract theory can be constructed by replacing all occurrences of the P1 's in the base theory by a single ab­ stract predicate P. For example, consider the following base theory:

The distinction between JapaneseCar and EuropeanCar is often irrelevant (e.g., when trying to answer a query Car(A)), and therefore these predicates can be replaced by ForeignCar, yielding the following simpler abstract theory:

However, suppose the base theory also includes the fol­ lowing:

Applying the same mapping to axioms 3 would result in the following:

However, adding these axioms to the axioms in (2) leads to false proofs [Plaisted, 1981], which may be undesir­ able. For example, one can infer that Toyotas are fast, and BMWs are reliable-inferences not sanctioned by the base theory.

The syntactic theory of abstractions does distinguish between abstractions that yield false proofs (TI) and those that don't (TD). However, it gives no guidance in comparing TD abstractions to determine which is more natural. For example, the axioms in (2) and (4), when used independently, will not yield false proofs, but the former is more natural, considering the intended inter­ pretation of ForeignCar . 1 Nor does the syntactic the­ ory tell us how to construct the strongest such abstrac­ tion. For example, we will see that adding the axiom

to (2) yields the strongest theory that removes predicates JapaneseCar and EuropeanCar and still does not ad­ mit false proofs. D

The fundamental shortcoming of the syntactic theory is that while it captures the final result of an abstrac­ tion, it does not capture the underlying justification that leads to the abstraction. In this paper we present a se­ mantic theory of abstractions that addresses this short­ coming. Our theory is based on the idea that knowledge representation involves using formulas to capture an in­ tended domain model. From this perspective, we argue that an abstraction should be performed in two steps: first, the intended domain model is abstracted and then a set of (abstract) formulas is constructed to capture the abstracted domain model. Hence, we argue that the decision of what to abstract is made at the model level (using knowledge about relevant aspects of the do­ main), with the syntactic transformation being justified by this decision. In our example, the intended abstrac­ tion to the domain model is to replace the relations de­ noted by JapaneseCar and EuropeanCar by one rela­ tion representing their union, denoted by ForeignCar. As mentioned earlier, the strongest theory that imple­ ments this intended abstraction consists of the axioms in (2) and (5).

1 Note that, since the axioms in (1) and (3) are mutually disjoint, the preorder !;;;; defined in [Giunchiglia and Walsh, 1992] provides no help in selecting between the two options.

We introduce a class of model increasing (MI) abstrac­ tions, a strict subset of TD abstractions. Like TD ab­ stractions, MI abstractions yield no false proofs. How­ ever, they have additional natural properties such as compositionality. We show that the abstract theory that precisely implements the intended model level abstrac­ tion, is exactly the strongest MI abstraction of a base theory. We show that if the base theory is axiomatizable, then so is its strongest MI abstraction. We present a pro­ cedure to automatically construct the strongest MI ab­ straction. Our work generalizes Tenenberg's treatment of predicate abstractions [Tenenberg, 1990j, and we dis­ prove his conjecture that the predicate abstraction of a finite theory is always finitely axiomatizable.

Abstractions that admit false proofs are commonly used to speed up problem solving by guiding search, e.g., ABSTRIPS [Sacerdoti, 1974]. We show that all such abstractions can be viewed as MI abstractions in conjunction with a set of simplifying a$sumptions. For example, in ABSTRIPS, we first make the simplifying assumption that a predicate of lower criticality can al­ ways be achieved without affecting predicates of higher criticality, and then we construct an MI abstraction by dropping the appropriate preconditions. This formaliza­ tion is insightful because it shows that an abstraction will yield false proofs only when the simplifying assump­ tion is violated. This enables us to evaluate the utility of an abstraction depending on the reliability of the sim­ plifying assumption.

2 Abstractions as model mappings

Our theory of abstractions applies to any language with a declarative semantics, e.g., propositional logic, con­ straint languages, first-order logic, modal logic. The declarative semantics of such languages is provided by interpretations of the language and the the notion of satisfaction. An interpretation, I, is a model of a set of sentences, E, (denoted I ~ E) if and only if I satisfies each sentence in the set. A set of sentences T1 entails another set of sentences T2 (denoted T1 ~ T2) if and only if every model of T1 is a model of T2.

2.1 Model increasing abstractions

Let Tbau and Tab· be sets of sentences in languages Lba·· and Lab·, respectively. What does it mean for Tab· to be an abstraction of Tbau? If Lba·· and Lab· are the same language, natural definitions are possible (e.g., Tbau ~ Tab· is one such option). However, if Lba·· and Lab· are different, such a direct comparison is not possible since Lbau and Lab· have no common interpretations. A comparison is possible only if there is a way of translating between the interpretations of the two languages. Such a translation can be specified by an abstraction mapping 1r (Section 3.1 shows how to formally specify 1r):

The idea is that 1r is a model level specification of how the interpretations of Lba·· are to be abstracted to in­ terpretations of Lab·. Recall that we view abstractions as consisting of two steps: first, the intended domain model is abstracted and then the abstract theory is con­ structed to capture the abstracted domain model. Given only Tba·e, any of its models could be its intended model. Hence, Tab· is an abstraction of Tbau, given the abstrac­ tion mapping 71'", if and only if Tab· captures all the ab­ stracted models of Tbau· This motivates the following definition of model increa&ing (MI) abstractions:

Definition 1 (Model increasing abstractions) Let Tba·e and Tab· be &et& of &entence& in language& Lbaoe and Lab·, re&pectively. Let 71'" : Interpretation&(Tbau) -t Interpretation&(Lab·) be an ab&traction mapping. Tab· i& a model increa&ing ab&traction of Tba·e, with re&pect to 71'", if for every model Mbau ofTbau 1 7r(Mbau) i& a model of Tab··

Example 2 Consider the predicate abstraction in Ex­ ample 1. Let the axioms in (1) and (3) be the base the­ ory. Given any model of the base theory, the abstraction mapping 71'" defines the extension of the abstract predi­ cate ForeignCar to be the union of the extensions of JapaneseCar and EuropeanCar. One can verify that the axioms in (2) and (5) form an MI abstraction of the base theory, i.e., the image of every model of the base theory is a model of (2) and (5). However, the axioms in ( 4) are not part of any MI abstraction of the base the­ ory, e.g., the image of a model of the base theory which has an unreliable European car is not a model of these axioms. D

A variety of commonly used abstractions are MI ab­ stractions. For example, sign algebras [Williams, 1991] and quantity spaces [Kuipers, 1986] are MI abstractions of the real algebra. Structural and behavioral abstrac­ tions used in model-based diagnosis [Genesereth, 1984; Hamacher, 1991] are MI abstractions. Ground abstrac­ tions, where a clause is replaced by (some of) its ground instances, used in theorem proving [Plaisted, 1981] are MI abstractions. These applications exploit the follow­ ing important property of MI abstractions:

Proposition 1 Let Tab· be an MI ab&traction of Tbau. If Tab· i& incon&i&tent, then Tbau i& incon&i&tent.

Proof: If Tbau were consistent, it would have a model, and the image of this model would be a model of Tab·, making Tab· consistent. D

In other words, to prove the inconsistency of a base theory, it suffices to prove the inconsistency of a (po­ tentially simpler) MI abstraction. Another important property of MI abstractions is compo&itionality:

Proposition 2 Let Tab· and Sab· be MI ab&traction& of Tbau and Sbau, re&pectively, with re&pect to 7r. Then Tab· U Sab· i& an MI ab&traction of nau U Sba·e, with re&pect to 71'".

Proof: Let Mba·e be any model of Tbau U Sbau· Hence, Mbaoe is a model of both Tbaoe and Sbau, and hence 7r(Mbau) is a model of both Tab· and Sab" and hence a model of Tab· U Sab·. D

Compositionality is exploited in diagnosis with multi­ ple theories [Nayak, 1994b], and in compositional mod­ eling [Falkenhainer and Forbus, 1991; Nayak, 1994a;

Nayak and Joskowicz, 1996; Iwasaki and Levy, 1994] where theories are built by composing knowledge from different sources. Moreover, one may argue that inde­ pendent of these applications, theory compositionality is intrinsic to the very notion of abstractions.

When Tab· is an MI abstraction ofTbau, Tab· can have models that are not the image of any model of Tbaw Therefore, an MI abstraction can be weaker than the in­ tended model-level abstraction. This motivates the def­ inition of the &tronge&t MI abstraction, which exactly implements the intended model-level abstraction:

Definition 2 (Strongest MI abstraction) Tab· i& the &tronge&t MI ab&traction of Tbau under 71'" if

Tab· = {u: for all model& Mbau ofTbau1 7r(Mba·e) F u}

2.2 MI Abstractions with simplifying assumptions

While many common abstractions are MI abstractions, a large class of abstractions described in the literature are not. In particular, abstractions that admit false proofs are commonly used to speed up problem solving by guiding the search (e.g., [Ellman, 1993; Imielinski, 1987; Sacerdoti, 1974]). In this section we argue that such ab­ stractions can be, and are .best viewed as MI abstractions in conjunction with a set of &implifying auumption&.

Example 3 Consider Imielinski 's domain ab&traction& [1987]. Given a base theory and an equivalence relation over the set of constants of the base language, he con­ structs an abstract theory by replacing each occurrence of each constant in the base theory by a representative of the constant's equivalence class. This is not, in gen­ eral, an MI abstraction of the base theory. For exam­ ple, let {P(a, b), --,P(c, d)} be the base theory, and let a and c be equivalent (with representative a) and b and d be equivalent (with representative b). Hence, the do­ main abstraction of this theory is the inconsistent theory {P(a, b), --,P(a, b)}. Since the base theory is consistent, Proposition 1 is violated, and hence it can't be an MI abstraction. However, suppose that the equivalence rela­ tion was a congruence, i.e., for every n-ary relation P and terms t,, t~, 1 ~ i ~ n, such that t, and t~ are equivalent, the base theory entails P(t1, ... , tn) ¢:> P(ti, ... , t~). In this case, one can see that the domain abstraction is, in­ deed, an MI abstraction. To put it another way, domain abstractions a~e MI abstractions under the simplifying assumption that the equivalence relation is a congruence. If the domain abstraction admits false proofs (as in the above case where the abstraction was inconsistent), it is precisely because the simplifying assumption is violated: the equivalence relation is not a congruence. D

A number of other commonly used abstractions can be viewed in this fashion. As mentioned earlier, the sim~:,>li­ fying assumption made in ABSTRIPS [Sacerdoti, 1974j is that the literal dropped from preconditions of actions can always be achieved without affecting the truth value of literals with higher criticality. Davis's work on diagnosis uses an abstract theory that is an MI abstraction of the base theory under the simplifyin~ assumption that there are no bridge fault& [Davis, 1984j. The heuristic under­ lying the use of Connection graph& in [Chang, 1979] is to use an MI abstraction of the base theory, under the simplifying assumption that different literals in a clause share no common variables, e.g., a clause P(:z:) V Q(:z:) is revised to the stronger clause P(y) V Q(z). An MI abstraction of the revised theory is constructed using a ground abstraction that preserves all possible unifica­ tions.

In the above examples, the simplifying assumption is added to the base theory by simply adding in addi­ tional axioms. However, there are common situations in which the simplifying assumption is incon8i8tent with the base theory, so that merely adding in the simplify­ ing assumption makes the theory inconsistent. In such cases, adding a simplifying assumption to a base theory is better viewed as a belief revi8ion operation: the base theory is revised to make sure that the simplifying as­ sumption holds, while ensuring that the revised theory is consistent. The revised theory is then abstracted.

Example 4 Most approximations in engineering in­ volve simplifying assumptions that contradict the base theory. For example, consider two railroad cars con­ nected by a linkage. Say that the base theory describing the linkage models it as a spring with a very large spring constant (i.e., as a very stiff spring). It is common to assume that such linkages are rigid, i.e., the spring con­ stant is infinite. Clearly, the simplifying assumption that the spring constant is infinite is inconsistent with the base theory; the base theory must be revised by retract­ ing the axiom specifying the large spring constant of the linkage, and then adding in the simplifying assumption. The revised theory can now be abstracted by combining the two railroad cars into a single, composite rigid body. The fitting appro:z:imation8 in [Weld, 1992] are all of this form. 0

Viewing abstractions as a combination of a set of simplifying assumptions and an MI abstraction has two key advantages. First, the simplifying assumptions un­ derlying the abstraction are made ezplicit, and there­ fore can be used in reasoning, as has been done in compositional modeling [Falkenhainer and Forbus, 1991; Iwasaki and Levy, 1994] and diagnosis [Davis, 1984; Nayak, 1994b; Struss, 1992]. Second, we can show that an abstraction will yield false proofs only if the simpli­ fying assumptions are inappropriate. In particular, a simple corollary of Proposition 1 is that if an abstrac­ tion of a consistent base theory is inconsistent then it is because the simplifying assumptions are inconsistent with the base theory. This enables us to evaluate the utility of an abstraction depending on the reliability of the simplifying assumption.

3 Abstracting first-order theories

The semantic account of abstractions developed thus far applies to arbitrary languages with a declarative seman­ tics, and to arbitrary model level abstraction mappings 1r. In this section we restrict our attention to first­ order languages, and show how abstraction mappings can be specified using interpretation mapping8 [Ender­ ton, 1972]. We use this development to precisely charac­ terize the strongest MI abstraction of a base theory. We show that if the base theory is axiomatizable, then the strongest MI abstraction is also axiomatizable, though not always finitely axiomatizable.

3.1 Interpretation mappings

Let Tbcue be a base theory in language Lba··· and let Lab· be an abstract language. A first-order interpreta­ tion consists of a universe of discourse and denotations of the object, function, and relation constants within this universe. Hence, specifying the abstraction mapping 7r amounts to specifying how the abstract universe and de­ notations for the abstract object, function, and relation constants are constructed using a base model. This is done using interpretation mappings. A key notion used in specifying interpretation mappings is the relation de­ fined by a well-formed formula ( wff) in an interpretation.

Definition 3 (Defined relation) Let if> be a wff in language L with n free variable8 v1, v2, ... , vn, and let I be an interpretation of L . The n-ary relation defined by if> in I i8:

i.e., the tuple (a1, a2, ... , a..} i8 in the defined relation iff I i8 a model of if> with a variable auignment that auign8 eli to v, , 1 ~ i ~ n.

The above notion is used in specifying interpretation mappings by finding appropriate formulas in Lbau that define, in a base model, the abstract universe, and de­ notations for the abstract object, function, and relation constants. More formally, an interpretation mapping 7r that maps a model Mbau of Tba·· to an interpretation 7r(Mbau) of Lab· consists of the following (if if> has free variables v1, ... , Vn, and :z:1, ... , :Z:n are any variables, we denote by if>(:z:l> ... , :z:n) the result of replacing all free occurrences of v, by :z:,, 1 ~ i ~ n, in if>) :

1. a wff 7r"V with one free variable, v 1 , that defines the abstract universe. The idea is that, given any model, Mbau, of Tbau 1 7rv defines the universe of 7r(Mbau) to be the set defined by 7rv in Mba···
2. for each n-ary relation R in Lab" a wff 7l'R with n free variables, v1 , ... , Vn, that defines R. The idea is that, given a model Mbau of Tba··· 7l'R defines an n-ary relation in Mba··. The denotation of R in 7r( Mba .e) is this relation restricted to the universe of 7r(Mba·e)·

In addition, similar wffs are used to specify the deno­ tations of abstract object and function constants (see [Enderton, 1972] for details).

Example 5 Consider Example 1 again. The abstrac­ tion mapping 71' preserves the universe of discourse. Hence, 7r"V is the wff ( v1 = vt), which is satis­ fied by all elements. The extension of the predi­ cate ForeignCar is the union of the extensions of Japane8eCar and EuropeanCar. Hence 7rFOf'eignCar is the wff Japane8eCar(v1) V EuropeanCar(vt). The ex­ tension of the other predicates (except JapaneseCar and EuropeanCar, which are not in the abstract language) is unchanged. Hence, 7l'Car is just the wff Car(v1), etc.

0

3.2 Strongest MI abstraction

Given the above specification of abstraction mappings as interpretation mappings, we now give a precise char­ acterization of the strongest MI abstraction of a base theory (defined in Definition 2). The characterization of this theory is based on a natural mapping f.,. that maps an arbitrary wff ifJ in La.b· to a wff f,.(ifJ) in Lba.·e· 2 In­ tuitively, in a sense to be made precise, f,.(ifJ) says the same thing as ifJ.

For any wff ifJ in La.b" f,.(ifJ) is defined recursively as follows. If ifJ is an atom P(:JJ11 ··· , :JJ,.) that con­ tains no function or constant symbols, then f,.(ifJ) is 7l'p(:JJ1 , ... , :JJ,.). When ifJ contains object or function constants, the translation is more complex and we refer the reader to [Enderton, 1972] for details. Non-atomic sentences are mapped in the natural way: f,.(-.ifJ) = -.f,.(ifJ), f,.(ifJ 1\ 1/J) = f,.(ifJ) 1\ f,.('I/J). Finally, f,.(V:JJljJ) = 'Vx7l'~;~(:JJ) => f,.(ifJ), i.e., the translation of quantifiers is restricted to just the elements that satisfy 11'1;1.

Example 6 Continuing Example 5, the translation of the abstract sentence 'r/:JJForeignCar(:JJ) is 'V:JJ(:JJ = :JJ) => (JapaneseCar(:JJ) V EuropeanCar(:JJ)). 0

The following lemma, taken from [Enderton, 1972], is the key property of f.,.. It formalizes the sense in which ifJ and f,. ( ifJ) say the same thing:

Lemma 1 Let Mba.u be any model of Tba.u and a be a sentence in La.b·. Then

i.e., Mba. 1 e is a model of f,.(a) if and only if11'(Mba.u) is a model of a.

The above lemma associates with every sentence cr in La.b· an equivalent sentence f,.(a) in Lba.u· However, not every sentence in Lba.u has an equivalent sentence in La.b·. This is not surprising since, intuitively, La.b· is a more abstract language and there is no reason to believe that every base level sentence in Lba.u has an equivalent sentence in La.b·.

Theorem 1 Let Ta.b· be the strongest MI abstraction of a base theory Tba.1 e 1 with respect to 11' 1 and let T' be a theory in La.b· such that

0

1 Note that while the model mapping 71' goes from the base theory to the abstract theory, the sentence mapping f.,. goes the other way.

Tenenberg's construction of the abstract theory for predicate abstractions is a special case of the above con­ struction. An immediate corollary of the above theorem is that if Tba.u is axiomatizable, so is its strongest MI abstraction: 3

Corollary 1 Let Ta.b· be the strongest MI abstraction of Tba.u. If Tba.·e is axiomatizable, then so is Ta.b·.

Proof: A theory is axiomatizable iff it is effectively enu­ merable [Enderton, 1972]. Since Tba.·e is axiomatizable, we can enumerate the theorems of Tba.·e· Whenever we encounter a theorem of the form f,.(a), where a is a sen­ tence of La.b·, we add a as a theorem of Ta.b·. Theorem 1 ensures that this will enumerate all the theorems of Ta.b·, and hence Ta.b· is axiomatizable. 0

This corollary raises the following natural question. If Tba.·e is finitely axiomatizable, i.e., Tba.·e is the deductive closure of a finite knowledge base, is Ta.b· also finitely axiomatizable?

Theorem 2 There exist finitely axiomatizable Tba.u such that its strongest MI abstraction is not finitely ax­ iomatizable.

Proof sketch: The proof is based on showing that while the theory of the structure (N, 0, S, <, > ), where N is the set of natural numbers, 0, <, and > have their ordi­ nary meaning, and S is the successor function, is finitely axiomatizable, the theory resulting from the predicate abstraction of< and >, i.e., f., is not. 0

Note that, in particular, the counterexample in the proof disproves Tenenberg's conjecture that the pred­ icate abstraction of a finitely axiomatizable theory is finitely axiomatizable. A major consequence of Theo­ rem 2 is that, in practice, it is not always possible to construct the strongest MI abstraction, since its axiom­ atization may be infinite. Hence, we must often settle for axiomatizations that yield weaker MI abstractions.

4 Automatically constructing abstractions

While model-level mappings and simplifying assump­ tions are usually very natural and easy to specify, it is not always easy to construct the abstract theories that best implement them. In this section we describe a pro­ cedure that automatically creates the strongest MI ab­ straction for a given model-level mapping. This proce­ dure can be complemented with techniques from [Eiter and Gottlob, 1992] when incorporating the simplifying assumptions requires belief revision. We consider the case where La.b· results from adding a set of new predi­ cates and dropping some old predicates from Lba.·e· i.e., the object and function constants are unchanged. This covers various common model level abstractions includ­ ing dropping predicate arguments, taking the union or intersection of a set of predicates, and selecting a subset of a predicate's extension. For simplicity, we also as­ sume that the abstract language does not include equal­ ity. This procedure is meant for off-line construction of abstractions that are later used at run-time.

3 A theory T is axiomatizable iff there is a, possibly infi­ nite, decidable set :E whose deductive closure is T.

Assume that the base theory, Tba·e· is specified as a set of clauses. Let the new predicates in Lab· be de­ fined by the clauses in the set N: if P is a new n-ary predicate, N contains the clauses resulting from the sen­ tence 'v'v1, ... , VnP(vl, ... , vn) ¢:} 1rp(v1. ... , vn)· Let 'P be the set of predicates of Lbau that are dropped in Lab·. Figure 1 shows the procedure to construct the resulting strongest MI abstraction. The idea is to first add in the clauses in N to Tbaoe, and then to use any refutation complete resolution strategy, e.g., linear resolution, to generate clauses. Only resolutions on the predicates in 'P are considered. A generated clause that contains none of the predicates in 'P is added to Tab·. The following theorem tells us that this procedure is correct:

Theorem 3 Procedure Construct-abstraction con­ structs the strongest MI abstraction of Tbau.

Proof sketch: Since the clauses in Tab· are a conse­ quence of nau u N, it is easy to show that Tab· is an MI abstraction of Tbaoe· To show that it is the strongest MI-abstraction of Tba·e· we define the class of Herbrand­ like models, and show that every Herbrand-like model of Tab· is an image of a model of na·e· Then, we show that every model of Tab· is elementarily equivalent to a Herbrand-like model. (Two models are elementarily equivalent iff the same set of first-order sentences are true in both of them.) D

Clearly, procedure Construct-abstraction will not terminate if an infinite number of resolutions are possi­ ble, leading to an infinite Tab·. In such cases, the pro­ cedure can be terminated at any time to yield a weaker MI abstraction.

Example 7 Consider constructing the strongest MI ab­ straction of the axioms in (1) and (3). The axiom defin­ ing ForeignCar is

ForeignCar(:c) ¢:} Japane8eCar(:c) V EuropeanCar(:c)

Adding this axiom to (1) and (3) and resolving on predi­ cates Japane8eCar and EuropeanCar yields the axioms in (2) and (5). This is the strongest MI abstraction. D

We conclude this section with an application of the procedure in an analysis of ABSTRIPS. This analysis shows how the simplifying assumption and the model­ level mappings justify the commonly used syntactic map­ ping, implementing the abstraction.

Example 8 ABSTRIPS solves planning problems by first solving abstract problems using abstract opera­ tors, and then using the abstract solution to guide the search in the base level problem. Each predicate is assigned a criticality level. Operators are abstracted at level i by dropping preconditions whose criticality is less than i. We now discuss the precise seman­ tic steps involved in constructing this abstraction. We use Green's formulation of planning problems [Green, 1969): actions are represented by axioms of the form q1(8) 1\ ... 1\ qn(8) => r(do(A, 8)), where qi are literals representing preconditions and r the postcondition of op­ erator A, and do( A, 8) is the state resulting from execut­ ing A in state 8.

Let q1(8) 1\ q2(8) 1\ p(8) => r(do(A, 8)) be an opera­ tor, and suppose that the criticality of pis less than the current abstraction level. Intuitively, this means that p can be achieved in any state without affecting the truth values of predicates at a higher level of criticality. We formalize this simplifying assumption using the axiom

where ¢J denotes the frame axioms expressing the fact that the action a does not affect the truth value of any other predicate, e.g., q1(8) ¢:} q1(do(a, 8)).

Next, we add in this simplifying assumption to the base theory. One of the clauses resulting from the sim­ plifying assumption is p( do(!( 8 ), 8) ), where f is a skolem function. Note that, because of the frame axioms, the only possible difference between a state 8 and a state do(/(8), 8) is in the truth value of p.

Now we use procedure Construct-abstraction to drop the predicate p, by resolving on p in all possible ways. For example, resolving the simplifying assump­ tion with the above operator leads to the operator

Since now the language does not contain the predicate p, it follows that the same set of facts are true at the states 8 and do(/(8), 8), i.e., they are congruent. Hence, the simplifying assumption underlying a domain abstrac­ tion which makes 8 and do(/(8), 8) equivalent is satis­ fied (see Example 3). Hence, we can replace all oc­ currences of do(/(8), 8) with 8 resulting in the axiom q1(8) 1\ q2(8) => r(do(A, 8)). This is exactly the abstract operator used by ABSTRIPS. D

5 Discussion

Giunchiglia and Walsh [1992) characterize abstractions as syntactic mappings between theories. While it is true that ultimately abstractions are syntactic mappings be­ tween theories, they are an overgeneral characterization of abstractions. Hence, this view of abstractions pro­ vides little constraint on what abstractions actually are. On the other hand, our theory provides a more meaning­ ful characterization of abstractions. It captures the fact that an abstraction is a model level mapping of the origi­ nal theory in conjunction with a simplifying assumption. This difference is made clearer by the following compar­ ison of TD abstractions to MI abstractions.

Since for every theorem u of an MI abstraction, f'JI'(u) is in the base theory, all MI abstractions are TD ab­ stractions. However, MI abstractions are a strict subset of TD abstractions. To see this, consider a base lan­ guage with propositions p and q, and an abstract lan­ guage with proposition r. Consider a syntactic mapping that maps p tor and q to ·r, the base theories B1 = {p} and B2 = {q}, and the abstract theories A1 = {r} and A2 = { ·r }. Clearly, A1 and A2 are TD abstractions of B1 and B2 , respectively. However, A1 U A2 is inconsis­ tent, while B1 U B2 is not. Hence, it follows that this TD abstraction is not compositional, and hence not an Ml abstraction.

It is worth noting that the strongest MI abstraction of Tb .. ,. is not, in general, a TC abstraction. It is TC abstraction only if there is also an abstraction mapping p in the opposite direction, e.g., the mappings between polar coordinates and rectilinear coordinates. In this latter case, the base and abstract theories are equivalent, and there is really no model level abstraction going on. However, a switch from one theory to another may still be motivated by computational considerations.

Levy [1994] has outlined another method for con­ structing MI abstractions. His method is based on iden­ tifying sentences in Tba·e that are independent of the abstraction, and hence can be syntactically abstracted. Intuitively, sentences of the form f'JI' ( u), or sentences that entail sentences of the form f'JI'(u), are independent, and such sentences can be abstracted to u. Identifying inde­ pendent sentences can often be done easily, resulting in an efficient algorithm for constructing abstract theories.

Our theory of abstractions raises several directions for future work. First, it raises the question of finding re­ stricted, but useful, settings within which the strongest MI abstraction is finitely axiomatizable and can be con­ structed efficiently. When the strongest MI abstrac­ tion cannot be constructed efficiently, an important is­ sue is finding methods for constructing weaker, though still useful, MI abstractions. Second, our theory of ab­ stractions is only a logical account of the process, and does not address the issue of the computational benefits of using abstractions. A better understanding of when model level abstractions lead to computational savings is needed. Third, we are developing probabilistic methods for reasoning about how likely it is that a simplifying assumption holds.