9512.net
甜梦文库
当前位置:首页 >> >>

David A. Basin Max-Planck-Institut fur Informatik


Difference Unification*
David A. Basin M a x - P l a n c k - I n s t i t u t fur I n f o r m a t i k Im Stadtwald, Saarbriicken, Germany (basin@mpi-sb.mpg.de)

Toby Walsh
Dept. of A I , University of Edinburgh, 80 S. Bridge, Edinburgh, Scotland (tw@aisb.ed.ac.uk)

Abstract
We extend work on difference identification and reduction as a technique for automated reasoning. We generalise unification so that terms are made equal not only by finding substitutions for variables but also by hiding term structure. This annotation of structural differences serves to direct rippling, a kind of rewriting designed to remove differences in a controlled way. On the technical side, we give a rule-based algor i t h m for difference unification, and analyze its correctness, completeness, and complexity. On the practical side, we present a novel search strategy for efficiently applying these rules. Finally, we show how this algorithm can be used in new ways to direct rippling and how it can play an important role in theorem proving and other kinds of automated reasoning.

ence identification and reduction as a means of reordering a potentially infinite search space. Here we report on research sharing both these cognitive and pragmatic aims. We have developed a general procedure called difference unification for identifying differences between two terms. Difference unification extends unification in that it decides if terms are syntactically equal not only by giving assignments for variables but also by computing what incompatible term structure must be removed. This incompatible term structure, called wave-fronts, is marked by annotations which are used to direct a special kind of rewriting called rippling; rippling seeks to reduce the differences between the terms by moving the wave-fronts "out of the way" while not disturbing the unannotated parts of the terms Related Work This research is the outgrowth of previous work at Edinburgh in inductive theorem proving. There Bundy [Bun88; BS+92] suggested that in proofs by mathematical induction, the induction conclusion could be proven from the induction hypothesis by rippling on the induction conclusion. Rippling has been employed in the O Y S T E R / C L A M prover. A similar kind of rewriting was developed independently by Hutter [Hut90], from ideas in [Bun88], and employed in the I N K A system. Both systems have enjoyed a high degree of success stemming from several desirable properties of rippling. These include (see [BS+92]) that rippling involves very little search and rippling always terminates since wave-fronts are only moved in some desired (well-founded) way — usually to the top of the term. Research C o n t r i b u t i o n s Motivated by a desire to apply rippling outside of inductive theorem proving, in BW92 we introduced difference matching which extends matching to annotate the matched term so it can be rewritten using rippling. We list there, as well as in [WNB92] several applications of this idea. In this report we take another step forward. Our contributions are several fold. First we extend difference matching to difference unification whereby substitutions and annotations are returned for both terms. The rule based algorithm we give uses conventional unification in a transparent way whereby other additions to unification, such as equations or higher order patterns,

1

Introduction

Motivation and Context Heuristics for judging similarity between terms and subsequently reducing differences have been applied to automated deduction since the 1950s when Newell, Shaw, and Simon built their "logic machine" [NSS63] for a propositional calculus. Their intent was to simulate the behavior of a human on the same task. More recently, in resolution theorem proving, a similar theme of difference identification and reduction appears in [BS88; Dig85; Mor69]. In this work a partial unification results in a special kind of resolution step (E or RUE-resolution) where the failure to unify completely produces new inequalities that represent the differences between the two terms. This leads to a controlled application of equality reasoning where paramodulation is used only when needed. The intention was not to design a human oriented problem solving strategy, but rather, to use differ*This research was partially funded by the German Ministry for Research and Technology (BMFT) under grant ITS 9102 and a SERC postdoctoral fellowship. The responsibility for the contents of this publication lies with the authors. We thank the Edinburgh Mathematical Reasoning Group for their encouragement and criticism, in particular Alan Bundy and Andrew Ireland.

116

Automated Reasoning

