Preserving Consistency Across Abstraction Mappings

1 Introduction

An important method of constraining search in combinatorially intractable problems is to map the representation of the problem into an abstract representation, solve the problem in the abstract search space and use the abstract solution to guide the search in the original problem space. Work of this nature has been pursued by many researchers, most notably [Amarel1972, Hobbs 1985, Korf 1985, Plaisted 1981, Sacerdoti 1974]. Of importance in this work is that certain formal properties hold between the original and the abstract versions of the problem in order to justify the use of abstraction. In this paper we will define a syntactic abstraction mapping between two first-order theories that involves the renaming of predicate symbols, a subclass of those mappings first defined in [Plaisted 1981]. The mapping is demonstrated to have the following properties. First, the abstract thoery will be consistent if the original theory is; second, for each abstract theorem T', there exists a theorem T in the original theory for which T' is an abstraction; third, the model-theoretic semantics of the abstract theory is intuitively appealing.

In section 2 we present the formal definition of a predicate mapping, and show in section 3 both its

This work was supported by the Air Force Systems Command, Rome Air Development Center, Griffiss Air Force Base, New York 13441-5700, and the Air Force Office of Scientific Research, Bolling AFB, DC 20332 under Contract Number F30602-85-C-0008 which supports the Northeast Artificial Intelligence Consortium (NAIC).

The author would like to thank the Xerox Corporation University Grants Program for providing equipment used in the preparation of this paper.

Preserving Consistency across Abstraction Mappings

Josh D. Tenenberg

Computer Science Department University of Rochester Rochester NY 14627

relation to Plaisted's abstraction mappings, and its inherent problem of generating inconsistencies at the abstract level. Section 4 provides a set of syntactic restrictions that satisfies a particular semantics, and Section 5 demonstrates that these restrictions overcome the inconsistency problem by showing constructively that a model exists for the abstract theory given a model of the original theory. Section 6 will consist of a small example, and section 7 finishes with concluding remarks.

2 Predicate Mappings

We will assume standard first-order logic terminology as in [Enderton 1972]. In addition, all wffs will be taken to be in clause form [Robinson 1965]. Recall that a clause is a set ofliterals, and that clause C subsumes clause D if there exists a substitution 4> such that Cct> is a subset of D. In addition, C and Dare variants ifC and D are instances of one another; that is, they are identical except for a renaming of variables.

Predicate mappings are functions that map predicate symbols from one first order language to those of another. Given two sets of predicates P1, P2, f: P1-+ P2,

where the Pi are the only symbols that possibly distinguish the first order languages L1 and L2. What is noteworthy about fis that it is not necessarily 1-1, and therefore more than one relation symbol from L1 can map to the same relation symbol from L2. We can then define f over literals such that literals in L1 are mapped to literals in L2 by replacing the predicate symbols under f. Likewise, f can be extended to clauses and sets of clauses in precisely this way.

3 Plaisted's Abstraction Mappings

Predicate mappings are a subclass of abstraction mappings that are defined in [Plaisted 1981]:

DEFINITION. An abstraction is an association of a set f(C) of clauses with each clause C such that fhas the following properties:

1. If clause C3 is a resolventofCl and C2 and D3 E f(C3), then there exist Dl E f(Cl) and D2 E f(C2) such that some resolvent ofDl and D2 subsumes D3.
2. f(NIL) ={NIL}. (NIL is the empty clause.)
3. IfCl subsumes C2, then for every abstraction D2 ofC2 there is an abstraction Dl ofCl such that Dl subsumes D2.

Iff is a mapping with these properties, then we call fan abstraction mapping of clauses.

In addition, Plaisted proves the following theorem:

THEOREM. Suppose 4> is a mapping from literals to literals. Let us extend 4> to a mapping from clauses to clauses by tl>(C) = {4>(1): L E C}. Suppose 4> satisfies the following two properties:

1. 4>( ...,L) = ...,(tl>(L)). That is, 4> preserves complements.
2. IfC and Dare clauses and Dis an instance ofC, then tl>(D) is an intance of tl>(C). That is, 4> preserves instances.

Then 4> is an abstraction mapping.

By this theorem, predicate mappings are abstraction mappings since they preserve both complement and instance.

Abstraction mappings have the property that from every clause C derivable from a set of clauses S, there exists a clause C' derivable from f{S) that subsumes an abstraction ofC (proven in [Plaisted 1981]). Informally, we m1ght say that every solution in the original problem space has a corresponding solution in the abstract space. This will be termed the upward­ solution property.

A problem with abstraction mappings, however, (and hence with predicate mappings) 1s that they may result in abstract theories which are inconsistent even though the original theory is consistent, which Plaisted termed the "false proor· problem. As an example, suppose we have a clause set for a simple domain in which we have objects that are bottles and glasses, with clauses stating that they are disjoint (note that all clauses will be in implication form for ease of interpretation):

1. Bottle(x) ::J ...,Glass(x),
2. Glass(x) ::J ...,Bottle(x),
3. and the clause stating that object A is a bottle:
4. Bottle(A). If our predicate mapping fmaps both Bottle and Glass to a new predicate Container in the abstract theory, then from the abstract theory we can derive a contradiction:

Container(x) ::J ...,Container(x) I- ...,Container(A) Container(A)

The approach taken in the remainder of the paper is to restrict the original set of clauses over which the predicate mapping can be applied so as to preserve consistency.

4 Restricted Predicate Mappings

The intuition behind the semantics of restricted predicate mappings is that we would like the interpretation of a predicate in the abstract theory to be the union of the mterpretations of each of the predicates in the original theory that map to it. So the objects that are Containers are all of those objects that are either Bottles or Glasses, or any of the other things that map to Container.

We can obtain this interpretation syntactically by removing all of those axioms from the original theory that serve to distinguish the relations that are conflated at the abstract level. Relations Rt. ... , Rn in axiomatization 81, can be made indistinguishable in axiomatization 82 by systematically replacing each Ri with a new symbol R' under some predicate mapping f as before, but including in 82 only those clauses HC) such that Cis in 81 and every clause mapping to Cis derivable from 81. So, for instance, if we wish to conflate the relations Glass and Bottle by mapping them to the same symbol, say Container, then given the axioms Glass(x) ::J Breakable(x)

Bottle(x) ::J Breakable(x)

Bottle(x) ::J Corkable(x)

• we would have in the new clause set only Container(x) ::J Breakable(x),

since Corkability is true only of Bottles, and therefore distinguishes Bottles from Glasses in the original theory, while Breakability is true ofboth Bottles and Glasses. In other words, the clause

Container(x) ::J Corkable(x) would not be placed in the new clause set since one of the clauses that maps to it, namely

Glass(x) ::J Corkable(x)

is not derivable from the original clause set.

This constraint, however, is stronger than required. For instance, it keeps one from ever asserting in the abstract theory that an object is a container in theories in which bottles and glasses are disjoint, as in (1)- (3) above, since it will never be the case that an object in the original theory is both a bottle and a glass. Given the desired semantics, it is permissible to allow the inclusion ofmappedpositive clauses from the original theory, those clauses containing no negated literals, into the abstract theory. That is, if object A has property P, then certainly object A will have the abstract property f{P), and likewise for predicates of any arity. Thus, one can map the clause Bottle(A) to Container(A), since all bottles are containers, even though Glass(A) may not hold. In addition, this allows the mapping of clauses such as Bottle(A) V Glass(A) to Container(A) V Container(A).

5 Formal Definitions and Proof of Consistency