can be easily m a d e . We prove the a l g o r i t h m given is b o t h s o u n d a n d c o m p l e t e w i t h respect t o i t s specificat i o n . Second, u n l i k e difference m a t c h i n g , difference u n i fication can r e t u r n a large n u m b e r of matches w h i c h we are n o t interested i n ; there m a y b e e x p o n e n t i a l l y m a n y ways t o a n n o t a t e t w o i d e n t i c a l t e r m s . Hence, w e dem a r c a t e t w o r e s t r i c t e d classes of useful answers ( w h i c h we call strongly a n d weakly m i n i m a l ) . F u r t h e r , we give a novel search s t r a t e g y (a m e t a - i n t e r p r e t e r ) t h a t finds answers i n these classes w i t h m i n i m a l search. T h i r d , we give a t h o r o u g h analysis of t h e c o m p l e x i t y of difference u n i f i c a t i o n a n d s u b p r o b l e m s . F i n a l l y , w e p r o v i d e examples of h o w difference u n i f i c a t i o n can be used. In d o i n g so, we present a new p a r a d i g m for t h e o r e m p r o v i n g / p r o b l e m s o l v i n g whereby p r o o f proceeds b y a l t e r n a t i n g between a n n o t a t i n g differences a n d r e d u c i n g t h e m . T h i s c o m b i n a t i o n i s different f r o m previous work c o m b i n i n g r i p p l i n g and difference m a t c h i n g since here successful r i p p l i n g does n o t guarantee successful r e w r i t i n g of one t e r m w i t h a n o t h e r ; r a t h e r , it m u s t be seen as one step, i n possibly m a n y , o f difference r e d u c t i o n . T h i s , a l o n g w i t h differences f r o m t r a d i t i o n a l r e w r i t e based t h e o r e m p r o v i n g , is developed in the n e x t section.

t h e o t h e r . However, t h i s fails w i t h difference u n i f i c a t i o n as b o t h t e r m s are a n n o t a t e d . For e x a m p l e , consider the associative ( i n f i x ) f u n c t i o n s y m b o l + . T h e f o l l o w i n g are w a v e - r u l e s ( c a p i t a l letters represent variables and lower case letters constants and b o u n d variables).

(1) (2)
A s p r e v i o u s l y n o t e d , r i p p l i n g t e r m i n a t e s because wavef r o n t s i n the r e w r i t e rules m u s t m a t c h those i n t h e r e w r i t ten t e r m a n d these are o n l y m o v e d i n some well-founded d i r e c t i o n . W e m a y therefore r e w r i t e w i t h the associativi t y o f + i n b o t h directions. Consider p r o v i n g

2
2.1

Applications
Normalization

If we difference u n i f y the left h a n d side of this equat i o n w i t h the r i g h t , there are 10 a n n o t a t e d answers corr e s p o n d i n g to t h e 6 ways of selecting any 2 constants f r o m the 2 t e r m s a n d 4 ways of selecting any one. In general, w e prefer o n l y those w i t h m i n i m a l a m o u n t s o f a n n o t a t i o n . F u r t h e r m o r e , as wave-rules o n l y exist to r i p ple these m i n i m a l a n n o t a t i o n s , r i p p l i n g w o u l d n o t f i n d proofs for the others. P i c k i n g m i n i m a l a n n o t a t i o n s (form a l l y defined in §3) n a r r o w s t h e choice to 2:

W e begin w i t h a s i m p l e e x a m p l e t h a t b o t h i n t r o d u c e s n o t a t i o n and i l l u s t r a t e s how difference u n i f i c a t i o n can be used to a p p l y r i p p l i n g in a new way: as an i t e r a t i v e difference r e d u c t i o n technique. I n r i p p l i n g ' s o r i g i n a l role i n i n d u c t i v e t h e o r e m p r o v i n g , successfully r i p p l i n g the goal always allows use of t h e i n d u c t i o n hypothesis. M o r e p a r t i c u l a r l y , i n a n i n d u c t i v e p r o o f the i n d u c t i o n conclusion is an i m a g e of t h e i n d u c t i o n hypotheses except for the appearance of certain f u n c t i o n s y m b o l s applied t o the i n d u c t i o n v a r i a b l e i n the conclusion. T h e rest of the i n d u c t i o n conclusion, w h i c h is an exact i m age of the i n d u c t i o n hypothesis, is called the skeleton. T h e f u n c t i o n s y m b o l s t h a t m u s t be m o v e d are the wavefronts. For e x a m p l e , i f w e w i s h t o prove p ( x ) for all n a t u r a l n u m b e r s , w e assume p ( n ) a n d a t t e m p t t o show p ( s ( n ) ) . T h e hypothesis a n d the conclusion are i d e n t i c a l except for the successor f u n c t i o n s(.) a p p l i e d to the i n duction variable n. We m a r k this wave-front by placing a box a r o u n d it a n d u n d e r l i n i n g t h e s u b t e r m contained i n the skeleton, R i p p l i n g t h e n applies j u s t

B o t h o f these w i l l lead t o proofs b y r i p p l i n g ( t h e f i r s t g i v i n g a left associative n o r m a l f o r m , t h e second g i v i n g a r i g h t ) . In w h a t f o l l o w s we concentrate on the first. T h e left h a n d side of t h i s e q u a t i o n is c o m p l e t e l y r i p p l e d - o u t : no m o r e wave-rules need (or can) be applied since the wave-fronts are already o u t e r m o s t . T h e r i g h t h a n d side ripples w i t h (2) y i e l d i n g

those r e w r i t e rules, called wave-rules, w h i c h m o v e the difference o u t o f the way l e a v i n g b e h i n d the skeleton. I n t h e i r s i m p l e s t f o r m , wave-rules are r e w r i t e rules o f t h e form B y design, t h e skeleton

a n d now b o t h t e r m s are r i p p l e d - o u t . T h o u g h r i p p l i n g is done, we have n o t succeeded in p r o v i n g the t e r m s equal since the wave-fronts themselves differ. One m i g h t conclude t h a t r i p p l i n g has n o t accomplished a n y t h i n g b u t t h a t w o u l d be false. It has reduced t h e " i n n e r difference" between these t e r m s : each now c o n t a i n a copy o f t h e previous skeleton a + b i n t a c t . Difference u n i f y i n g ( ( a + b) + c) + d against (a + b) + (c + d) reveals t h i s . T h e r e are 12 a n n o t a t i o n s in t o t a l , b u t o n l y 3 are m i n i m a l , a n d o n l y one of these can be r i p p l e d :

a { y ) remains unaltered by their application. If rippling succeeds t h e n the conclusion is r e w r i t t e n usi n g wave-rules i n t o some f u n c t i o n o f p ( n ) ; t h a t is, i n t o m a y b e t h e i d e n t i t y ) . A t t h i s p o i n t w e can call u p o n the i n d u c t i o n hypothesis. A n analogous s i t u a t i o n occurs i n difference m a t c h i n g . I f w e can m a t c h t w o t e r m s , a n n o t a t i n g one w i t h wavef r o n t s , t h e n successful r i p p l i n g allows r e w r i t i n g one t o We have m a d e progress since these t e r m s have a larger skeleton. As before t h e left h a n d side is r i p p l e d - o u t ; r i p p l i n g o n t h e r i g h t w i t h (2) yields the left h a n d side, s o we are done. T h i s e x a m p l e i l l u s t r a t e s a general phen o m e n o n : i t e r a t i n g difference u n i f i c a t i o n a n d r i p p l i n g successively decreases t h e difference between t w o t e r m s . T h i s c o m b i n a t i o n can be very effective. In associat i v e reasoning each i t e r a t i o n of difference u n i f i c a t i o n a n d

Basin and Walsh

117

r i p p l i n g increases t h e skeleton a n d hence t e r m i n a t e s successfully. Of course, exhaustive a p p l i c a t i o n of one of the associativity rules w o u l d also suffice, b u t there are a d vantages i n u s i n g difference u n i f i c a t i o n a n d r i p p l i n g . T o begin w i t h , one n e e d n ' t c o m p l e t e l y n o r m a l i z e t e r m s , r i p p l i n g proceeds o n l y as f a r as is required to reduce the difference. M o r e o v e r , as b o t h left a n d r i g h t a s s o c i a t i v i t y m a y be used, fewer r e w r i t e steps m a y be r e q u i r e d . M o r e s i g n i f i c a n t l y , t h e r e are theories where we need b o t h a n d where n o r m a l i z a t i o n w o u l d therefore l o o p . T h e c o m b i n a t i o n of difference u n i f i c a t i o n a n d r i p p l i n g is often an effective heuristic in theories where r e w r i t e based procedures d o n o t exist; t h e n e x t e x a m p l e , aside f r o m b e i n g m o r e general, i l l u s t r a t e t h i s . 2.2 Series

where C and D are constant w i t h respect to j. Note t h a t (6) c o u l d n o t be used in a procedure based on exh a u s t i v e r e w r i t i n g since, l i k e associativity w h e n used i n b o t h directions, it w o u l d loop. T h e s t a n d a r d f o r m m e t h o d f i r s t applies wave-rule (6) t o t h e goal d i v i d i n g its wave-front i n t o t w o ,

Difference u n i f i c a t i o n and r i p p l i n g have proved also very useful in s u m m i n g series. Consider, for e x a m p l e , the p r o b l e m of finding a closed f o r m s u m for

using the s t a n d a r d result (such results are c o m p u t e d automatically in [WNB92])

We therefore re-difference u n i f y goal and hypothesis to give, as w i t h the a s s o c i a t i v i t y e x a m p l e , a larger skeleton,

(5) We encode t h e p r o b l e m of finding a closed f o r m s u m as the task of p r o v i n g a t h e o r e m of the f o r m ,

where the e x i s t e n t i a l witness S is restricted to be in closed f o r m . T o prove t h i s t h e o r e m , w e f i r s t e l i m i n a t e the existential quantifier. T h e standard form m e t h o d [ W N B 9 2 ] t h e n difference unifies t h e dequantified goal w i t h (5) g i v i n g t h e m i n i m a l a n n o t a t i o n s

R i p p l i n g , t h o u g h u n a b l e t o move t h e differences u p c o m pletely, has reduced the inner difference. I n d e e d , the difference has been so reduced t h a t we can now s u b s t i t u t e t h e s t a n d a r d result i n t o t h e g o a l ,

T h e standard form m e t h o d now difference unifies against the s t a n d a r d result for the s u m of the first n integers, a n d ripples w i t h (7) t o complete the proof. 2.3 Other applications