We use [C]rto denote the set of symbols or clauses that map into C under predicate mapping f. That is, [CJr= {D I f{D) = C}.

Each such D will be called a specialization of C. Ife is a clause set and D is a clause then we will use e 1-- D to mean that the null clause can be derived from the clause set 8 u ·D by the inference rule full resolution [Robinson 1965]. Let 8 be an axiomatization in clause form of a theory over language Lt and let f be a predicate mapping from Lt to L2. We define g(8), a restricted predicate mapping, to be a subset off{8), where

1. g(8) = {C I there exists some DE[C]rsuch that DES and either Cis a positive clause or for every DE[C]rit is the case that 81--D}.

The main theorem states that given a clause form axiomatization e and a restricted predicate mapping g, g(8) is consistent if e is. In other words, consistency is preserved by the mappin~. Given that a first-order clause set e is consistent 1f and only if it is satisfiable, i.e., there exists a model that assigns truth to all of the clauses D such that e t- D, this theorem will be proven by constructing a model of g(8) from a model of e.

Standard formal semantic terminology will be assumed [Enderton 1972]. In particular, an interpretation is a structure < D, G >,where Dis a set of objects, the domain, and G is an interpretation function that assigns to each constant symbol an object from D, to each n-function symbol an n-function mapping objects in D to an object in D, and to each n-predicate symbol ann-relation over objects in D. Further, we say that y is a value assignment if it assigns to every variable symbol an object in D. If a is a symbol from the language over which G is defined, we say that G(a) is the interpretation of a under M, which in the case of an n-predicate will be a set of n-tuples. In addition, clauses are assigned truth values according to semantic rules pertaining to the logical symbols, which in the case of clause form is universal quantification, negation, and disjunction. If a is a clause andy is a value assignment, then M(a) returns either True or False under y, denoted by My( a). If My( a) =True for every value assignment y, then we say that a is True in M, or M(a) =True, otherwise a is False in M. An interpretation M = < D, G > is a model of a clause set 8 ifD is True in M for every clause D such that 8 f- D.

Theorem:

Let 8 be an axiomatization in clause form of a theory over language Lt,let fbe a predicate mapping from Lt to L2, and let g be the restricted predicate mapping defined relative to f as in ( 4) above. For any model M= <D, G> of8, M'= <D, G'> isamodelofg(8) where for every predicate symbol a ofL2,

and for every non-predicate symbol a, G'(a) =G(a). Proof:

Let us assume that M' is not a model of g(8). There must then be some clause C E g(8) that is False in M'. There are two cases to consider- first where C is a positive clause, and second where C contains negated literals.

Case 1: Assume Cis a positive clause. For membership ofC in g(8), it must be that there exists some c.lause E E [C]r such that E E 8, by the definition of g. Since M is a model of8, E is True in M. Then, for every value assignement y, My(E) =True. Let us take truth in M and M' relative to a particular value assignment y. E is of the form E ={Pt(at), ... , Pn(an)}. where &i represents the predicate Pi'S list of arguments. My(E) =True means that My(Pi(&i)) =True for some literal of E. Since &i represents the terms (ail, ... , aij) of Pi. then <G(ail) , ... , G(aij)> E G(Pi). Additionally it follows that < G'(ail) , ... , G'(aij) > E G'(f(Pi)) under y. by the definitions of the inter~retation function G given in (5) above, and the predicate J11apping f. That is, for Q=f(Pi), M'y(Q(ail, ... , aij))=True. But this literal is inC, and so M'y(C) =True. Therefore, M'y(C) =True for every value assignment y since y was chosen arbitrarily, making M'( C) =True, contradicting our assumption. This dispatches the first case. ·

Case 2: Assume C contains negated literals. For membership of C in g(8), for every clause E E [C]r, 8 f- E and some E E 8, by the definition of g. Since M is a model of8, M(E) =True for every such E, and therefore My(E) =True for every value assignment y.

Since Cis False in M', there must exist a value assignment y such that M'y(C) =False. Let us take truth in M and M' relative to this value assignment y.

Cis of the form C ={Rt(at), ... , Rn(an) . ...,St(bt), ... ,..., Sk(hk)}, where ai and hi are the arguments of each of the literals. That is, some of the literals inC are negated, and some may be positive. For every literal L E C, M'y(L) =False. This means that for every E E [C]r, for every positive literal WEE, My(W)=False, since were it not, then M'y(g(W)) =True for some literal W and hence M'y(C) =True by the definition ofG', contradicting our assumption that M'y(C) =False. Therefore, under this value assignment one or more of the negated literals in each E E [C]rmust be True.

Since each ...,Si(bi) is False in M' under y, then each Si(bi) is True. That is, taking hi to represent the ground terms (bit ·... , bi,U of each ..., Si. < G'(bil) , ... , G'(bijJ > E U'(Si) for each of the negated literals under y. Hut by the definition ofG', for each of the Si'S there exists some Qi E [Silrwhere <G(bH) , ... , G(bij) > E G(Qi) under this same value assi~ment. That is, My(..., Qi(bi)) =False for some specialization Qi of each predicate Si of each negated hteral in C. Let E be the clause consisting of the negation of each such Qi(bi) and some specialization of each of the positiv~ literals in C. Note thatE E [CJr. My(E)=False, since each of the literals in E are False. This then contradicts the earlier conclusion that every E E [CJr be assigned True by M for every value assignment y. This dispatches case 2, and hence establishes the theorem. QED

Restricted predicate mappin~ are no longer abstraction mappings by Plaisted's definition, since the upward-solution property is not preserved. However, abandoning the completeness afforded by the upward­ solution property is likely what is required to solve frequently encountered problems at a lower cost than if they were solved directly in the original theory. These restricted mappings do have what can be termed the downward-solution property, since a trivial corollary of the theorem is that for every clause derivable from the abstract theory, there will be a specialization of it derivable from the original theory. Note that there may be no solution to the problem in the abstract theory since its solution requires some of the details that are ignored at that level. However, every abstract solution is guaranteed to have a specialized solution to the original problem.

An important objection that one might have is that the syntactic mapping function g given in (4) is undecidable, since it is based upon determining 8 f- D for every clause D mapping to each candidate clause in the abstract clause set. One should note, however, that the search for derivability can always be arbitrarily bounded, and if no proof is obtained within this bound then it can be assumed that this clause is not derivable. In this way, consistency is still preserved between the original and the abstract theory, the abstract theory being simply weaker than it theoretically could be, i.e., having fewer theorems. The appropriate amount of resource that one should expend in constructing abstract theories is quite an important issue but outside the bounds of this paper. These kinds of Eerformance choices, however, are discussed in [Hartman and Tenenberg 1987], elsewhere in this volume.

6 Example

Let 8, the original clause set, be the following clauses (note that A:::> B is equivalent to ..,A v B, and is therefore not a positive clause):

Let f1 map each predicate symbol to itself except that it maps Bottle and Glass both to GlassContainer. Therefore, g1(8) is the following:

• 1') GlassContainer(x) :J MadeOfGiass(x)
• 2') GlassContainer(x) :J Graspable(x)
• 6') Box(x) :J Graspable(x)
• 9') GlassContainer(x) :J ~Box(x)
• 11') Box(x) :J ~�iassContainer(x)
• 14') Open(x) 1\ Graspable(x) :J Pourable(x)
• 15') Graspable(x) :J Movable(x)
• 16') MadeOfGiass(x) :J Breakable(x)
• 17') GlassContainer(x) v Box(x)
• 18') Open(A)

Note that clauses 3 and 4 are redundant in the abstract theory and are therefore not included in g1(8), as are 10 and 12. Clause 5 gets eliminated because Bottle(x) :::> Open(x) is not derivable from 8. Likewise with 7 and 8 as seen earler. Additionally, 17' was factored so that the same literal did not appear twice. Although g1(8) is much smaller than 8, there are still several intuitive inferences that can be made, such as Graspable( x), Movable( x) and Pourable( A).

Given the way in which abstraction is defined, g1(8) can additionally be treated as a primitive level theory and mapped into a more abstract theory g2(g1 (8)). For instance, let {2 map all predicates to themselves except Box and GlassContainer get mapped to Container. Thus, g2(g1(8)) is:

• 2") Container(x) :J Graspable(x)
• 14") Open(x) 1\ Graspable(x) :J Pourable(x)
• 15") Graspable(x) :J Movable(x)

16") MadeOfGiass(x) :J Breakable(x)

17") Container(x)

18") Open(A)

One can therefore abstract a theory arbitrarily many times, preserving consistency throughout. Each abstract theory has the advantage that those clauses that it can derive will likely be done so at considerably less cost than in the original theory. Although this would be true of any subset of 8, it is important to reco~ize that the mapping functions embed a significant amount of heuristic information about the domain. This function determines which clauses are important, and which are mere details, and so the choice about which clauses remain in the abstract theory is not done so on an arbitrary basis.

7 Conclusion

A useful way of viewing abstraction is as a function that maps one first-order theory into another. We have defined predicate mappings that involve the renaming of predicate symbols, where more than one of the original symbols can map into the same abstract symbol. These predicate mappings are a subclass of Plaisted's abstraction mappings, and as such suffer from the fact that consistency in the original theory may be lost in the abstract theory. To remedy this, we introduced syntactic restrictions to the predicate mapping that guarantee the preservation of consistency. These restrictions amount to eliminating the axioms in the original theory that distinguish the predicates which are being conflated in the abstract theory. This has a simple semantics; the extension of each of the predicates P in a model of the abstract theory can be constructed from the union of the extensions of each of the predicates that map toP in any model of the original theory. A proof of this was provided, along with an example demonstrating one possible use of the restricted predicate mappings.

Acknowledgements

I would like to thank my advisor, Dana Ballard, for his encouragement and wealth of ideas on abstraction. In addition, I would like to thank members of the UR-Al group, especially Leo Hartman, who always seems a step ah~ad, sometimes two, and Jay Weber, for pushing for a semantic definition. I am also grateful to Mark Fulk, for finding the problems with the old versions of the main proof, and pointing the way to the correct version.