We have explored a n u m b e r of other a p p l i c a t i o n s of difference u n i f i c a t i o n t h a t , for lack of space, we cannot develop here. For e x a m p l e , in [ B W 9 2 a ; B B H 9 3 ] we show how difference u n i f i c a t i o n can be used to guide r e w r i t i n g in so called proof by consistency techniques. O t h e r researchers have also e x p l o r e d a p p l i c a t i o n s of these ideas. H u t t e r has recently r e p o r t e d o n a p p l y i n g associative c o m m u t a t i v e difference u n i f i c a t i o n a n d r i p p l i n g t o solve S A M s l e m m a i n t h e I N K A system [CH92J.

3

Specification

To specify difference u n i f i c a t i o n we m u s t be m o r e precise a b o u t t h e representation o f a n n o t a t i o n s . A s i n [ B W 9 2 ] a n n o t a t i o n s are represented i n a n o r m a l f o r m i n w h i c h

118

Automated Reasoning

Basin and Walsh

119

F i g u r e 1: D U N I F Y : t r a n s f o r m a t i o n rules for difference u n i f y i n g s and t

These rules have been i m p l e m e n t e d in P r o l o g . T h e f o l l o w i n g t a b l e gives 8 o u t of the 24 results of difference u n i f y i n g ( X + Y ) + Z w i t h X + (Y + Z ) . N o t e t h a t for r e a d a b i l i t y we have merged adjacent wavefronts in t h e "box and hole" presentation.

u n i f i c a t i o n s . In the s t r o n g l y m i n i m a l case, p o t e n t i a l l y an e x p o n e n t i a l a m o u n t of search is saved. We first describe the s t r u c t u r e of the search space. Nodes correspond to the quadruples g i v i n g the current state. A r c s t o t h e left result f r o m a p p l y i n g one o f the u n i f i c a t i o n rules: D E L E T E , D E C O M P O S E , I M I T A T E L ,
IMITATER, EL1MINATE
L

,

and E L I M I N A T E R .

Arcs to

T h e first three a n n o t a t i o n s are s t r o n g l y m i n i m a l a n d give the o n l y wave-rules (oriented a p p r o p r i a t e l y ) . T h e f o u r t h , f i f t h and s i x t h a n n o t a t i o n s are neither w e a k l y nor s t r o n g l y m i n i m a l . T h e last t w o a n n o t a t i o n s are w e a k l y b u t n o t s t r o n g l y m i n i m a l . T h i s once again demonstrates t h a t difference u n i f i c a t i o n is n o t u n i t a r y , even w h e n res t r i c t e d t o s t r o n g o r weak m i n i m a l i t y . T h e f o l l o w i n g is a sample execution trace of the first result. I t results f r o m a p p l y i n g the rules: HIDEL, D E C O M P O S E , D E L E T E , H I D E R , and D E L E T E .

5

L e f t - f i r s t Search

the r i g h t result f r o m a p p l y i n g a h i d i n g r u l e : H I D E L a n d H I D E R . T h e key t o r e t u r n i n g m i n i m a l difference u n i f i cations is observing t h a t a n o n - m i n i m a l difference u n i fication uses m o r e a p p l i c a t i o n s of the h i d i n g rules t h a n a m i n i m a l one, t h o u g h it m a y use a greater, lesser or equal n u m b e r o f u n i f i c a t i o n rules. T h u s , i n searching the tree we w a n t to m i n i m i z e r i g h t arcs since each adds m o r e a n n o t a t i o n . We call a search a l g o r i t h m w h i c h does t h i s left-first search. At the n + 1-th p l y of the search we explore a l l those nodes whose p a t h back to the r o o t includes n r i g h t arcs. T h i s search strategy returns m i n i m a l cost solutions where h i d i n g rules ( r i g h t - r u l e s ) have ( u n i t ) cost and other rules (left-rules) h a v i n g no cost. We have i m p l e m e n t e d a m e t a - i n t e r p r e t e r t h a t p e r f o r m s t h i s search as follows. G i v e n a set of nodes TV, left*(N) r e t u r n s t h e set of nodes reachable f r o m t h e nodes in N by t a k i n g any n u m b e r of left arcs. T h e f u n c t i o n right(N) r e t u r n s t h e set of nodes reachable f r o m the nodes in N by t a k i n g one r i g h t arc. F i n a l l y solutions{N) returns any answers in the set of nodes N. Figure 2 gives the a l g o r i t h m a n d i l l u s t r a t e s the order in which nodes in a b i n a r y tree are explored under left-first search. For s t r o n g l y m i n i m a l difference u n i f i c a t i o n s , t h i s algor i t h m r e t u r n s t h e first set of answers a n d stops. For w e a k l y m i n i m a l difference u n i f i c a t i o n s , we m u s t save t h e answers generated, a n d continues to search c o m p a r i n g new answers f o r weak m i n i m a l i t y against previous ones. U n f o r t u n a t e l y , t o r e t u r n a l l t h e w e a k l y m i n i m a l difference u n i f i c a t i o n s we m u s t search the w h o l e tree. T h e advantage of l e f t - f i r s t search is t h a t we can i m m e d i a t e l y t e l l w h e t h e r an answer is w e a k l y m i n i m a l .

T h e t r a n s f o r m a t i o n rules, w h e n e x h a u s t i v e l y a n d n o n d e t e r m i n i s t i c a l l y a p p l i e d , generate a l l possible difference u n i f i c a t i o n s , n o t j u s t those t h a t are w e a k l y o r s t r o n g l y m i n i m a l . T h i s i s b o t h t i m e c o n s u m i n g a n d a l m o s t always unnecessary. We have therefore i m p l e m e n t e d a search a l g o r i t h m (i.e., a m e t a - i n t e r p r e t e r ) for t r a v e r s i n g t h e space defined by these rules so t h a t we are guaranteed to encounter j u s t t h e w e a k l y o r s t r o n g l y m i n i m a l difference

6

Properties

L e t u s i n t r o d u c e some n o t a t i o n t h a t w i l l b e used t o prove p r o p e r t i e s o f difference u n i f i c a t i o n a n d t h e D U N I F Y rule set. We w r i t e ) to i n dicate t h a t there is a d e r i v a t i o n D ( t h a t is, a possib l y e m p t y sequence o f D U N I F Y r u l e a p p l i c a t i o n s ) w h i c h

120

Automated Reasoning

Figure 2: Algorithm and Search Tree in turn follows from our restrictions on the deletion and elimination rule; they guarantee that every term position in Pos(B) and Pos(t) eventually appears in some equation in the derivation D. Since elements of A, are a subset of Pos(s) corresponding to addresses of function arguments in s, and likewise for At, appropriate hiding rule can always be applied. The soundness and completeness arguments only rely on the underlying unification algorithm being sound, complete, and "decompositional" in the sense that every position in the original terms eventually appears in the course of the derivation. Hence, if we replace the underlying unification algorithm with something stronger, e.g., incorporating equations that preserve these properties for some equational theory, then again we will have a sound and complete algorithm with respect to that theory. We suspect that there are many natural applications of equational difference unification, e.g., the previously mentioned work of Hutter. T h e o r e m 3 ( T e r m i n a t i o n ) The DUNIFY rule set always terminates. P r o o f (sketch): Given input s and i, use a lexicographic ordering on the triple ( I , V, F) were / is |Pos(s)| + |Pos()tI — / ' , V is the number of imitation steps performed in a sequence of rule applications, V is the number of distinct variables in the (current) equation set, and F is the number of function symbols (including constants) in the (current) equation set.

7

Complexity

DUNIFY has been given as a set of rules. If they are applied non-deterministically, it is easy to see that it can take exponential time to find a solution to a problem as we may, using the hide and imitate rules, consider all the ways of hiding function symbols. 1 A term of size n (n function symbols) has O(n) interior (neither constants or variables) function symbols that can be hidden in 0 ( 2 n ) different ways; hence, naive execution can be exponential. It is natural to ask whether this the best that we can do, and which are the tractible cases. In asking such questions we must distinguish between the Also note that unification algorithms which explicitly represent substitutions are not efficient. This can, however, be avoided by using a rule-based approach such as [JK9l] at the cost of rules with rather more complicated sideconditions.
1

Basin and Walsh

121

p r o b l e m o f generating all solutions a n d t h a t o f generati n g a s o l u t i o n or k n o w i n g if one exists. T h e first p r o b l e m is easily seen to require e x p o n e n t i a l size even in the very restricted of case of g r o u n d difference m a t c h i n g . T h e o r e m 4 There are difference m a t c h i n g problems req u i r i n g exponential t i m e .

This process eventually halts when the difference ts no longer negotiable [ v i a an assignment] f at which p o i n t the outcome depends on whether the difference is empty or nonempty." In t h i s l i g h t , our research can be seen as a direct extension of R o b i n s o n ' s n o t i o n of difference r e d u c t i o n : we reduce differences n o t j u s t b y variable assignment, b u t also b y t e r m s t r u c t u r e a n n o t a t i o n . W h a t makes our extended n o t i o n o f u n i f i c a t i o n tenable, indeed a t t r a c t i v e , is t h a t t h i s a n n o t a t i o n is precisely w h a t is required for r i p p l i n g t o remove t h i s difference.

References
P r o b l e m s generating e x p o n e n t i a l n u m b e r s o f solutions are exceptional as t h e y involve u n u s u a l a m o u n t s of repeated s t r u c t u r e . In general, there are far fewer matches a n d unifiers; so it is interesting to investigate the comp l e x i t y of r e t u r n i n g a single s o l u t i o n , or d e t e r m i n i n g if one exists. T h e first p r o b l e m is p o l y n o m i a l t i m e solvable for g r o u n d t e r m s . T h e o r e m 5 Given terms s and t we can determine if s difference matches t (s may be annotated w i t h skeleton t) or s difference unifies w i t h t in p o l y n o m i a l t i m e . P r o o f ( s k e t c h ) : I n [NS87] a n a l g o r i t h m based o n dyn a m i c p r o g r a m m i n g is given for s o l v i n g the h o m o m o r phic e m b e d d i n g p r o b l e m o f one g r o u n d t e r m i n t o another i n p o l y n o m i a l t i m e . T h i s p r o b l e m i s t h e same p r o b l e m as g r o u n d difference m a t c h i n g . It is easy to m o d i f y this idea to provide an a l g o r i t h m for g r o u n d difference u n i f i c a t i o n . F u r t h e r m o r e , these a l g o r i t h m s can be easily m o d i f i e d to r e t u r n sets of answers as well as i n d i c a t i n g if answers exist [ B W 9 2 a ] . . As a side note, observe t h a t w h i l e the above g r o u n d difference u n i f i c a t i o n a l g o r i t h m can be easily m o d i f i e d to y i e l d m i n i m a l answers, there is a t r i v i a l linear t i m e a l g o r i t h m for d e t e r m i n i n g difference u n i f i a b i l i t y a l t h o u g h it does n o t give m i n i m a l answers. T h a t is, s and t w i l l difference u n i f y iff they share at least one constant ( o f a r i t y 0 ) . In the n o n - g r o u n d case, s a n d t are difference u n i f i a b l e iff they share one constant or if either contains a variable. In t h i s respect, difference u n i f i c a t i o n is, perhaps s u r p r i s i n g l y , easier t h a n difference m a t c h i n g . I n general, difference u n i f i c a t i o n a n d a l l its s u b p r o b lems are t r i v i a l l y in NP since we can guess a n n o t a t i o n s a n d t h e n u n i f y o r m a t c h r e s u l t i n g skeletons i n p o l y n o m i a l t i m e . In the n o n g r o u n d case, when variables are added d e t e r m i n i n g the existence of a s o l u t i o n is NP h a r d . T h e o r e m 6 Difference u n i f y i n g s and t, w i t h annotat i o n on only one side is NP hard. T h e p r o o f is given in [ B W 9 2 a ] and uses a r e d u c t i o n f r o m 3 S A T s i m i l a r t o t h a t used i n the p r o o f o f the N P h a r d ness of s e t - m a t c h i n g given in [ K N 8 6 ] . R. B a r n e t t , D. Basin a n d J. Hesketh. A recursion p l a n n i n g analysis o f i n d u c t i v e complet i o n . A n n a l s o f M a t h s , a n d A I , 8(3-4), 1993. [BS88] K . Hans Blasius a n d J . S i e k m a n n . P a r t i a l u n i fication for g r a p h based e q u a t i o n a l reasoning. I n 9th C A D E , 3 9 7 - 4 1 4 , 1988. [BS+92] A . B u n d y , A . Stevens, F . van H a r m e l e n , A . I r e l a n d and A . S m a i l l . R i p p l i n g : A heurist i c for g u i d i n g i n d u c t i v e proofs. T o appear i n A r t i f i c i a l Intelligence, 1993. [Bun88] A. B u n d y . T h e use of e x p l i c i t plans to guide i n d u c t i v e p r o o f s . I n 9th C A D E , 111 120, 1988 [BW92] D . Basin and T . W a l s h . Difference m a t c h i n g . I n 11th C A D E , 2 9 5 - 3 0 9 , 1992. [ B W 9 2 a ] D . Basin a n d T . W a l s h . Difference u n i f i c a t i o n . Technical R e p o r t M P I - I - 9 2 - 2 4 7 , M a x - P l a n c k I n s t i t u t e f u r I n f o r m a t i k , 1992. [CH92] J. Cleve a n d D. H u t t e r . A new m e t h o d ology for e q u a t i o n a l reasoning. Univerity Saarbriicken Technical R e p o r t , 1993. [Dig85] V . D i g r i c o l i . T h e m a n a g e m e n t o f heuristic search i n boolean e x p e r i m e n t s w i t h R U E reso l u t i o n . I n 9th I J C A I , 1 1 5 4 - 1 1 6 1 , 1985. [Hut90] D . H u t t e r . G u i d i n g i n d u c t i v e proofs. I n 10th C A D E , 1 4 7 - 1 6 1 , 1990. [JK91] J.-P. J o u a n n a u d a n d C. K i r c h n e r . Solvi n g E q u a t i o n s in A b s t r a c t Algebras: A Rule Based Survey o f U n i f i c a t i o n . I n J . - L . Lassez and G. P l o t k i n , eds., C o m p u t a t i o n a l Logic. M I T Press, 1991. [KN86] D. K a p u r a n d P. N a r e n d r a n . NP-completeness of the set u n i f i c a t i o n and m a t c h i n g problems. I n 8th C A D E , 4 8 9 - 4 9 5 , 1986. [Mor69] J. M o r r i s . E-resolution: an extension of reso l u t i o n to include the equality r e l a t i o n . In Proceedings of the 1JCA1-69, 1969. [NS87] P. N a r e n d r a n and J. S t i l l m a n . In F i f t h I n t . C o n f o n A p p l i e d Algebra and E r r o r Correcti n g Codes, M e n o r c a , S p a i n , 1987. [NSS63] A . N e w e l l , J . C . Shaw a n d H . A . S i m o n . T h e logic t h e o r y m a c h i n e . I n Feigenbaum a n d F e l d m a n , editors, C o m p u t e r s and Thought. M c G r a w - H i l l , 1963. [Rob89] J . A . R o b i n s o n . Notes o n r e s o l u t i o n . I n F . L . Bauer, e d i t o r , Logic, Algebra, and C o m p u t a t i o n , pages 1 0 9 - 1 5 1 . Springer V e r l a g , 1989. [ W N B 9 2 ] T . W a l s h , A . Nunes a n d A . B u n d y . T h e use o f p r o o f plans t o s u m series. I n 11th C A D E , 325-339, 1992. [BBH93]

8

Conclusions

In [ R o b 8 9 ] , J . A . R o b i n s o n presented a s i m p l e account of u n i f i c a t i o n i n t e r m s o f difference r e d u c t i o n . H e observed: " U n i f i e r s remove differences ... We repeatedly reduce the difference between the two given expressions by applying to them an a r b i t r a r y reduction of the d i f ference and accumulate the product of these reductions.

122

Automated Reasoning


赞助商链接

更多相关文章:
更多相关标签:

All rights reserved Powered by 甜梦文库 9512.net

copyright ©right 2010-2021。
甜梦文库内容来自网络,如有侵犯请联系客服。zhit325@126.com|网站地图