"Science, Faculty of"@en . "Computer Science, Department of"@en . "DSpace"@en . "UBCV"@en . "Etherington, David William"@en . "2010-03-30T23:01:49Z"@en . "1982"@en . "Master of Science - MSc"@en . "University of British Columbia"@en . "The thesis presents a survey of formalisms for non-monotonic reasoning, providing a sketch of the \"state of the art\" in the field. Reiter's logic for default reasoning is discussed in detail. Following this, a procedure which can determine the extensions of general finite default theories is demonstrated.\r\nThe potential impact of this procedure on some of the other research in the field is explored, and some promising areas for future research are indicated. Grounds for cautious optimism about the tractability of default theories capable of representing a wide variety of common situations are presented."@en . "https://circle.library.ubc.ca/rest/handle/2429/23138?expand=metadata"@en . "F I N I T E DEFAULT THEORIES by DAVID WILLIAM ETHERINGTON B . S c , The U n i v e r s i t y o f L e t h b r i d g e , 1977 A THESIS SUBMITTED IN PARTIAL FULFILMENT OF THE REQUIREMENTS FOR THE DEGREE OF MASTER OF SCIENCE i n THE FACULTY OF GRADUATE STUDIES (Department o f Computer S c i e n c e ) We a c c e p t t h i s t h e s i s as c o n f o r m i n g t o the r e q u i r e d s t a n d a r d . THE UNIVERSITY OF BRITISH COLUMBIA AUGUST, 198 2 (c) D a v i d W i l l i a m E t h e r i n g t o n , 1982 In presenting t h i s thesis i n p a r t i a l f u l f i l m e n t of the requirements for an advanced degree at the University of B r i t i s h Columbia, I agree that the Library s h a l l make i t f r e e l y available for reference and study. I further agree that permission for extensive copying of t h i s thesis for scholarly purposes may be granted by the head of my department or by his or her representatives. I t i s understood that copying or publication of t h i s thesis for f i n a n c i a l gain s h a l l not be allowed without my written permission. Department of Computer Sc ience The University of B r i t i s h Columbia 1956 Main Mall Vancouver, Canada V6T 1Y3 \u00E2\u0080\u00A2J n a + . _ 1 September 1982 . DE-6 (3/81) A b s t r a c t The t h e s i s p r e s e n t s a s u r v e y o f f o r m a l i s m s f o r non-monotonic r e a s o n i n g , p r o v i d i n g a s k e t c h o f t h e \" s t a t e o f t h e a r t \" i n t h e f i e l d . R e i t e r ' s l o g i c f o r d e f a u l t r e a s o n i n g i s d i s c u s s e d i n d e t a i l . F o l l o w i n g t h i s , a p r o c e d u r e which can d e t e r m i n e t h e e x t e n s i o n s o f g e n e r a l f i n i t e d e f a u l t t h e o r i e s i s d e m o n s t r a t e d . The p o t e n t i a l impact o f t h i s p r o c e d u r e on some o f the o t h e r r e s e a r c h i n the f i e l d i s e x p l o r e d , and some p r o m i s i n g a r e a s f o r f u t u r e r e s e a r c h a r e i n d i c a t e d . Grounds f o r c a u t i o u s o p t i m i s m a b o u t t h e t r a c t i b i l i t y o f d e f a u l t t h e o r i e s c a p a b l e o f r e p r e s e n t i n g a wide v a r i e t y o f common s i t u a t i o n s a r e p r e s e n t e d . T a b l e o f C o n t e n t s A b s t r a c t i i T a b l e o f F i g u r e s i v Acknowledgements v 1 I n t r o d u c t i o n 1 1.1 I n c o m p l e t e Knowledge 1 1.2 O v e r v i e w 4 2 N o n - M o n o t o n i c R e a s o n i n g 6 2.1 N e g a t i o n As F a i l u r e To D e r i v e 8 2.2 D a t a b a s e C o m p l e t i o n 11 2.3 C i r c u m s c r i p t i o n 13 2.4 D e f a u l t L o g i c 15 2.4.1 D e f a u l t T h e o r i e s 16 2.4.2 C l o s e d D e f a u l t T h e o r i e s and T h e i r E x t e n s i o n s ... 19 2.4.3 G e n e r a l D e f a u l t T h e o r i e s 22 2.5 N o n - M o n o t o n i c L o g i c 24 2.6 C o n s i s t e n c y M a i n t e n a n c e 27 2.7 S e m a n t i c N e t w o r k s 28 2.8 O b j e c t i o n s t o N o n - M o n o t o n i c F o r m a l i s m s 32 3 D e t e r m i n i n g t h e E x t e n s i o n s o f D e f a u l t T h e o r i e s 34 3.1 M o t i v a t i o n 34 3.2 A C o n s t r u c t i v e Mechanism 35 D e f i n i t i o n 3.1 37 Lemma 3.2 38 Lemma 3.3 38 Theorem 3.4 40 C o r o l l a r y 3.5 44 Theorem 3.6 46 Lemma 3.7 49 4 D i r e c t i o n s f o r F u t u r e R e s e a r c h 56 4.1 D e f a u l t T ype H i e r a r c h i e s 56 4.2 P a r a l l e l I n h e r i t a n c e M a c h i n e s 58 4.3 T r u t h M a i n t e n a n c e 61 4.4 T h e o r e t i c a l A n a l y s i s 61 5 C o n c l u s i o n 63 5.1 E v a l u a t i o n o f R e s u l t s 63 5.1.1 F i n i t e n e s s R e s t r i c t i o n s 63 5.1.2 I n f i n i t e T h e o r i e s 64 5.1.3 C o m p u t a t i o n a l C o n s i d e r a t i o n s 65 5.2 Summary 67 B i b l i o g r a p h y 69 APPENDIX A ( D i c t i o n a r y o f Symbols) 72 i i i T a b l e o f F i g u r e s 2.1a \u00E2\u0080\u0094 A t y p i c a l NETL example 30 2.1b \u00E2\u0080\u0094 D e f a u l t t h e o r y f o r F i g u r e 2.1a 30 2.2a \u00E2\u0080\u0094 A p r o b l e m a t i c c a s e 31 2.2b \u00E2\u0080\u0094 D e f a u l t t h e o r y f o r F i g u r e 2.2a 31 4.1 \u00E2\u0080\u0094 D must be a c t i v a t e d b e f o r e E 59 4.2 \u00E2\u0080\u0094 E must be a c t i v a t e d b e f o r e D 59 i v Acknowledgments The m a t e r i a l i n t h i s t h e s i s owes much t o l o n g h o u r s o f f r u i t f u l d i s c u s s i o n s w i t h Ray R e i t e r and Bob M e r c e r . They, t o g e t h e r w i t h P a u l G i l m o r e , A k i r a Kanda, and J a n i n e E t h e r i n g t o n , a l s o made many h e l p f u l comments on e a r l i e r d r a f t s o f some s e c t i o n s . Dave T o u r e t z k y p r o v i d e d i n s i g h t i n t o t h e p r o b l e m s i n t r o d u c e d by c a n c e l l a t i o n i n i n h e r i t a n c e s t r u c t u r e s , and i n t o t h e w o r k i n g s o f NETL. J a n i n e p r o v i d e d t h e p e r s p e c t i v e r e q u i r e d t o s e e t h e e n t e r p r i s e t h r o u g h . The f i n a n c i a l s u p p o r t o f a N a t u r a l S c i e n c e and E n g i n e e r i n g R e s e a r c h C o u n c i l o f Canada p o s t g r a d u a t e s c h o l a r s h i p i s a l s o g r a t e f u l l y a c k n o w l e d g e d . v C h a p t e r 1 I n t r o d u c t i o n A r t i f i c i a l I n t e l l i g e n c e ( A l ) r e s e a r c h e r s have shown a g r e a t d e a l o f i n t e r e s t i n t h e a b i l i t y t o d e a l w i t h i n c o m p l e t e or i n c o n s i s t e n t i n f o r m a t i o n . Much o f human i n t e l l i g e n t b e h a v i o u r a p p a r e n t l y d e r i v e s f r o m t h i s c a p a c i t y t o draw c o n c l u s i o n s i n t h e a b s e n c e o f t o t a l knowledge. T h i s s u g g e s t s t h a t e x i s t i n g a p p r o a c h e s t o r e a s o n i n g and knowledge r e p r e s e n t a t i o n s h o u l d be c a r e f u l l y r e - e x a m i n e d t o c a p i t a l i z e on t h e i r s t r e n g t h s and r e d r e s s t h e i r w e a knesses i n t h i s a r e a . T h i s t h e s i s examines s e v e r a l a p p r o a c h e s , f o c u s s i n g on t h e way each a t t e m p t s t o d e a l w i t h t h e s e p r o b l e m s . D e f a u l t L o g i c ( R e i t e r 1980) p r o v i d e s a s u i t a b l e framework f o r s t u d y i n g many knowledge r e p r e s e n t a t i o n i s s u e s . A t r a c t i b l e means f o r a p p l y i n g D e f a u l t L o g i c t o many common p r o b l e m d o m ains, s u c h as s e m a n t i c n e t w o r k s and d a t a b a s e s , i s p r e s e n t e d . 1.1 I n c o m p l e t e Knowledge I t has been a r g u e d t h a t i f a l l o f t h e f a c t s w h i c h i m p i n g e on any g i v e n d e c i s i o n had t o be c o n s i d e r e d , human r e a s o n i n g \u00E2\u0080\u0094 as i t i s commonly e x p e r i e n c e d \u00E2\u0080\u0094 would be i m p o s s i b l e . F o r example, t h e 1 I n c o m p l e t e Knowledge 2 s h e e r volume o f t h i n g s w h i c h a r e n o t t r u e a b o u t t h e w o r l d has f o r c e d many t o t r e a t much o f t h i s knowledge as i m p l i c i t \u00E2\u0080\u0094 so t h a t i t need o n l y be r e p r e s e n t e d or m a n i p u l a t e d when n e c e s s a r y . S e m a n t i c n e t w o r k s t u r n t h i s n e c e s s i t y i n t o a v i r t u e . I f l a r g e amounts o f i n f o r m a t i o n c a n be e x c l u d e d f r o m t h e knowledge b a s e , t h e i n t e r a c t i o n s between f a c t s d u r i n g t h e \" d e d u c t i o n \" p r o c e s s a r e r e s t r i c t e d . So c o n s t r a i n i n g t h e \" c o m b i n a t o r i a l e x p l o s i o n \" may r e s u l t i n s i g n i f i c a n t improvements i n s p e e d . I n d a t a b a s e t h e o r y , i t i s a l s o common n o t t o e x p l i c i t l y r e p r e s e n t much o f t h e n e g a t i v e i n f o r m a t i o n a b o u t a domain (eg t h e c i t i e s a g i v e n a i r l i n e f l i g h t d o e s n o t c o n n e c t ) . The i m p l i c a t i o n i s t h a t a n y t h i n g n o t ( s t a t e d t o be) t r u e must be f a l s e ( c f [Codd 1972, R e i t e r 1 9 8 1 a ] ) . The p r o b l e m o f r e p r e s e n t i n g and u s i n g \" n e g a t i v e i n f o r m a t i o n \" m a n i f e s t s i t s e l f i n a v a r i e t y o f o t h e r ways i n c l u d i n g , i n a s l i g h t l y d i f f e r e n t f o r m , t h e c e l e b r a t e d \"frame p r o b l e m \" (M c C a r t h y and Hayes 1969, R a p h a e l 1 9 7 1 ) . Many i d e a s have been p r o p o s e d t o h e l p r e d u c e t h e amount o f n e g a t i v e i n f o r m a t i o n w h i c h must be d e a l t w i t h . Most p r o v i d e mechanisms embodying t h e r u l e : \" I f you do n o t 'know' X t h e n i n f e r - i X \" . T h i s r u l e h i n g e s on an a s s u m p t i o n l i k e : \" I f X were t r u e , I w o u l d know X \" , o r \" E v e r y t h i n g a b o u t t h e w o r l d i s known\" ( c f R e i t e r 1 9 7 8 ) . A n o t h e r f o r m o f r e a s o n i n g w i t h i n c o m p l e t e i n f o r m a t i o n i s c h a r a c t e r i z e d by s t a t e m e n t s s u c h a s : \"Most A's a r e B's\" o r \" T y p i c a l A's a r e B ' s \" . Such s t a t e m e n t s c a p t u r e t h e i n t u i t i o n u n d e r l y i n g network r e p r e s e n t a t i o n s o f knowledge, t h a t a g r e a t d e a l o f knowledge a b o u t t h e w o r l d i n v o l v e s \" p r o t o t y p e s \" o f I n c o m p l e t e Knowledge 3 members o f c l a s s e s . G r e a t e c o n o m i e s o f d e s c r i p t i o n c a n be o b t a i n e d i n t h i s f a s h i o n . I t becomes u n n e c e s s a r y t o a t t a c h a l l o f t h e p r o p e r t i e s a s s o c i a t e d w i t h members o f a c l a s s t o e v e r y member. When i n f o r m a t i o n i s r e q u i r e d a b o u t a p a r t i c u l a r member o f a c l a s s , i t c a n be o b t a i n e d by c o n s u l t i n g t h e d e s c r i p t i o n o f t h e c l a s s p r o t o t y p e . P r o t o t y p i c d e s c r i p t i o n s a r e o f t e n c a l l e d \" d e f a u l t d e s c r i p t i o n s \" ( R e i t e r 1 9 7 8 a ) , s i n c e t h e y t e n d t o be a p p l i e d o n l y i n t h e a b s e n c e o f c o n t r a d i c t o r y e v i d e n c e . F o r example, one c a n p r e d i c t t h a t C l y d e t h e e l e p h a n t i s g r a y w i t h o u t s e e i n g him or b e i n g t o l d h i s c o l o u r , b u t one must be a b l e t o c o n s i s t e n t l y d e a l w i t h t h e f a c t t h a t F r e d \u00E2\u0080\u0094 w h i l e an e l e p h a n t \u00E2\u0080\u0094 i s w h i t e (or p i n k ) . T h e r e i s a l a r g e body o f l i t e r a t u r e d e t a i l i n g a t t e m p t s t o t a k e a d v a n t a g e o f t h e r e p r e s e n t a t i o n a l power o f p r o t o t y p i c d e s c r i p t i o n s , some o f w h i c h i s d i s c u s s e d i n t h e f o l l o w i n g c h a p t e r . P r o t o t y p i c r e a s o n i n g p r o v i d e s t o o l s w h i c h make i t e a s i e r t o d e a l w i t h t h e i m p r e c i s i o n e n c o u n t e r e d i n e v e r y d a y l i f e . U n f o r t u n a t e l y , t h e s e t o o l s a r e n o t w i t h o u t t h e i r own p r o b l e m s . A d m i t t i n g i m p r e c i s i o n i n t o one's r e a s o n i n g mechanisms i s an open i n v i t a t i o n t o i m p r e c i s i o n i n one's c o n c l u s i o n s . T h i s may m a n i f e s t i t s e l f i n s i t u a t i o n s i n w h i c h t h e r e a r e no g r o u n d s f o r d e c i d i n g between a l t e r n a t i v e s , o r where c o n c l u s i o n s drawn a r e i n c o n s i s t e n t w i t h f u r t h e r s p e c i f i c a t i o n o f t h e s i t u a t i o n b e i n g r e a s o n e d a b o u t . (The l a t t e r c o n d i t i o n i s a c o n s e q u e n c e o f n o n - m o n o t o n i c i t y , w h i c h i s d i s c u s s e d i n d e t a i l i n C h a p t e r 2.) O v e r v i e w 4 1.2 O v e r v i e w C h a p t e r 2 c o n s i d e r s s e v e r a l a s p e c t s o f t h e p r o b l e m o f d e a l i n g w i t h i n c o m p l e t e i n f o r m a t i o n , t o g e t h e r w i t h some p a r t i a l s o l u t i o n s w h i c h have been p r o p o s e d . The l a t t e r r a n g e f r o m t h e v e r y f o r m a l t o t h e ad h o c . One o f t h e more f o r m a l , \" D e f a u l t L o g i c \" ( R e i t e r 1 9 8 0 ) , i s examined i n d e t a i l . T h i s d i s c u s s i o n i s i n t e n d e d t o p r o v i d e t h e r e a d e r f a m i l i a r o n l y w i t h f i r s t - o r d e r l o g i c w i t h t h e c o n c e p t s n e c e s s a r y t o u n d e r s t a n d t h e d e v e l o p m e n t o f t h e major c o n t r i b u t i o n o f t h i s t h e s i s . T h i s o c c u r s i n C h a p t e r 3, w h i c h p r e s e n t s a mechanism f o r d e t e r m i n i n g t h e b e l i e f s s a n c t i o n e d by p a r t i c u l a r d e f a u l t t h e o r i e s . C h a p t e r 4 o u t l i n e s d i r e c t i o n s i n w h i c h t h i s r e s e a r c h m i g h t be e x t e n d e d . The d i s c u s s i o n b r e a k s down i n t o two c a t e g o r i e s : p r o b l e m s s p e c i f i c t o d e f a u l t l o g i c , and p r o b l e m s o f d e t e r m i n i n g t h e i n t e r r e l a t i o n s h i p s between d e f a u l t l o g i c and o t h e r work i n t h e f i e l d . I t w i l l become a p p a r e n t t h a t t h e s e p a r a t i o n i s somewhat a r b i t r a r y ; r e s u l t s i n e i t h e r a r e a a r e l i k e l y t o have a s i g n i f i c a n t i m p a c t i n b o t h . C h a p t e r 5 e v a l u a t e s t h e s i g n i f i c a n c e o f t h e r e s u l t s p r e s e n t e d . The e f f e c t s o f t h e r e s t r i c t i o n s p l a c e d on t h e a l l o w a b l e c l a s s o f t h e o r i e s i s d i s c u s s e d . T h i s i s f o l l o w e d by some s p e c u l a t i o n c o n c e r n i n g t h e p o s s i b i l i t y o f o b t a i n i n g more p o w e r f u l r e s u l t s a l o n g s i m i l a r l i n e s . The t h e s i s c o n c l u d e s w i t h a s h o r t summary. The m a t e r i a l p r e s e n t e d i s r e l a t i v e l y s e l f - c o n t a i n e d , a s s u m i n g o n l y a f a m i l i a r i t y w i t h t r a d i t i o n a l f i r s t o r d e r l o g i c (see O v e r v i e w 5 [ M e n d e l s o n 1964] f o r an i n t r o d u c t i o n ) . The l a t e r c h a p t e r s , however, draw f r e e l y on c o n c e p t s p r e s e n t e d e a r l i e r . R e a d e r s f a m i l i a r w i t h n o n - m o n o t o n i c r e a s o n i n g i n g e n e r a l , and w i t h d e f a u l t l o g i c i n p a r t i c u l a r , may w i s h t o m e r e l y s k i m C h a p t e r 2. T h o s e i n t e r e s t e d i n an o n l y m o d e s t l y t e c h n i c a l o v e r v i e w o f non-m o n o t o n i c r e a s o n i n g may w i s h t o r e s t r i c t t h e m s e l v e s t o t h a t c h a p t e r . F i n a l l y , t h e p r o o f s o f t h e theorems p r e s e n t e d i n C h a p t e r 3 may be s k i p p e d w i t h o u t l o s s o f c o n t i n u i t y , p r o v i d e d t h e t h eorems t h e m s e l v e s a r e u n d e r s t o o d . Chapter 2 Non-Monotonic Reasoning T r a d i t i o n a l l o g i c s suffer from the 'Monotonicity Problem' \u00E2\u0080\u0094 Drew McDermott In t r a d i t i o n a l l o g i c a l systems, extending a set of axioms, S, can never prevent the derivation of conclusions derivable from S alone. More formally, i f S and S' are a r b i t r a r y sets of formulae then: S C S' => {w| S \- w} C {w| S' |- w}.1 The addition of formulae to a set monotonically increases what can be proved from that set, hence the lo g i c s are sometimes c a l l e d monotonic.* More recently, i t has been noted that monotonic l o g i c s seem inadequate to capture the tentative nature of human reasoning. Since peoples' knowledge about the world i s necessarily incomplete, there w i l l always be times when they w i l l be forced to draw conclusions based on an incomplete s p e c i f i c a t i o n of pertinent d e t a i l s of the s i t u a t i o n . Under such circumstances, S j- w means w i s provable from premises S. o This property has been c a l l e d the extension property by Hayes (1973) and others, but the former term appears to be gaining pre-eminence. For this reason, and because \"extension\" has been used in so many ways in the related l i t e r a t u r e , \"monotonic\" w i l l be used in this discussion. 6 7 a s s u m p t i o n s a r e made ( i m p l i c i t l y o r e x p l i c i t l y ) a b o u t t h e s t a t e o f t h e unknown f a c t o r s . B e c a u s e t h e s e a s s u m p t i o n s a r e n o t i r r e f u t a b l e , t h e y may have t o be w i t h d r a w n a t some l a t e r t i m e s h o u l d new e v i d e n c e p r o v e them i n v a l i d . I f t h i s h a p p e n s , t h e new e v i d e n c e w i l l p r e v e n t some a s s u m p t i o n s f r o m b e i n g u s e d ; h e n c e a l l c o n c l u s i o n s w h i c h c a n be a r r i v e d a t o n l y i n c o n j u n c t i o n w i t h t h o s e a s s u m p t i o n s w i l l no l o n g e r be d e r i v a b l e . T h i s c a u s e s any s y s t e m w h i c h a t t e m p t s t o r e a s o n c o n s i s t e n t l y u s i n g a s s u m p t i o n s t o e x h i b i t n o n - m o n o t o n i c b e h a v i o r . I n A I , a t t e m p t s t o s o l v e t h e p r o b l e m s p r e s e n t e d by i n c o m p l e t e i n f o r m a t i o n have f a l l e n i n t o two c a t e g o r i e s . The f i r s t c a t e g o r y i n c l u d e s t h o s e w h i c h assume t h a t a l l o f t h e r e l e v a n t p o s i t i v e i n f o r m a t i o n (eg w h i c h i n d i v i d u a l s e x i s t , w h i c h p r e d i c a t e s a r e s a t i s f i e d by w h i c h i n d i v i d u a l s ) i s known. From t h i s a s s u m p t i o n , i t f o l l o w s t h a t a n y t h i n g w h i c h i s n o t \"known\" t o be t r u e must be f a l s e . N e g a t i v e f a c t s c a n t h u s be o m i t t e d , s i n c e t h e y c a n be i n f e r r e d f r o m t h e a b s e n c e o f t h e i r p o s i t i v e c o u n t e r p a r t s . Such a s s u m p t i o n s t y p i f y PLANNER'S \"THNOT\" ( H e w i t t 1972) and r e l a t e d n e g a t i o n o p e r a t o r s i n AI programming l a n g u a g e s ( R e i t e r 1 9 7 8 a ) , as w e l l as P r e d i c a t e C o m p l e t i o n ( C l a r k 1 9 7 8 ) , C i r c u m s c r i p t i o n ( M c C a r t h y 1980) and t h e C l o s e d W o r l d A s s u m p t i o n ( R e i t e r 1 9 7 8 ) , a l l o f w h i c h a r e d i s c u s s e d below, and many o t h e r s . I n c o n t r a s t , many have wanted t o r e p r e s e n t and u s e what would g e n e r a l l y d e s c r i b e d as \" d e f a u l t \" o r \" p r o t o t y p i c \" i n f o r m a t i o n . D e f a u l t s a r e u s e d t o f i l l gaps i n knowledge. I n t h e a b s e n c e A f a c t i s n e g a t i v e i f f a l l o f t h e l i t e r a l s i n i t s c l a u s a l f o r m a r e n e g a t i v e . 8 o f s p e c i f i c e v i d e n c e , t h e y a l l o w a s y s t e m t o make ( h o p e f u l l y ) e n l i g h t e n e d \" g u e s s e s \" i n s t e a d o f r e s e r v i n g judgement or a s s u m i n g t h a t w h a t e v e r i s unknown i s f a l s e . N o n - M o n o t o n i c L o g i c (McDermott and -Doyle 1 9 8 0 ) , D e f a u l t L o g i c ( R e i t e r 1 9 8 0 ) , T r u t h M a i n t e n a n c e Systems ( D o y l e 1 9 7 9 , M c A l l e s t e r 1 9 7 8 , 1 9 8 0 ) , and v a r i o u s f r a m e - b a s e d p r o c e d u r a l knowledge r e p r e s e n t a t i o n schemes (M i n s k y 1 9 7 5 ) a l l embody t h i s i d e a . The two a p p r o a c h e s a r e n o t m u t u a l l y e x c l u s i v e \u00E2\u0080\u0094 i n some i n s t a n c e s , a t l e a s t , t h e l a t t e r subsumes t h e f o r m e r \u00E2\u0080\u0094 b u t c o m p a r i s o n s o f t h e i r power a r e most n o t a b l e f o r t h e i r a b s e n c e f r o m t h e l i t e r a t u r e . The d i s c u s s i o n i n t h e r e m a i n d e r o f t h i s c h a p t e r d o e s n o t p r o v i d e s u c h a c o m p a r i s o n , a l t h o u g h some p o i n t s o f c o r r e s p o n d e n c e a r e i n d i c a t e d . 2.1 N e g a t i o n As F a i l u r e To D e r i v e N e g a t i v e f a c t s \u00E2\u0080\u0094 t h o s e w h i c h s t a t e what i s NOT t r u e a b o u t t h e w o r l d \u00E2\u0080\u0094 v a s t l y outnumber p o s i t i v e f a c t s . F o r example, i n a d i s c u s s i o n a t a s u f f i c i e n t l y h i g h l e v e l , e v e r y t h i n g w h i c h i s a t some p l a c e i s NOT a t EVERY o t h e r p l a c e . S i m i l a r l y , i f Tumnus i s a c a t , he i s n o t a dog, f i s h , t r e e , e t c . The amount o f n e g a t i v e i n f o r m a t i o n a b o u t a w o r l d i n c r e a s e s g e o m e t r i c a l l y w i t h t h e s i z e o f t h e H e r b r a n d U n i v e r s e . 4 One would l i k e t o a v o i d h a v i n g t o r e p r e s e n t a l l s u c h i n f o r m a t i o n . The i n f o r m a t i o n must r e m a i n The H e r b r a n d U n i v e r s e i s t h e s e t o f a l l g r o u n d t e rms c o n s t r u c t a b l e f r o m t h e c o n s t a n t s and o t h e r f u n c t i o n s y m b o l s . N e g a t i o n As F a i l u r e To D e r i v e 9 a v a i l a b l e , however \u00E2\u0080\u0094 a t some p o i n t i t may become u s e f u l t o know t h a t Tumnus i s n o t a dog. AI programming l a n g u a g e s (eg PROLOG [ R o u s s e l 1 9 7 5 ] , PLANNER) have o f t e n a d d r e s s e d t h i s p r o b l e m by r e p r e s e n t i n g o n l y p o s i t i v e i n f o r m a t i o n , a s s u m i n g t h a t i f s o m e t h i n g c a n n o t be shown t o be t r u e i t must be f a l s e . Such s y s t e m s embody an i n f e r e n c e r u l e o f t h e f o r m : I f Y P t h e n i n f e r f- nP w h i c h c a n be p a r a p h r a s e d as \" I f P i s n o t p r o v a b l e f r o m t h e d a t a b a s e , assume -iP as a lemma o f t h e d a t a b a s e \" . A d e r i v a t i o n o f iP t h u s c o n s i s t s o f an u n s u c c e s s f u l e x h a u s t i v e s e a r c h f o r a d e r i v a t i o n o f P. T h i s t e c h n i q u e i s c a l l e d n e g a t i o n as f a i l u r e (NAF). D e s p i t e i t s a t t r a c t i v e n e s s as a means o f i m p l i c i t l y r e p r e s e n t i n g n e g a t i v e knowledge, NAF i s n o t w i t h o u t s h o r t c o m i n g s and p i t f a l l s . The most o b v i o u s o f t h e s e i s t h a t t h e r e i s no room f o r i n c o m p l e t e knowledge i n s u c h s y s t e m s \u00E2\u0080\u0094 a n y t h i n g w h i c h i s n o t known w i l l be assumed f a l s e . R e i t e r (1978) c a l l s t h i s a s s u m p t i o n o f \" t o t a l knowledge a b o u t t h e domain b e i n g r e p r e s e n t e d \" t h e C l o s e d W o r l d A s s u m p t i o n (CWA), s i n c e i t i m p l i e s a c l o s e d domain i n w h i c h a l l p o s s i b i l i t i e s a r e known. To s e e t h e p r o b l e m s p r e s e n t e d by i n c o m p l e t e i n f o r m a t i o n , c o n s i d e r a d a t a b a s e c o n s i s t i n g o f o n l y BLOCK(A) V BLOCK ( B ) . S i n c e i t i s i m p o s s i b l e t o d e r i v e e i t h e r BLOCK (A) o r BLOCK(B), NAF a l l o w s t h e d e r i v a t i o n o f nBLOCK(A) and ^ L O C K ( B ) . I t i s e a s y t o s e e t h a t s u c h s i t u a t i o n s a r e n o t c o n s i s t e n t w i t h NAF. The f a c t t h a t some c l a s s i c a l l y c o n s i s t e n t d a t a b a s e s a r e n o t N e g a t i o n As F a i l u r e To D e r i v e 10 c o n s i s t e n t w i t h t h e C W A l e a d s t o t h e q u e s t i o n , \"Under what c i r c u m s t a n c e s c a n t h e n e g a t i o n as f a i l u r e i n f e r e n c e r u l e (and hen c e t h e CWA) be c o n s i s t e n t l y employed?\" T h e r e i s no c o m p l e t e c h a r a c t e r i z a t i o n o f s u i t a b l e d a t a b a s e s , b u t i t has been shown t h a t a s u f f i c i e n t c o n d i t i o n i s t h a t t h e d a t a b a s e be H o r n J and c o n s i s t e n t . P u r e l y n e g a t i v e i n f o r m a t i o n p l a y s no p a r t i n c l o s e d - w o r l d q u e r y e v a l u a t i o n f o r s u c h d a t a b a s e s . I t c a n be i g n o r e d w i t h o u t l o s s o f d e d u c t i v e power ( R e i t e r 1 9 7 8 ) . E v e n t h o u g h a p a r t i c u l a r d a t a b a s e may be c o n s i s t e n t w i t h t h e CWA, i m p l e m e n t a t i o n s u s i n g NAF a r e n o t g u a r a n t e e d t o be c o m p l e t e . Answers t o a q u e r y , a l t h o u g h i m p l i e d by t h e d a t a b a s e , may be m i s s e d . I t has been n o t e d , f o r example, t h a t NAF must be a p p l i e d o n l y t o g r o u n d l i t e r a l s i f i n f e r e n c e s drawn a r e t o be c o r r e c t ( C l a r k 1978, R e i t e r 1 9 7 8 ) . S i g n i f i c a n t l y , n e i t h e r PROLOG nor PLANNER make s u c h s t i p u l a t i o n s . The f o l l o w i n g example i l l u s t r a t e s t h e p r o b l e m s t h a t t h i s may c a u s e . F o r t h e PROLOG d a t a b a s e : E Q U A L ( x , x ) . BLOCK(A). BLOCK(B). TWO-BLOCKS(x,y) <- n E Q U A L ( x , y ) & BLOCK(x) & B L O C K ( y ) . t h e q u e r y : <- TWO-BLOCKS(x,y). a l w a y s f a i l s . PROLOG 'S s e l e c t i o n r u l e , a l w a y s r e s o l v e on t h e l e f t m o s t l i t e r a l f i r s t , c a u s e s t h e g o a l T E Q U A L ( x , y ) t o be s e l e c t e d w i t h t h e v a r i a b l e s x and y unbound. Thus t h e s u b g o a l EQUAL(x,y) i s n o t g r o u n d and c a n be p r o v e d w i t h t h e u n i f y i n g 5 A d a t a b a s e i s Horn i f and o n l y i f each c l a u s e i n t h e c l a u s a l f o r m has a t most one p o s i t i v e l i t e r a l . N e g a t i o n As F a i l u r e To D e r i v e 11 s u b s t i t u t i o n 'x f o r y ' . No f a i l u r e p r o o f f o r nEQUAL(x,y) w i l l be f o u n d , even though one e x i s t s . -iTWO-BLOCKS (x,y) may be i n f e r r e d d e s p i t e t h e f a c t t h a t t h i s i s i n c o n s i s t e n t w i t h t h e d a t a b a s e . I t s h o u l d be remembered t h a t t h e s e a r e p r o b l e m s w i t h p a r t i c u l a r i m p l e m e n t a t i o n s o f NAF, n o t w i t h NAF i t s e l f . The r e q u i r e m e n t s f o r t h e c o r r e c t f u n c t i o n i n g o f s u c h s y s t e m s have been c l e a r l y l a i d o u t . U n f o r t u n a t e l y , c o r r e c t n e s s and c o m p l e t e n e s s a r e o f t e n s a c r i f i c e d f o r t h e s a k e o f s i z e a b l e g a i n s i n s p e e d . I t i s assumed t h a t i n c o m p l e t e n e s s i s b e t t e r t h a n i n e f f i c i e n c y . Whether t h i s a s s u m p t i o n i s a p p r o p r i a t e d e pends on t h e a p p l i c a t i o n , and t h e f a c t t h a t an i m p l e m e n t a t i o n i s i n c o m p l e t e may n o t be known t o i t s u s e r s . 2.2 D a t a b a s e C o m p l e t i o n NAF a l l o w s one t o a c t on t h e a s s u m p t i o n t h a t \" t h e o b j e c t s t h a t c a n be shown t o have a c e r t a i n p r o p e r t y , P, by r e a s o n i n g f r o m c e r t a i n f a c t s , A, a r e a l l t h e o b j e c t s t h a t s a t i s f y P\" (Mc C a r t h y 1 9 8 0 ) . I t does n o t , however, a l l o w t h e r e a s o n e r t o d e r i v e t h i s a s s u m p t i o n . Such s y s t e m s c a n n e v e r be \" c o n s c i o u s \" o f t h e u n d e r l y i n g p r i n c i p l e s w h i c h t h e y a r e i m p l i c i t l y a s s u m i n g . C l a r k ( 1 9 7 8 ) r e m e d i e s t h i s s h o r t c o m i n g by making t h e c o m p l e t e n e s s a s s u m p t i o n s e x p l i c i t i n t h e d a t a b a s e . A l l o f t h e i n f o r m a t i o n a b o u t a p a r t i c u l a r r e l a t i o n i n DB i s g a t h e r e d t o g e t h e r and a c o m p l e t i o n axiom i s added w h i c h s t a t e s t h a t a p a r t i c u l a r t u p l e D a t a b a s e C o m p l e t i o n 12 s a t i s f i e s t h e r e l a t i o n o n l y i f DB s a y s i t must. A p p l y i n g t h i s p r o c e s s t o a l l o f t h e r e l a t i o n s i n DB y i e l d s t h e c o m p l e t e d d a t a b a s e ( C ( D B ) ) . T h i s c o m p l e t i o n o f t h e d a t a b a s e makes e x p l i c i t t h e a s s u m p t i o n s o f t o t a l w o r l d knowledge. F o r example, i f t h e d a t a b a s e c o n t a i n s : ON(A,B) and ON(B,C) (1) and no g e n e r a l r u l e s a b o u t t h e ON r e l a t i o n , t h e n t h e c o m p l e t i o n a xiom i s : Vky.[ON(x ry) D ( x = A A Y = B ) V (x=B A y = C ) ] (2) C o m b i n i n g ( 1 ) , ( 2 ) , and i n e q u a l i t y schemata s t a t i n g t h a t d i f f e r e n t names d e n o t e d i f f e r e n t o b j e c t s r e s u l t s i n t h e c o n c l u s i o n t h a t (A,B) and (B,C) f o r m t h e c o m p l e t e e x t e n s i o n f o r ON. R e i t e r (1981a) e x p l o r e s t h e e f f e c t s o f a d d i n g c o m p l e t i o n axioms t o n o r m a l r e l a t i o n a l d a t a b a s e s . He d e m o n s t r a t e s t h a t s u c h t e c h n i q u e s p r o v i d e a means f o r d e a l i n g w i t h t y p e s o f i n c o m p l e t e i n f o r m a t i o n commonly e n c o u n t e r e d i n t h e d a t a b a s e f i e l d , s u c h as n u l l v a l u e s and d i s j u n c t i v e i n f o r m a t i o n . D a t a b a s e c o m p l e t i o n i s more p o w e r f u l t h a n a f i r s t o r d e r s y s t e m augmented by NAF. C l a r k shows t h a t t h e s t r u c t u r e o f a f a i l u r e p r o o f i s a l w a y s i s o m o r p h i c t o t h a t o f a f i r s t o r d e r p r o o f f r o m t h e c o m p l e t e d d a t a b a s e . C o n v e r s e l y , t h e c o m p l e t i o n o f t h e d a t a b a s e : DB = { P(a) } i s : C(DB) = { Yx.[P(x) <=> x=a] } f r o m w h i c h \/x. [ x ^ a Z) (x) ] f o l l o w s by f i r s t - o r d e r r e a s o n i n g . D a t a b a s e C o m p l e t i o n 13 F o r any p a r t i c u l a r x ^ a , NAF c a n show n P ( x ) , b u t t h e u n i v e r s a l summary i s beyond i t s c a p a b i l i t i e s . A n o t h e r a d v a n t a g e o f d a t a b a s e c o m p l e t i o n i s t h a t i t does n o t i n t r o d u c e i n c o n s i s t e n c i e s when a p p l i e d t o d a t a b a s e s c o n t a i n i n g i n c o m p l e t e i n f o r m a t i o n . The d a t a b a s e : BLOCK(A) V BLOCK (B) , w h i c h i s i n c o n s i s t e n t w i t h t h e CWA, c a n be r e w r i t t e n a s : V x . HBLOCK (A) A x=B D BLOCK (x) ] and: V x . HBLOCK (B) A x=A D BLOCK (x) ] From t h e s e , t h e c o n s i s t e n t c o m p l e t e d d a t a b a s e : \u00E2\u0080\u00A2 V x . [BLOCK (x) < = > HBLOCK (A) A x=B) V ( n B L O C K ( B ) A x=A) j c a n be d e r i v e d . N o t i c e t h a t t h e d i s j u n c t i o n i n t h e o r i g i n a l d a t a b a s e has become an \" e x c l u s i v e o r \" i n t h e c o m p l e t e d d a t a b a s e , w h i c h s t a t e s t h a t t h e r e i s e x a c t l y one b l o c k , and i t must be e i t h e r A o r B. T h e s e t e c h n i q u e s do n o t a v o i d a l l o f t h e p r o b l e m s o f NAF s i m p l y b e c a u s e a l l o f t h e d e d u c t i o n s a r e f i r s t o r d e r . T h e r e w i l l s t i l l be p r o p o s i t i o n s w h i c h a r e u n d e c i d a b l e i n t h e c o m p l e t e d d a t a b a s e , p r o p o s i t i o n s c o r r e s p o n d i n g t o t h o s e f o r w h i c h t h e e x h a u s t i v e s e a r c h f o r a f a i l u r e p r o o f n e v e r t e r m i n a t e s . 2.3 C i r c u m s c r i p t i o n M c C a r t h y (1980) has p r o p o s e d a r u l e o f c o n j e c t u r e c a l l e d \" p r e d i c a t e c i r c u m s c r i p t i o n \" . T h i s r u l e a l l o w s e x p l i c i t C i r c u m s c r i p t i o n 14 c o m p l e t e n e s s a s s u m p t i o n s , s i m i l a r t o C l a r k ' s c o m p l e t i o n a x i o m s , t o be d e r i v e d as t h e y a r e r e q u i r e d . The f o r m a l m e c h a n i c s o f c i r c u m s c r i p t i o n a r e beyond t h e s c o p e o f t h i s d i s c u s s i o n . E s s e n t i a l l y , however, c i r c u m s c r i p t i o n p r o v i d e s a means f o r c l o s i n g o f f t h e w o r l d w i t h r e s p e c t t o a p a r t i c u l a r p r e d i c a t e a t a p a r t i c u l a r t i m e . A schema f o r a s e t o f f i r s t o r d e r s e n t e n c e s i s g e n e r a t e d . T h i s schema i s t h e n i n s t a n t i a t e d by s u b s t i t u t i n g a r b i t r a r y p r e d i c a t e s f o r t h e p r e d i c a t e v a r i a b l e s i t c o n t a i n s . The p a r t i c u l a r s u b s t i t u t i o n ( s ) c h o s e n d e t e r m i n e w h i c h i n d i v i d u a l s a r e c o n j e c t u r e d t o be t h e e n t i r e e x t e n s i o n o f t h e p r e d i c a t e b e i n g c i r c u m s c r i b e d . M c C a r t h y c o n s i d e r s t h e b l o c k s - w o r l d example, d i s c u s s e d p r e v i o u s l y , i n w h i c h a l l t h a t i s known i s : BLOCK(A) V BLOCK(B) 6 (1) I f t h e p r e d i c a t e v a r i a b l e , 0, i n t h e c i r c u m s c r i p t i o n o f ( 1 ) : [9(A) V \u00C2\u00A9 ( B ) ] AVx.[\u00C2\u00A9(x) => BLOCK (x) ] => V*. [BLOCK (x) => 9 ( x ) ] i s r e p l a c e d s u c c e s s i v e l y by t h e p r e d i c a t e s (2) and ( 3 ) : c a n be d e r i v e d . As d i d t h e c o m p l e t e d d a t a b a s e , (4) s a y s t h a t t h e r e i s o n l y one b l o c k : A o r B. A g a i n , t h e c o n j e c t u r e c l o s e s t h e w o r l d and p u t s t h e \" e x c l u s i v e \" i n t e r p r e t a t i o n on t h e o r i g i n a l d i s j u n c t i o n . The c h o i c e o f s u b s t i t u e n d s v i t a l l y d e t e r m i n e s what c a n be R e c a l l t h a t t h i s d a t a b a s e i s NOT c o n s i s t e n t w i t h t h e CWA. x=A x=B (2) (3) t h e c o n j e c t u r e : Vx.[BLOCK(x) D x=A] V V*.[BLOCK(x) Z) x=B] (4) C i r c u m s c r i p t i o n 15 o b t a i n e d f r o m t h e c i r c u m s c r i p t i o n p r o c e s s . I t i s n o t c l e a r , i n g e n e r a l , how t h e s e s u b s t i t u e n d s a r e t o be c h o s e n . M c C a r t h y s u g g e s t s t h a t t h e d e s i r e d g o a l d i r e c t s t h e c h o i c e o f a p p r o p r i a t e s u b s t i t u t i o n s . I t r e m a i n s t o be s e e n whether t h i s i s c o r r e c t . I t i s e a s y t o s e e t h a t C i r c u m s c r i p t i o n subsumes NAF ( i n a l l o f i t s f o r m s ) . M c C a r t h y shows t h a t i t c a n d e r i v e t h e i n d u c t i o n a xiom f o r a r i t h m e t i c , w h i c h s u g g e s t s t h a t i t i s more p o w e r f u l t h a n d a t a b a s e c o m p l e t i o n . A l l o f t h e i d e a s d i s c u s s e d so f a r have p r o v i d e d ways o f becoming more \" c l o s e d - m i n d e d \" . E a c h f u n c t i o n s by r e s t r i c t i n g t h e s e t o f m o d e l s f o r t h e g i v e n a x i o m s . The g o a l has been t o a l l o w o n l y m i n i m a l m o dels ( D a v i s 1 9 8 0 ) , i n w h i c h o n l y a m i n i m a l s e t o f p r e d i c a t e i n s t a n c e s n e c e s s a r y t o s a t i s f y t h e axioms i s a l l o w e d t o be t r u e . The c o m p l e m e n t a r y a p p r o a c h a l s o i n v o l v e s r e s t r i c t i n g t h e s e t o f m o d e ls c o n s i d e r e d . R a t h e r t h a n f o c u s s i n g on m i n i m a l i t y , t h e s y s t e m s d i s c u s s e d i n t h e s e q u e l p r o v i d e more f l e x i b i l i t y i n d e t e r m i n i n g w h i c h m o dels a r e c o n s i d e r e d \" i n t e r e s t i n g \" . 2.4 D e f a u l t L o g i c I n t h e f o l l o w i n g , D e f a u l t L o g i c ( R e i t e r 1980, 1981) i s s u r v e y e d i n more d e t a i l t h a n t h o s e p a r a d i g m s a l r e a d y d i s c u s s e d . T h i s i s n e c e s s a r y b o t h t o f a m i l i a r i z e t h e r e a d e r w i t h t h e c o n c e p t s and n o t a t i o n r e q u i r e d t o u n d e r s t a n d t h e r e s u l t s i n D e f a u l t L o g i c 16 C h a p t e r 3, and t o p l a c e t h o s e r e s u l t s i n p e r s p e c t i v e . 2.4.1 D e f a u l t T h e o r i e s D e f a u l t L o g i c i s based on a f i r s t o r d e r l a n g u a g e , L A , c o n s i s t i n g o f the f i r s t o r d e r w e l l - f o r m e d f o r m u l a e ( w f f s ) formed from an a l p h a b e t , A, c o n s i s t i n g o f c o u n t a b l y many v a r i a b l e s : x, y, z, x-^, f u n c t i o n l e t t e r s : a, b, c, and p r e d i c a t e symbols: P, Q, R, ...; t o g e t h e r w i t h the u s u a l p u n c t u a t i o n s i g n s ; l o g i c a l c o n n e c t i v e s : i ( n o t ) , A ( a n d ) , V ( o r ) , ~Z) ( i m p l i e s ) ; and q u a n t i f i e r s : V x ( f o r a l l x ) , 3X ( t h e r e e x i s t s an x) . A w f f c o n t a i n i n g no f r e e v a r i a b l e s i s s a i d t o be c l o s e d . G i v e n an a r b i t r a r y s e t o f w f f s , S, t h e l o g i c a l c l o s u r e o f S, T h L ( S ) , i s d e f i n e d a s : T h L ( S ) = {w| w 6 L, w i s c l o s e d , S \- w}. 7 A d e f a u l t i s any e x p r e s s i o n o f the form: A ( x ) : B1 (x) , . . . , B m ( x ) 8 w(x) where A ( x ) , B ^ ( x ) , and w ( x ) a r e a l l w f f s whose f r e e v a r i a b l e s a r e among t h o s e i n x = x^, ..., x n . A , B ^ , and w a r e c a l l e d t h e When the a l p h a b e t and/or l a n g u a g e a r e c l e a r from c o n t e x t , t h e s u b s c r i p t s on L A and T h L ( S ) w i l l be o m i t t e d . o T h i s n o t a t i o n d i f f e r s from R e i t e r ' s i n the o m i s s i o n o f t h e \"M\" p r e c e e d i n g each o f t h e B^'s. S i n c e t h e y a r e i m p l i c i t i n t h e p o s i t i o n a l n o t a t i o n , t h e y have been o m i t t e d as a n o t a t i o n a l c o n v e n i e n c e . D e f a u l t T h e o r i e s 17 p r e r e q u i s i t e , j u s t i f i c a t i o n s , and c o n s e q u e n t o f t h e d e f a u l t , r e s p e c t i v e l y . I f none o f A, B^, and w c o n t a i n f r e e v a r i a b l e s , t h e d e f a u l t i s s a i d t o be c l o s e d . I f t h e p r e r e q u i s i t e i s empty, i t may t a k e n t o be any t a u t o l o g o u s p r o p o s i t i o n . Two c l a s s e s o f d e f a u l t s h a v i n g o n l y a s i n g l e j u s t i f i c a t i o n , B ( x ) , a r e d i s t i n g u i s h e d . T h o s e w i t h B(x) = w(x), a r e s a i d t o be n o r m a l , w h i l e t h o s e w i t h B(x) = w(x) A C (x) , f o r some C ( x ) , a r e c a l l e d s e m i - n o r m a l . A d e f a u l t t h e o r y , A, i s an o r d e r e d p a i r , (D,W). D i s a s e t o f d e f a u l t s ; W i s a s e t o f f i r s t o r d e r f o r m u l a e . I f a l l o f t h e d e f a u l t s i n D a r e n o r m a l o r s e m i - n o r m a l , A i s s a i d t o be a n o r m a l o r s e m i - n o r m a l d e f a u l t t h e o r y , r e s p e c t i v e l y . I f e a c h d e f a u l t o f D i s c l o s e d , A i s a c l o s e d d e f a u l t t h e o r y . D e f a u l t s s e r v e as r u l e s o f i n f e r e n c e o r c o n j e c t u r e , a u g m e n t i n g t h o s e n o r m a l l y p r o v i d e d by f i r s t - o r d e r l o g i c . Under c e r t a i n c o n d i t i o n s , t h e y s a n c t i o n i n f e r e n c e s w h i c h c o u l d n o t be made w i t h i n a s t r i c t l y f i r s t - o r d e r framework. I f t h e i r p r e r e q u i s i t e s a r e known and t h e i r j u s t i f i c a t i o n s a r e \" c o n s i s t e n t \" (^e t h e i r n e g a t i o n s a r e n o t p r o v a b l e ) , t h e n t h e i r c o n s e q u e n t s c a n be i n f e r r e d . Thus t h e t e r m \" j u s t i f i c a t i o n \" i s s e e n t o be somewhat m i s l e a d i n g , s i n c e j u s t i f i c a t i o n s need n o t be known, m e r e l y c o n s i s t e n t . 9 The c o n s e q u e n t ' s s t a t u s i s a k i n t o t h a t o f a b e l i e f , s u b j e c t t o r e v i s i o n s h o u l d t h e j u s t i f i c a t i o n s be d e n i e d a t some f u t u r e t i m e . I t i s t h i s c h a r a c t e r i s t i c w h i c h i n d u c e s t h e n o n - m o n o t o n i c b e h a v i o r o f d e f a u l t s . I n a modal l o g i c w i t h t h e o p e r a t o r K (know) t h e j u s t i f i c a t i o n s Bj_ m i g h t a p p e a r as -iK-tBj. D e f a u l t T h e o r i e s 18 D e f a u l t r u l e s c a n be s e e n t o have a g r e a t d e a l i n common w i t h many p r e v i o u s l y m e n t i o n e d a p p r o a c h e s . F o r example, t h e C l o s e d W o r l d A s s u m p t i o n s t a t e s : I f Y w i n f e r j- n w w h i c h c a n be r e p r e s e n t e d i n D e f a u l t L o g i c by: : - i w (1) I n f a c t , (1) w i l l l a t e r be r e f e r r e d t o as t h e \" C l o s e d W o r l d \" d e f a u l t . The DEFAULT a s s i g n m e n t s w h i c h c a n be a t t a c h e d t o frame s l o t s i n KRL (Bobrow and W i n o g r a d 1977) a l s o a p pear t o be r e l a t e d . KRL p r o v i d e s a mechanism f o r o b t a i n i n g a v a l u e f o r a s l o t i n t h e a b s e n c e o f a \" b e t t e r \" v a l u e . A KRL d e f a u l t v a l u e , d , f o r a s l o t , s, i n a frame i n s t a n c e , f , c a n be v i e w e d a s : I f Y s ( f ) ^ d i n f e r |- s ( f ) = d o r , i n D e f a u l t L o g i c , a s : :s (f )=d s ( f ) = d S i m i l a r mechanisms a r e a v a i l a b l e i n many o t h e r f r a m e - b a s e d knowledge r e p r e s e n t a t i o n schemes (Minsky 1 9 7 5 ) . A c l o s e l y r e l a t e d a p p r o a c h i s S a n d e w a l l ' s (1972) \" U n l e s s \" o p e r a t o r . \" U n l e s s ( P ) \" i s i n t e r p r e t e d as \"Y P \" i and \" U n l e s s \" t e r m s a r e a l l o w e d i n t h e c o n s t r u c t i o n o f w f f s , w i t h r e s u l t s l i k e : A A U n l e s s (B) D C w h i c h c o r r e s p o n d r o u g h l y t o : A : -iB C \" U n l e s s \" was o r i g i n a l l y p r o p o s e d as a s o l u t i o n t o t h e frame p r o b l e m . R a t h e r t h a n h a v i n g t o have e x p l i c i t axioms s t a t i n g D e f a u l t T h e o r i e s 19 t h a t t h e p r o p e r t i e s o f o b j e c t s r e m a i n e d i n v a r i a n t f r o m s i t u a t i o n t o s i t u a t i o n u n l e s s e x p l i c i t l y c h a n g e d , S a n d e w a l l s u g g e s t e d t h a t t h e s e \" f r a me axioms\" be r e p l a c e d by a frame i n f e r e n c e r u l e l i k e : I S ( o b j e c t , p r o p e r t y , s i t u a t i o n ) U n l e s s ( E N D S ( o b j e c t , p r o p e r t y , S u c c e s s o r ( s i t u a t i o n , a c t ) ) ) I S ( o b j e c t , p r o p e r t y , S u c c e s s o r ( s i t u a t i o n , a c t ) ) w h i c h c a n be i n t e r p r e t e d : I f an o b j e c t has a p r o p e r t y i n a s i t u a t i o n , i t c a n be c o n c l u d e d t o r e t a i n t h a t p r o p e r t y i n t h e s u c c e s s o r s i t u a t i o n r e s u l t i n g f r o m p e r f o r m i n g ' a c t 1 , u n l e s s i t c a n be shown o t h e r w i s e . No f o r m a t i o n r u l e s were p r o v i d e d f o r \" U n l e s s \" , however, so q u e s t i o n a b l e f o r m u l a e s u c h a s : A D U n l e s s ( B ) c a n be c o n s t r u c t e d . The s e m a n t i c s o f s u c h f o r m u l a e a r e , a t b e s t , d i f f i c u l t t o d e t e r m i n e . S a n d e w a l l a l s o f a i l s t o p r o v i d e any f o r m a l u n d e r s t a n d i n g o f t h e i m p a c t o f t h e \" U n l e s s \" r u l e on t h e u n d e r l y i n g l o g i c . D e f a u l t L o g i c h a s , t o some e x t e n t , r e m e d i e d t h e s e s h o r t c o m i n g s . 2.4.2 C l o s e d D e f a u l t T h e o r i e s and T h e i r E x t e n s i o n s R e i t e r (1980) d e s c r i b e s t h e e x t e n s i o n s o f a d e f a u l t t h e o r y , A= (D,W), as b e i n g \" a c c e p t a b l e s e t s o f b e l i e f s t h a t one may h o l d a b o u t an i n c o m p l e t e l y s p e c i f i e d w o r l d , W\". D i s v i e w e d as e x t e n d i n g t h e f i r s t o r d e r knowledge o f W i n o r d e r t o p r o v i d e i n f o r m a t i o n n o t d e r i v a b l e f r o m W. An e x t e n s i o n , E , f o r A i s r e q u i r e d t o have t h e f o l l o w i n g C l o s e d D e f a u l t T h e o r i e s and T h e i r E x t e n s i o n s 20 p r o p e r t i e s : W C E (1) T h L ( E ) = E (2) A : B l f . . . f B m (3) F o r e a c h d e f a u l t , \u00E2\u0080\u0094 6 D, i f A 6 E , and n B ^ , . . . , ^ m 0 E t h e n w \u00E2\u0082\u00AC E . T h e s e p r o p e r t i e s s t a t e t h a t E must c o n t a i n a l l t h e known f a c t s , t h a t E must be c l o s e d under t h e |- r e l a t i o n , and t h a t t h e c o n s e q u e n t o f any d e f a u l t whose p r e r e q u i s i t e i s s a t i s f i e d by E , and whose j u s t i f i c a t i o n s a r e c o n s i s t e n t w i t h E , must a l s o be i n E . R e i t e r d e f i n e s an e x t e n s i o n f o r a c l o s e d d e f a u l t t h e o r y t o be a m i n i m a l f i x e d p o i n t o f an o p e r a t o r h a v i n g t h e above c h a r a c t e r i s t i c s . The e x t e n s i o n s o f a d e f a u l t t h e o r y s e l e c t a r e s t r i c t e d s u b s e t o f t h e m o d e ls o f t h e u n d e r l y i n g f i r s t - o r d e r t h e o r y , W. Any m odel f o r an e x t e n s i o n o f A w i l l a l s o be a model f o r W, b u t t h e c o n v e r s e i s g e n e r a l l y n o t t r u e . T h e r e i s an i t e r a t i v e mechanism f o r v e r i f y i n g an e x t e n s i o n . The method i s , u n f o r t u n a t e l y , n o t s u i t a b l e f o r c o n s t r u c t i n g e x t e n s i o n s . T h i s i s b e c a u s e an o r a c l e i s r e q u i r e d w h i c h c a n d e c i d e whether a w f f ' s n e g a t i o n i s i n t h e g i v e n e x t e n s i o n . The t h e o r e m o u t l i n i n g t h e mechanism i s q u o t e d below, b o t h t o p r o v i d e a b e t t e r i n t u i t i o n a b o u t e x t e n s i o n s and b e c a u s e i t w i l l be drawn on s e v e r a l t i m e s i n C h a p t e r 3. N o t e t h e e x p l i c i t r e f e r e n c e t o E i n t h e d e f i n i t i o n o f E ^ + - i _ . Theorem ( R e i t e r 1980) L e t A = (D,W) be a c l o s e d d e f a u l t t h e o r y , and E be and a r b i t r a r y Closed Default Theories and Their Extensions 21 set of formulae. Define: and, for i > 0: E i + 1 = T h ( E i > u A B 1' \u00E2\u0080\u00A2 \u00E2\u0080\u00A2 \u00E2\u0080\u00A2 i 'm 6 D, A 6 E i f n B x i \u00E2\u0080\u00A2 \u00E2\u0080\u00A2 \u00C2\u00AB / - i B m 0 E} CO Then E i s an extension for A i f f E = U E^. i=0 Default theories need not always have extensions, even when W i s consistent. There are, however, certa i n classes of theories for which the existence of at least one extension i s guaranteed. Normal theories have been shown to always have extensions, and i t appears that t h i s i s also true for c e r t a i n classes of semi-normal theories (see Chapter 4 for a discussion). Some examples of defaults were presented in the preceeding section. The following example i l l u s t r a t e s the extensions induced by the closed world default on the theory: W = { BLOCK(A) V BLOCK(B) }. The closed world default i s r e a l l y a default schema which i s applicable to any p o s i t i v e ground l i t e r a l . In t h i s case, i t results in the following set of normal defaults: D = ( : - i B L O C K (A) : - i B L O C K ( B ) \ . 1 ^LOCK(A) n B L O C K ( B ) ' The theory, (D,W), has two extensions, E^ and E2. E1 = Th({TBLOCK(A), BLOCK(B)}) E 2 = Th({BLOCK(A), n B L O C K ( B ) } ) Note that E = Th({BLOCK(A), BLOCK(B)}) i s not an extension. Like database completion and Circumscription, the closed world C l o s e d D e f a u l t T h e o r i e s and T h e i r E x t e n s i o n s 22 d e f a u l t g i v e s t h e e x c l u s i v e i n t e r p r e t a t i o n o f d i s j u n c t i o n s t o w h i c h i t i s a p p l i e d . I n t u i t i v e l y , t h i s i s b e c a u s e t h e d e f a u l t s f o r c e as many t h i n g s t o be f a l s e as p o s s i b l e , r e s u l t i n g i n e x t e n s i o n s whose models may be m i n i m a l m o dels f o r W. More p r e c i s e l y , E i s n o t an e x t e n s i o n b e c a u s e i t v i o l a t e s t h e m i n i m a l i t y c o n d i t i o n o f t h e d e f i n i t i o n o f e x t e n s i o n s . (Were W a l s o t o c o n t a i n b o t h BLOCK(A) and BLOCK(B), E w o u l d be t h e o n l y e x t e n s i o n . ) N o t i c e how t h e e x t e n s i o n s E ^ and E 2 m a n i f e s t W*s i n c o n s i s t e n c y w i t h t h e CWA. The i n c o n s i s t e n t a s s i g n m e n t s f o r BLOCK(A) and BLOCK(B) a r e s t i l l o b t a i n a b l e , b u t t h e y a r e s e p a r a t e d i n t o o r t h o g o n a l , s e l f - c o n s i s t e n t e x t e n s i o n s . I n f a c t , R e i t e r has shown t h a t t h e e x t e n s i o n s o f any d e f a u l t t h e o r y w i l l a l w a y s be s e l f - c o n s i s t e n t p r o v i d e d t h a t t h e f i r s t - o r d e r t h e o r y W i s c o n s i s t e n t , and t h a t a l l t h e e x t e n s i o n s o f a n o r m a l d e f a u l t t h e o r y w i l l be m u t u a l l y i n c o n s i s t e n t . R e i t e r g i v e s a p r o o f p r o c e d u r e a p p l i c a b l e t o n o r m a l t h e o r i e s , b u t no means o f d e t e r m i n i n g t h e e x t e n s i o n s o f n o n - n o r m a l t h e o r i e s has h e r e t o f o r e been p r e s e n t e d . Such a mechanism, a p p l i c a b l e t o a r b i t r a r y f i n i t e t h e o r i e s , i s p r e s e n t e d i n C h a p t e r 3. 2.4.3 G e n e r a l D e f a u l t T h e o r i e s I n c o n t r a s t t o c l o s e d d e f a u l t s , an open d e f a u l t i s one i n w h i c h a t l e a s t one o f A ( x ) , B^ (x) , o r w(x) c o n t a i n f r e e G e n e r a l D e f a u l t T h e o r i e s 23 v a r i a b l e s i n x. R e i t e r (1980) d e f i n e s t h e e x t e n s i o n s o f an a r b i t r a r y d e f a u l t t h e o r y as f o l l o w s : 1) The S k o l e m i z e d f o rm o f a d e f a u l t , 6, i s o b t a i n e d by r e p l a c i n g t h e c o n s e q u e n t o f o w i t h i t s S k o l e m i z e d form ( R o b i n s o n 1965).. 2) A d e f a u l t t h e o r y , A = (D,W), i s S k o l e m i z e d i f a l l d e f a u l t s i n D and a l l w f f s i n W a r e i n S k o l e m i z e d form. 3) I f A = (D,W) i s a S k o l e m i z e d d e f a u l t t h e o r y , i i s t h e s e t o f Skolem f u n c t i o n s o f A, and F i s t h e s e t o f f u n c t i o n l e t t e r s o f t h e a l p h a b e t , A, t h e n CLOSED-DEFAULTS (A) i s d e f i n e d a s : {ci(g) | d{x) 6 D, g 6 H (F U J.) i s a ground t u p l e } where H r e p r e s e n t s t h e H e r b r a n d U n i v e r s e . 4) E i s an e x t e n s i o n f o r a S k o l e m i z e d d e f a u l t t h e o r y , A, i f f E i s an e x t e n s i o n f o r t h e t h e o r y (CLOSED-DEFAULTS (A) ,W) . An open d e f a u l t i s i n t e r p r e t e d as s t a n d i n g f o r t h e s e t o f c l o s e d d e f a u l t s o b t a i n a b l e by r e p l a c i n g i t s f r e e v a r i a b l e s by g round t e r m s . H(F U S ) w i l l g e n e r a l l y be c o u n t a b l y i n f i n i t e , making (CLOSED-DEFAULTS (A) ,W) a d e f a u l t t h e o r y w i t h an i n f i n i t e s e t o f d e f a u l t s . The r e p e r c u s s i o n s o f t h i s w i l l become a p p a r e n t i n C h a p t e r 3. Most i n t e r e s t i n g d e f a u l t t h e o r i e s a r e not c l o s e d . C o n s i d e r what, by now, must be t h e a r c h e t y p a l d e f a u l t t h e o r y : W = { N/x. P e n g u i n (x) Z) B i r d (x) , \/x. P e n g u i n (x) Z) n C a n - F l y (x) , Vx. D e a d - B i r d (x) Z) B i r d (x) , Vx. D e a d - B i r d (x)_ Z) -iCan-Fly(x) , \/x. O s t r i c h (x) Z) B i r d (x) , N/x. O s t r i c h ( x ) Z) - i C a n - F l y (x) , B i r d ( T w e e t y ) } D = I B i r d ( x ) : C a n - F l y ( x ) I 1 C a n - F l y (x) ' ' The d e f a u l t , which i s not c l o s e d , m i g h t be i n t e r p r e t e d as \" I f x i s a b i r d , and i t i s c o n s i s t e n t t h a t x can f l y , c o n c l u d e t h a t i t c a n \" . T h i s t h e o r y a l l o w s one t o c o n c l u d e , f o r an a r b i t r a r y b i r d G e n e r a l D e f a u l t T h e o r i e s 24 (eg T w e e t y ) , t h a t i t c a n f l y \u00E2\u0080\u0094 u n l e s s one i s t o l d t h a t i t c a n n o t , o r t h a t i t i s a p e n g u i n , an o s t r i c h , o r d e a d . The c o n c l u s i o n may l a t e r have t o be r e v o k e d s h o u l d T weety t u r n o u t t o be a- p e n g u i n , b u t common s e n s e seems t o s a n c t i o n t h e same c o n c l u s i o n . T h i s i s p a r t l y b e c a u s e p e o p l e t e n d t o assume t h a t t h e y have t h e r e l e v a n t i n f o r m a t i o n i n most s i t u a t i o n s ( c f l i n g u i s t s ' u s e o f G r i c e ' s C o n v e r s a t i o n a l I m p l i c a t u r e s [ G r i c e 1 9 7 5 ] : one o f t h e s e i s t h a t a l l i n f o r m a t i o n n e c e s s a r y t o i n t e r p r e t an u t t e r a n c e i s e x p e c t e d t o be c o n t a i n e d i n t h e u t t e r a n c e . ) 2.5 N o n - M o n o t o n i c L o g i c McDermott and D o y l e (1980, McDermott 1982) p r o p o s e a f o r m a l i s m c o m p l e m e n t a r y t o D e f a u l t L o g i c , w h i c h t h e y c a l l N o n - M o n o t o n i c L o g i c (NML). U n l i k e D e f a u l t L o g i c , w h i c h u s e s t h e n o t i o n o f c o n s i s t e n c y o n l y a t t h e \"meta\" l e v e l ( i n t h e i n f e r e n c e r u l e s ) , NML c e n t r e s a r o u n d t h e i n t r o d u c t i o n o f c o n s i s t e n c y i n t o t h e o b j e c t l a n g u a g e . I n t h e f i r s t i n c a r n a t i o n o f NML (McDermott and D o y l e 1 9 8 0 ) , a s t a n d a r d f i r s t - o r d e r l o g i c was augmented w i t h an \"M\" o p e r a t o r , r o u g h l y e q u i v a l e n t t o t h e f a m i l i a r \" J / V . The s e t o f theorems was d e f i n e d as t h e i n t e r s e c t i o n o f a l l o f t h e f i x e d p o i n t s o f an o p e r a t o r , NM. E s s e n t i a l l y , NM p r o d u c e s t h e l o g i c a l c l o s u r e o f t h e o r i g i n a l t h e o r y t o g e t h e r w i t h as many a s s e r t i o n s o f t h e f o r m Mq as p o s s i b l e . The s e t o f t h eorems c a n be c o n t r a s t e d w i t h t h e e x t e n s i o n s o f a d e f a u l t t h e o r y , e a c h o f N o n - M o n o t o n i c L o g i c 25 w h i c h i s a f i x e d p o i n t . T h i s i n d i c a t e s t h a t n o n - m o n o t o n i c theoremhood i s , i n some s e n s e , a more r e s t r i c t i v e c o n c e p t t h a n e x t e n s i o n membership. I n f a c t , t h e two a r e i n c o m p a r a b l e i n g e n e r a l . The agreement i n t u i t i v e l y e x p e c t e d c o n s i d e r i n g t h a t any d e f a u l t : \u00E2\u0080\u00A2 ' \u00E2\u0080\u00A2 \u00E2\u0080\u00A2 \u00E2\u0080\u00A2 f w c a n be a p p r o x i m a t e d i n NML by: A A MB]_ A A MB m D w o f t e n o c c u r s . T h e r e a r e , however, d e f a u l t t h e o r i e s w h i c h have e x t e n s i o n s even t h o u g h t h e c o r r e s p o n d i n g n o n - m o n o t o n i c t h e o r i e s have no f i x e d p o i n t s , and v i c e v e r s a (see [ R e i t e r 1980] f o r e x a m p l e s ) . D a v i s (1980) s u g g e s t s t h a t i t m i g h t be i m p o s s i b l e t o a s s i g n a r e a s o n a b l e s e m a n t i c s t o t h e M o p e r a t o r were i t i n c l u d e d i n t h e o b j e c t l a n g u a g e . T h i s and o t h e r p r o b l e m s l e d t o t h e r e c a s t i n g o f t h e t h e o r y i n terms o f a more c l a s s i c a l modal l o g i c (McDermott 1 9 8 2 ) . ^ The r e s u l t i n g n o n - m o n o t o n i c S5 i s u n f o r t u n a t e l y r e d u n d a n t , s i n c e i t i s no more p o w e r f u l t h a n S5. P r o o f s o f t h e c o n s i s t e n c y o f n o n - m o n o t o n i c T and S4 have n o t been p r e s e n t e d . Such p r o o f s a r e n e c e s s a r y f o r NML t o be s u c c e s s f u l . I n v e r s i o n I I o f NML, McDermott c o n s i d e r s t h e a d v a n t a g e s o f b e l i e v i n g f o r m u l a e o t h e r t h a n t h o s e i n t h e i n t e r s e c t i o n o f a l l t h e f i x e d p o i n t s . He p r o p o s e s a \" b r a v e r o b o t \" w h i c h would A d i s c u s s i o n o f modal l o g i c s i s beyond t h e s c o p e o f t h i s t h e s i s . See [Hughes and C r e s s w e l 1968] f o r an i n t r o d u c t i o n . N o n - M o n o t o n i c L o g i c 26 b e l i e v e a l l o f t h e f o r m u l a e o f a p a r t i c u l a r f i x e d p o i n t . Such an a p p r o a c h i s r e q u i r e d i n o r d e r t o p r o v i d e an i n t u i t i v e l y s a t i s f a c t o r y s e m a n t i c s f o r Mp: \"p i s c o n s i s t e n t w i t h what i s b e l i e v e d \" . The a v a i l a b i l i t y o f t h e \"M\" terms i n t h e l a n g u a g e has a d v a n t a g e s and d i s a d v a n t a g e s . F o r example, i t c a n be shown t h a t c o n s t r u c t s o f t h e f o r m : P D Mq where p and q a r e a r b i t r a r y f o r m u l a e , a r e e i t h e r r e d u n d a n t o r i n c o n s i s t e n t . ( T h i s f o l l o w s b e c a u s e t h e \" t h e o r e m s \" o f any NML t h e o r y must c o n t a i n a l l f o r m u l a e Mp w h i c h a r e n o t i n c o n s i s t e n t . ) Such c o n s t r u c t s c a n n o t be formed i n d e f a u l t l o g i c , b u t a r e r e a d i l y a v a i l a b l e i n NML (as t h e y a r e i n S a n d e w a l l ' s f o r m a l i s m ) . On t h e p o s i t i v e s i d e , t h e d e f a u l t r u l e s c a n be m a n i p u l a t e d by t h e t h e o r y . F o r example, i n t h e n o r m a l d e f a u l t t h e o r y w i t h no axioms and t h e d e f a u l t s : A : B , - i A : B B B n o t h i n g c a n be i n f e r r e d a b o u t B. The c o r r e s p o n d i n g non-m o n o t o n i c t h e o r y : { A A MB D B , n A A MB D B} i m p l i e s MB and MB 3 B, f r o m w h i c h B c a n be i n f e r r e d . T h i s a p p e a r s t o be more i n a c c o r d w i t h n o r m a l common s e n s e r e a s o n i n g . F i n a l l y , Lp <=> p i s a t h e s i s o f NML. W h i l e most modal l o g i c i a n s w o u l d a g r e e t h a t \"p i s n e c e s s a r i l y t r u e \" i m p l i e s \"p i s t r u e \" , t h e c o n v e r s e i s u s u a l l y n o t a c c e p t e d . Hughes and C r e s s w e l l (1968, p28) c o n c l u d e t h a t \"no i n t u i t i v e l y p l a u s i b l e m o dal s y s t e m \" would have s u c h a t h e s i s . T h i s i n d i c a t e s t h a t N o n - M o n o t o n i c L o g i c 27 t h e r e may be f u n d a m e n t a l p r o b l e m s w i t h NML. 2.6 C o n s i s t e n c y M a i n t e n a n c e A l l o f t h e p a r a d i g m s d i s c u s s e d i n t h i s c h a p t e r p r o v i d e means f o r j u m p i n g t o c o n c l u s i o n s . Jumping t o c o n c l u s i o n s c a n be a r i s k y p r o c e s s , s i n c e t h e r e i s an e v e r - p r e s e n t p o s s i b i l i t y o f r e f u t a t i o n . R e f u t a t i o n o f a c o n c l u s i o n a l r e a d y e n t e r e d i n t o t h e knowledge b a s e has c o n s e q u e n c e s beyond t h e s i m p l e d e l e t i o n o f t h e o f f e n d i n g f a c t . E v e r y o t h e r c o n c l u s i o n r e a c h e d on t h e b a s i s o f t h e r e j e c t e d f a c t must be s o u g h t o u t and i t s e l f r e j e c t e d . T h e s e r e j e c t i o n s may have r e p e r c u s s i o n s s c a t t e r e d t h r o u g h o u t t h e knowledge b a s e . The \" r e a s o n e r \" must e i t h e r remember t h e j u s t i f i c a t i o n s f o r e v e r y t h i n g i t \" b e l i e v e s \" and be a b l e t o u n r a v e l a f l a w e d web o f b e l i e f s , o r e l s e be p r e p a r e d t o throw e v e r y t h i n g away and s t a r t a g a i n f r o m f i r s t p r i n c i p l e s . The l a t t e r c o u r s e i s c l e a r l y i m p r a c t i c a l , b u t t h e f o r m e r i s by no means t r i v i a l . F o r example, a l t h o u g h t h e j u s t i f i c a t i o n s w h i c h were u s e d f o r d e r i v i n g a p a r t i c u l a r f a c t may have been i n v a l i d a t e d , t h e r e may be i n d e p e n d e n t j u s t i f i c a t i o n s w h i c h r e m a i n \u00E2\u0080\u00A2 v a l i d . To r e v o k e t h e f a c t m i g h t r e c u r s i v e l y f o r c e t h e r e v o k i n g o f a l a r g e body o f i n f o r m a t i o n w h i c h w i l l l a t e r have t o be r e d e r i v e d . Many \" b e l i e f r e v i s i o n \" s y s t e m s h ave been d e s i g n e d t o s t u d y t h e p r o b l e m s o f c h a n g i n g m o d els o f s i t u a t i o n s . D o y l e (1979) and M c A l l e s t e r (1978, 1980) p r e s e n t s u r v e y s o f t h e p r o b l e m s w h i c h must be d e a l t C o n s i s t e n c y M a i n t e n a n c e 28 w i t h , and some s u g g e s t e d a p p r o a c h e s . A d i s c u s s i o n o f s u c h t e c h n i q u e s i s o u t s i d e t h e i n t e n d e d s c o p e o f t h i s t h e s i s , b u t i t s h o u l d be n o t e d t h a t t h e s e i s s u e s a r e r e a l and must be d e a l t w i t h i f any o f t h e m a t e r i a l d i s c u s s e d h e r e i n i s t o be p r a c t i c a l l y a p p l i c a b l e . 2.7 S e m a n t i c N e t w o r k s Type o r IS-A h i e r a r c h i e s a r e e x t r e m e l y common i n A I . I n t h e i r s i m p l e s t f o r m , t h e y c o r r e s p o n d t o l o g i c a l s t r u c t u r e s c o n s i s t i n g o f g r o u n d l i t e r a l s and s i m p l e , u n i v e r s a l l y q u a n t i f i e d , i m p l i c a t i o n s o f t h e f o r m \/x.. [A (x) D B (x) ] where A and B a r e monadic p r e d i c a t e s . \" I n f e r e n c i n g \" d e g e n e r a t e s t o p a t h f o l l o w i n g ( c o m p u t i n g t h e t r a n s i t i v e c l o s u r e o f a c h a i n o f i m p l i c a t i o n s ) , w i t h n e g a t i o n a c h i e v e d by f a i l u r e p r o o f s . The l o g i c a l e q u i v a l e n t o f s u c h n e t w o r k s a r e d e f i n i t e d a t a b a s e s . ^ D e f i n i t e d a t a b a s e s a r e n e c e s s a r i l y c o n s i s t e n t w i t h t h e CWA, so t h e s e m a n t i c s o f s u c h n e t w o r k s c a n be c l e a r l y l a i d o u t . I n t h e l i g h t o f t h e common need t o d e a l w i t h p r o t o t y p i c d e s c r i p t i o n s , i t i s w o r t h c o n s i d e r i n g whether s e m a n t i c n e t w o r k s c a n d e a l w i t h e x c e p t i o n s . S i m p l y i n c o r p o r a t i n g e x c e p t i o n s i n t o t h e s t r u c t u r e d e s c r i b e d a b ove, as i s f r e q u e n t l y done, means t h a t a d i f f e r e n t s e m a n t i c s must be p r o v i d e d . O t h e r w i s e , t h e r e s u l t i n g s t r u c t u r e s would be i n c o n s i s t e n t . T r a d i t i o n a l l y , A d e f i n i t e d a t a b a s e i s a Horn d a t a b a s e i n w h i c h each c l a u s e has EXACTLY one p o s i t i v e l i t e r a l . S e m a n t i c N e t w o r k s 29 n e t w o r k e r s have c i r c u m v e n t e d t h i s p r o b l e m by a l l o w i n g i n c o n s i s t e n t i n f o r m a t i o n b u t u s i n g an i n c o m p l e t e i n f e r e n c e s y s t e m i n c a p a b l e o f d e t e c t i n g t h e i n c o n s i s t e n c i e s . C o n f l i c t s a r e t h u s r e s o l v e d by g i v i n g p r e f e r e n c e t o w h a t e v e r c a n be d e r i v e d v i a t h e s h o r t e s t c h a i n o f i n f e r e n c e s . Not o n l y i s i t d i f f i c u l t t o d e t e r m i n e t h e s e m a n t i c s o f s u c h an i n f e r e n c e s y s t e m , b u t t h e r e s u l t s a r e sometimes c o u n t e r - i n t u i t i v e . F o r example, a d d i n g a l i n k w h i c h summarizes a c h a i n ( p e r h a p s t o i m p r o v e e f f i c i e n c y ) m i g h t c o m p l e t e l y change t h e p a t h l e n g t h s and h e n c e what c a n be d e r i v e d f r o m t h e n e t w o r k . NETL (Fahlman 1979, Fahlman e t a l 1 9 8 1 ) , a s y s t e m d e s i g n e d t o a l l o w t h e c o n s t r u c t i o n o f l a r g e - s c a l e IS-A h i e r a r c h i e s w i t h e x c e p t i o n s (MIGHT-BE-A h i e r a r c h i e s ) , a d d r e s s e s t h i s p r o b l e m by m aking e x c e p t i o n s e x p l i c i t i n t h e network s t r u c t u r e . NETL i s i n t e n d e d t o be a m a s s i v e l y p a r a l l e l a r c h i t e c t u r e , w i t h one p r o c e s s o r a s s i g n e d t o e a c h node o f t h e s e m a n t i c n etwork i t r e p r e s e n t s . T h r e e o f NETL's l i n k t y p e s a r e r e l e v a n t t o t h i s d i s c u s s i o n : 1) VC \u00E2\u0080\u0094 c o r r e s p o n d s t o t h e n o r m a l ISA l i n k , e x c e p t t h a t e x c e p t i o n s ( i n d i c a t e d by CANCEL l i n k s ) a r e a l l o w e d w h i c h may d i s r u p t t h e n o r m a l i n h e r i t a n c e s t r u c t u r e s . R e p r e s e n t e d g r a p h i c a l l y by: >. 2) CANCEL \u00E2\u0080\u0094 c a n c e l s i n h e r i t a n c e by t h e t a i l node and a l l \" l o w e r \" nodes o f p r o p e r t i e s a s s o c i a t e d w i t h t h e h ead node and a l l \" h i g h e r \" n o d e s . R e p r e s e n t e d by: -\-\-\-> \u00E2\u0080\u00A2 3) UNCANCEL - undoes t h e e f f e c t o f t h e CANCEL l i n k a t i t s h e a d . The node a t t h e t a i l and i t s d e s c e n d a n t s w i l l i n h e r i t as t h o u g h t h e CANCEL l i n k were n o t t h e r e . R e p r e s e n t e d by: >. S e m a n t i c N e t w o r k s 30 NETL g r a p h s c a n be mapped i n t o monadic s e m i - n o r m a l d e f a u l t t h e o r i e s ( t h e o r i e s i n v o l v i n g o n l y m o n a d i c p r e d i c a t e s ) , as f o l l o w s : VC l i n k s become n o r m a l d e f a u l t s : A > B becomes A(x) : B ( x ) . B(x) CANCEL and UNCANCEL l i n k s combine t o p r o d u c e s e m i - n o r m a l d e f a u l t s . A CANCEL l i n k f r o m A t o B on w h i c h UNCANCEL l i n k s i m p i n g e f r o m C-i_, ... , C n (n > 0) becomes: A(x) : iB(x) A n C]_(x) A \u00E2\u0080\u00A2\u00E2\u0080\u00A2\u00E2\u0080\u00A2 \"\u00C2\u00BBC n (x) - i B ( x ) A c t i v a t i o n o f a node c o r r e s p o n d s t o a s s e r t i n g a g r o u n d i n s t a n c e o f t h a t node. T h e s e t h r e e l i n k s a l l o w t h e c o n s t r u c t i o n o f complex s t r u c t -u r e s . F o r example, F i g u r e 2.1 d i a g r a m s t h e NETL s t r u c t u r e and c o r r e s p o n d i n g d e f a u l t t h e o r y f o r t h e f o l l o w i n g (Fahlman e t a l 1 9 8 1 ) : A m o l l u s c i s a s h e l l - b e a r e r . C e p h a l o p o d s a r e m o l l u s c s w h i c h a r e n o t s h e l l - b e a r e r s . A n a u t i l u s i s a c e p h a l o p o d , b u t _is a s h e l l - b e a r e r . S h e l l - b e a r e r M o l l u s c C e p h a l o p o d N a u t i l u s F i g u r e 2.1a \u00E2\u0080\u0094 A t y p i c a l NETL example. T h i s f i g u r e d e m o n s t r a t e s t h a t c o n n e c t i o n s c a n become r a t h e r c omplex i n n a t u r a l l y o c c u r r i n g s i t u a t i o n s . I t t u r n s o u t t h a t i n h e r i t a n c e (or i n f e r e n c e ) i n NETL doe s n o t have t h e s t r a i g h t -f o r w a r d s e m a n t i c s one m i g h t e x p e c t . F o r example, i n F i g u r e S e m a n t i c N e t w o r k s 31 M o l l u s c ( x ) : S h e l l - b e a r e r ( x ) , C e p h a l o p o d ( x ) ; M o l l u s c ( x ) S h e l l - b e a r e r ( x ) M o l l u s c ( x ) N a u t i l u s ( x ) ; C e p h a l o p o d ( x ) , N a u t i l u s ( x ) : S h e l l - b e a r e r ( x ) C e p h a l o p o d ( x ) S h e l l - b e a r e r ( x ) C e p h a l o p o d (x) ; - i S h e l l - b e a r e r (x) A n N a u t i l u s (x) ^ h e l l - b e a r e r (x) F i g u r e 2.1b \u00E2\u0080\u0094 D e f a u l t t h e o r y f o r F i g u r e 2.1a. 2.2a, i t i s u n c l e a r t o NETL whether o r n o t A s h o u l d i n h e r i t f r o m E . B F i g u r e 2.2a \u00E2\u0080\u0094 A p r o b l e m a t i c c a s e . A ( x ) : B (x) , A ( x ) ; C (x) , B (x) ; D (x) B(x) C ( x ) D(x) C (x) : D (x) , D (x) ; E (x) , C (x) ; i E ( x ) D(x) E ( x ) -iE{x) F i g u r e 2.2b \u00E2\u0080\u0094 D e f a u l t t h e o r y f o r F i g u r e 2.2a. T h i s i s b e c a u s e one p a t h (A, B, D, E) i n d i c a t e s \" y e s \" and t h e o t h e r (A, C, E) \"no\", b e c a u s e o f t h e CANCEL l i n k f r o m C t o E . W h i l e t h e f o r m e r i n t e r p r e t a t i o n may seem p r e f e r a b l e , s i n c e t h e r e i s a p a t h i n v o l v i n g no c a n c e l l i n k s , t h e p a r a l l e l n a t u r e o f NETL f o r c e s t h e l a t t e r c h o i c e . S i n c e t h i s i s somewhat c o u n t e r i n t u i t i v e , s u c h s t r u c t u r e s a r e now d e c l a r e d ' i l l - f o r m e d ' and t h e u s e r must e x p l i c i t l y r e s o l v e t h e a m b i g u i t y . The s o u r c e o f t h e p r o b l e m becomes a p p a r e n t when t h e c o r r e s p o n d i n g d e f a u l t t h e o r y ( F i g u r e 2.2b) i s c o n s i d e r e d . T h i s t h e o r y has two e x t e n s i o n s , c o n t a i n i n g E and -,E r e s p e c t i v e l y . S e m a n t i c N e t w o r k s 32 Such d i f f i c u l t i e s h i g h l i g h t t h e need f o r a sound t h e o r e t i c a l b a s i s f o r s y s t e m s w h i c h a r e i n t e n d e d t o r e p r e s e n t and use knowledge. D e f a u l t L o g i c may p r o v i d e a s u i t a b l e v e h i c l e f o r t h i s work. C h a p t e r 4 s u r v e y s t h i s p r o b l e m i n more d e t a i l , i n d i c a t i n g t h a t t h e r e s u l t s p r e s e n t e d i n C h a p t e r 3 may be u s e f u l i n f o r m a l i z i n g t h e s e m a n t i c s o f network r e p r e s e n t a t i o n s . 2.8 O b j e c t i o n s t o N o n - M o n o t o n i c F o r m a l i s m s K r a m o s i l (1975) c l a i m s t o have shown t h a t any f o r m a l i z e d t h e o r y w h i c h a l l o w s u n p r o v a b i l i t y as a p r e m i s e i n d e d u c t i o n s must e i t h e r be \" m e a n i n g l e s s \" , o r no more p o w e r f u l t h a n t h e c o r r e s p o n d i n g f i r s t o r d e r t h e o r y w i t h o u t r u l e s i n v o l v i n g s u c h p r e m i s e s . He p r e s e n t s two \" p r o o f s \" t o s u p p o r t h i s c l a i m . C a r e f u l e x a m i n a t i o n shows t h a t t h e f i r s t r e s u l t f o l l o w s f r o m a d e f i n i t i o n o f \" f o r m a l i z e d t h e o r y \" w h i c h e x p r e s s l y e x c l u d e s any t h e o r y w h i c h e x h i b i t s t h e t y p e s o f b e h a v i o r common t o n o n - m o n o t o n i c t h e o r i e s . The s e c o n d r e s u l t i s b a s e d on an i n c o r r e c t d e f i n i t i o n o f \" p r o o f \" and hence o f \"theoremhood\" and i s i t s e l f m e a n i n g l e s s . As t h e p a p e r s t a n d s , i t shows o n l y t h a t n o n - m o n o t o n i c t h e o r i e s must behave d i f f e r e n t l y t h a n m o n o t o n i c t h e o r i e s i n t h o s e c a s e s where t h e f o r m e r c a n d e r i v e r e s u l t s u n o b t a i n a b l e u s i n g t h e l a t t e r . K r a m o s i l was n o t t h e o n l y one t o be u n c o m f o r t a b l e w i t h o p e n i n g t h e \" P a n d o r a ' s Box\" o f n o n - m o n o t o n i c i t y . S a n d e w a l l (1972) n o t e s t h a t t h e \" U n l e s s \" o p e r a t o r has \"some d i r t y l o g i c a l O b j e c t i o n s t o N o n - M o n o t o n i c F o r m a l i s m s 33 p r o p e r t i e s \" . C o n s i d e r i n g t h e example: A A A U n l e s s (B) D C A A U n l e s s (C) D B he o b s e r v e s t h a t e i t h e r B and C c a n be t h e o r e m s , b u t , i n g e n e r a l , n o t b o t h s i m u l t a n e o u s l y . R e i t e r (1978a) makes a s i m i l a r o b s e r v a t i o n i n an e a r l y p a p e r , s t a t i n g t h a t : S u c h b e h a v i o r [ i s ] c l e a r l y u n a c c e p t a b l e . A t t h e v e r y l e a s t , we must demand o f a d e f a u l t t h e o r y t h a t i t s a t i s f y a k i n d o f ' C h u r c h - R o s s e r 1 p r o p e r t y : No m a t t e r what t h e o r d e r i n w h i c h t h e theorems o f a t h e o r y a r e d e r i v e d , t h e r e s u l t i n g s e t o f theorems w i l l be u n i q u e . I t a p p e a r s t h a t t h e C h u r c h - R o s s e r p r o p e r t y i s a n e c e s s a r y c a s u a l t y i f n o n - m o n o t o n i c i t y i s a c c e p t e d . A f u r t h e r p r o b l e m w h i c h must be f a c e d by t h o s e e m b r a c i n g n o n - m o n o t o n i c i t y i s t h a t t h e non-theorems o f a f i r s t o r d e r t h e o r y a r e n o t r e c u r s i v e l y e n u m e r a b l e . T h i s means t h a t t h e r u l e s o f i n f e r e n c e i n t h e o r i e s i n v o l v i n g t h e Y o p e r a t o r c a n n o t be e f f e c t i v e i n g e n e r a l . From t h i s , i t f o l l o w s t h a t t h e theorems a r e n o t r e c u r s i v e l y e n u m e r a b l e . By c o n t r a s t , i n m o n o t o n i c l o g i c s , t h e r u l e s o f i n f e r e n c e MUST be e f f e c t i v e and t h e theorems MUST be r e c u r s i v e l y e n u m e r a b l e . F i n a l l y , t h e v e r y n o n - m o n o t o n i c i t y w h i c h makes s u c h t h e o r i e s i n t e r e s t i n g means t h a t \" t h e o r e m s \" may have t o be r e t r a c t e d i f t h e a s s u m p t i o n s on w h i c h t h e y a r e b a s e d a r e r e f u t e d ( e i t h e r by new knowledge o r c h a n g e s i n t h e s t a t e o f t h e w o r l d ) . To be u s e f u l , a n o n - m o n o t o n i c r e a s o n i n g s y s t e m must be a b l e t o remember w h i c h a s s u m p t i o n s u n d e r l y each t h e o r e m and be a b l e t o unwind t h e p o t e n t i a l l y complex c h a i n o f d e d u c t i o n s f o u n d e d on r e t r a c t e d j u s t i f i c a t i o n s . C h a p t e r 3 D e t e r m i n i n g t h e E x t e n s i o n s o f D e f a u l t T h e o r i e s 3.1 M o t i v a t i o n I n t h e p r e v i o u s c h a p t e r , R e i t e r ' s D e f a u l t L o g i c was examined i n some d e t a i l . I t was o r i g i n a l l y t h o u g h t t h a t most commonly-o c c u r r i n g d e f a u l t s were n o r m a l ( R e i t e r 1980) and t h e r e s u l t s o b t a i n e d c o n c e r n i n g n o r m a l t h e o r i e s seemed most e n c o u r a g i n g . R e i t e r and C r i s c u o l o (1981) l a t e r o b s e r v e d t h a t i n t e r a c t i n g d e f a u l t s c o u l d n o t be s a t i s f a c t o r i l y d e a l t w i t h by s t r i c t l y n o r m a l t h e o r i e s . They c o n s i d e r e d t h e example: T y p i c a l a d u l t s a r e employed. T y p i c a l h i g h - s c h o o l d r o p o u t s a r e a d u l t s . T y p i c a l h i g h - s c h o o l d r o p o u t s a r e n o t employed. W h i c h c o u l d be r e p r e s e n t e d by t h e f o l l o w i n g n o r m a l t h e o r y : A d u l t ( x ) : E m p l o y e d ( x ) (1) E m p l o y e d ( x ) D r o p o u t ( x ) : A d u l t ( x ) (2) A d u l t ( x ) D r o p o u t ( x ) : n E mployed(x) (3) -lEmployed (x) G i v e n t h e f a c t t h a t J o h n i s a d r o p o u t , t h i s t h e o r y has two d i s t i n c t e x t e n s i o n s , a s s e r t i n g e i t h e r t h a t J o h n i s employed o r n o t employed, r e s p e c t i v e l y . I n t u i t i v e l y , i t seems more l i k e l y t h a t J o h n i s unemployed. U n f o r t u n a t e l y , t h e r e i s no way t o f o r c e t h i s i n t e r p r e t a t i o n on t h e n o r m a l d e f a u l t t h e o r y w i t h o u t 34 m o t i v a t i o n 35 r e p l a c i n g (3) w i t h a f i r s t - o r d e r axiom o f t h e f o r m : V x . [ D r o p o u t (x) Z) nEmployed (x) ] . (4) T h i s f a i l s t o c a p t u r e t h e t e n t a t i v e n a t u r e o f t h e E n g l i s h d e s c r i p t i o n \u00E2\u0080\u0094 d i s c o v e r i n g an employed d r o p o u t w o u l d r e s u l t i n a l o g i c a l i n c o n s i s t e n c y . U s i n g t h i s and s e v e r a l o t h e r e x a m p l e s , R e i t e r and C r i s c u o l o i l l u s t r a t e a need f o r s e m i - n o r m a l d e f a u l t s s u c h a s : A d u l t (x) : E m p l o y e d ( x ) A i D r o p o u t ( x ) (5) Emp l o y e d ( x ) i n s t e a d o f (3) o r ( 4 ) , i n o r d e r t o f u l l y c h a r a c t e r i z e common u s e s o f d e f a u l t r e a s o n i n g . S e m i - n o r m a l d e f a u l t t h e o r i e s c a n be us e d t o r e p r e s e n t many forms o f knowledge, i n c l u d i n g s e m a n t i c n e t w o r k s , d a t a b a s e s , and t h e i n t e r a c t i o n s between d e f a u l t s , T h i s w i l l be l i t t l e more t h a n a l o g i c a l c u r i o s i t y , however, i f t h e e x t e n s i o n s o f t h e r e s u l t i n g d e f a u l t t h e o r i e s c a n n o t be computed, and t h e p r o p e r t i e s o f n o n - n o r m a l d e f a u l t t h e o r i e s have so f a r been l a r g e l y unexamined. The f o l l o w i n g s e c t i o n a d d r e s s e s t h i s p r o b l e m . 3.2 A C o n s t r u c t i v e Mechanism R e i t e r p r o v i d e s a t e s t t o d e t e r m i n e whether a s e t o f f o r m u l a e i s an e x t e n s i o n f o r an a r b i t r a r y d e f a u l t t h e o r y , b u t he p r o v i d e s no c o n s t r u c t i v e mechanism w h i c h y i e l d s t h e e x t e n s i o n s o f s u c h t h e o r i e s . Of c o u r s e , t h e e x t e n s i o n s o f d e f a u l t t h e o r i e s a r e n o t r e c u r s i v e l y e n u m e r a b l e i n g e n e r a l ( R e i t e r 1 9 8 0 ) . A l l t h a t c a n be hoped f o r i s a p r o c e d u r e w h i c h y i e l d s t h e e x t e n s i o n s o f A C o n s t r u c t i v e Mechanism 36 t h e o r i e s r e s t r i c t e d t o d e c i d a b l e subcases o f the p r e d i c a t e c a l c u l u s (eg s e n t e n t i a l , monadic, or f i n i t e t h e o r i e s ) . T h i s c h a p t e r p r o v i d e s such a mechanism a p p l i c a b l e t o a r b i t r a r y f i n i t e d e f a u l t t h e o r i e s . I n what f o l l o w s , the a l p h a b e t , A, d i s c u s s e d i n Chapter 2, i s r e s t r i c t e d t o c o n t a i n o n l y f i n i t e l y many v a r i a b l e s , c o n s t a n t symbols, and p r e d i c a t e l e t t e r s , p l u s the p u n c t u a t i o n s i g n s and l o g i c a l c o n n e c t i v e s . No f u n c t i o n l e t t e r s a r e a l l o w e d (except the 0-ary f u n c t i o n l e t t e r s , or c o n s t a n t s ) . The d i s c u s s i o n i s f u r t h e r r e s t r i c t e d by the r e q u i r e m e n t t h a t f o r any g i v e n d e f a u l t t h e o r y , A = (D,W), D must be f i n i t e . The e f f e c t o f the above r e s t r i c i o n s i s t o ensure t h a t the Herbrand U n i v e r s e a s s o c i a t e d w i t h A i s f i n i t e and hence t h a t the c l o s u r e o f A ( d i s c u s s e d p r e v i o u s l y ) i s f i n i t e . The r e a s o n s f o r t h e s e r e s t r i c t i o n s , t h e i r r e p e r c u s s i o n s , and the e f f e c t s o f r e l a x i n g them a r e d i s c u s s e d i n the f o l l o w i n g s e c t i o n s . A d e f i n i t i o n o f an i t e r a t i v e p r o c e d u r e f o r d e t e r m i n i n g the e x t e n s i o n s o f an a r b i t r a r y f i n i t e d e f a u l t t h e o r y i s now g i v e n . T h i s i s f o l l o w e d by the d e r i v a t i o n o f the two h a l v e s o f a completeness r e s u l t which shows t h a t the p r o c e d u r e can r e t u r n a l l (Theorem 3.6) and o n l y (Theorem 3.4) the e x t e n s i o n s o f the d e f a u l t t h e o r y t o which i t i s a p p l i e d . A Constructive Mechanism 37 D e f i n i t i o n 3.1 Consider an ar b i t r a r y closed default theory, A= (D,W). A sequence of \"hypothesized extensions\", H^, (i > 0) i s then defined as follows: H Q = Th(W) For j > 0 define hj = Th(W) and GDJJ = 0 For i > 0 l e t D^ be the set of defaults whose precondi-tions have been s a t i s f i e d and whose j u s t i f i c a t i o n s have not been denied. More precisely: D^ = {6\ 6 = 6 D, v A 6 h j , - , B l f . . . , n B m 0 (hj U Hj_ x) } A : B - ^ , . . . , B m \"|\" Choose o' = a r b i t r a r i l y from (D^ - GD^) , v from those defaults e l i g i b l e to be, but which have not yet been, applied. Then define: G D J + 1 = GDJ U {Ar } h j + l = T h ( h j u M ) oo . H i = u h3 i=0 Observe that Hj i s l o g i c a l l y closed. Since D i s f i n i t e , i may be bounded above by the c a r d i n a l i t y of D without loss of generality. D e f i n i t i o n 3.1 38 The a p p l i c a t i o n o f t h e T h ( ) o p e r a t o r i n t h e above d e f i n i t i o n makes i t i m m e d i a t e l y c l e a r t h a t t h e H^'s w i l l n o t be w e l l d e f i n e d i n any s i t u a t i o n where f i r s t - o r d e r theoremhood i s un-d e c i d a b l e . F i n i t e t h e o r i e s , s u c h as t h o s e d i s c u s s e d h e r e , a r e d e c i d a b l e . T h i s s h o u l d be k e p t i n mind i n t h e f o l l o w i n g d i s c u s s i o n s . The f o l l o w i n g lemmas w i l l be r e q u i r e d i n o r d e r t o o b t a i n t h e d e s i r e d c o m p l e t e n e s s r e s u l t : Lemma 3.2 F o r ( i > 0) d e f i n e d as i n D e f i n i t i o n 3.1, A : B l f...,B m i f O = 6 D, w t h e n w 6 Th(W) => V j . v 6 Hj The p r o o f i s an o b v i o u s c o n s e q u e n c e o f t h e f a c t t h a t , f o r a l l j , hjj = Th(W) and hj C H j . The n e x t lemma has a b i t more s u b s t a n c e . Lemma 3.3 F o r H^ and <\u00C2\u00A3 d e f i n e d as i n Lemma 3.2, i f -iBlr ,nBm 0 ( H j - i u H j ) a n d A 6 Hj t h e n w G H j . P r o o f F i r s t , o b s e r v e t h a t : y e . e e Hj => ^ i . e e hj ( i ) Lemma 3 . 3 39 V e. e M j => V i . e \u00C2\u00A3 h j ( i i ; I t f o l l o w s t h a t A 6 Hj => ^ i . A \u00E2\u0082\u00AC h j . L e t k be t h e l e a s t s u c h i . C l e a r l y , V i ^ k , A 6 h j and nB 1,...,nB m 0 ( H j _ ! U Hj) => V i>k. d> G DJ C D. L e t c be t h e c a r d i n a l i t y o f D. S i n c e D i s f i n i t e , c i s f i n i t e . I t c a n be shown t h a t 6 6 GDJJ + C , as f o l l o w s : C l e a r l y , i f GDJ Z) G D ^ + 1 f o r some i , k c a r d ( G D J ) must be monotone i n c r e a s i n g . => c a r d ( G D J J + c ) > c b u t i t must be t h a t GD^ Q D. T h e r e f o r e GDJ3 + C = D => ci 6 GDJJ + C ( c o n t r a d i c t i o n ) I f ci G G D ^ + C t h e n w 6 h j + c Q H j . Thus w G H j . QED The p r o o f o f lemma 3 . 3 r e l i e s on t h e f i n i t e n e s s o f D, e x p l a i n i n g t h e r e s t r i c t i o n s p l a c e d on t h e a l p h a b e t and d e f a u l t t h e o r i e s a t t h e b e g i n n i n g o f t h i s c h a p t e r . I t i s r e a s o n a b l e t o ask whether s u c h r e s t r i c t i o n s a r e n e c e s s a r y . The answer t o t h i s q u e s t i o n a p p e a r s t o be \" y e s \" . C e r t a i n l y , i t c a n be shown t h a t t h e lemma does n o t h o l d f o r i n f i n i t e D. To s e e t h i s , c o n s i d e r t h e t h e o r y w i t h an i n f i n i t e s e t o f c o n s t a n t s , {a^}, an i n f i n i t e s e t o f d e f a u l t s , Lemma 3.3 40 A : P ( a i ) A : Q U ^ D = { 0) , s a t i s f i e s D e f i n i t i o n 3.1, b u t t h a t Q(a^) 0 E^. The r e l a t e d q u e s t i o n , whether t h e r e i s any i t e r a t i v e mechanism w h i c h y i e l d s t h e d e s i r e d r e s u l t s w i l l be a d d r e s s e d i n C h a p t e r 5. The t e r m \" H y p o t h e s i z e d E x t e n s i o n s \" f o r t h e H^'s w i l l now be j u s t i f i e d by t h e f i r s t h a l f o f a c o m p l e t e n e s s r e s u l t . The s e q u e n c e o f H^'s i s s a i d t o c o n v e r g e i f 3 n - H n = Hn+1* I f c ^ s shown t h a t i f t h e s e q u e n c e o f H^'s e v e r c o n v e r g e s , H n i s an e x t e n s i o n . F u r t h e r m o r e , i f any o f t h e H^'s i s an e x t e n s i o n , t h e s e q u e n c e c o n v e r g e s a t t h a t p o i n t . Theorem 3.4 A s e q u e n c e Hg, H^, ... d e f i n e d as i n D e f i n i t i o n 3.1 c o n t a i n s two c o n s e c u t i v e , i d e n t i c a l e l e m e n t s , H n_^ and H n , i f f Hn_-j_ i s an e x t e n s i o n f o r A. P r o o f (=>) F o l l o w i n g R e i t e r (1980, thm 2 . 1 ) , d e f i n e EQ = w and, f o r i > o, A : B-L , . . . , B M E i + 1 = T h ( E i ) u M 6 D ' w Theorem 3.4 41 A G E i f -,Blr . . . ,-,Bm 0 Hn} CO then H n (= H^^) i s an e x t e n s i o n f o r A i f f H n = U E^. i=0 Thus i t must be proved that co (a) U E i C H n and i = 0 (b) H n C ? E i i=0 a) This can be shown by induction. Clearly Eg C H n. Assume E^ Q H n and consider 0 6 E i + 1 . There are two cases for 9: i) 0 6 Th (E^) => 0 6 H n since E^ C H n and the are closed under Th ( ) . i i ) Otherwise 0 is w where: A : B ^ , . . . / B M G D, A G E\u00C2\u00B1, nB1,...,nBm 0 H n. w But A 6 => A G H n. Thus, by lemma 3.3, w G H n. co It follows that 0 E t C H n. i = 0 b) By d e f i n i t i o n , H n = U h\u00C2\u00A3. It suff i c e s , therefore, to show i = 0 co that V k. h\u00C2\u00A3 C D This is demonstrated by induction i=0 on k. The base step is provided by: CD h n = Th(W) = Th ( E Q ) Q E\u00C2\u00B1 C U E\u00C2\u00B1. i=0 Theorem 3.4 42 co Hence, assume h \" ^ C U E i r for some k > 0. Consider i=0 hj = Th(h n_ x u {w}). A : i . . . , B m C l e a r l y w 6 {w| G D, A 6 hg_ l f nBlt.,.,-,Bm 0 (hjj_]_ U Hn_-^ ) } (Note that (ri{J_-L U H,^) = Hn.) co co Since U i s closed under Th ( ), and hj^.^ Q U E i by i=0 i=0 co hypothesis, i t s u f f i c e s to show that w 6 U . i=0 co A 6 h^_1 => A G U E\u00C2\u00B1. (hypothesis) i=0 A : B-^, . . . , B m Thus G D, A G U E \u00C2\u00A3 , n B 1 , . . . , n B m 0 Hn, w i=0 CO Therefore w G U E\u00C2\u00B1. From t h i s , the r e s u l t follows, i=0 Combining (a) and (b) y i e l d s : co Hn-1 = H n = . u E i -i=0 => H^-j^ i s an extension for A. (<=) It w i l l now be shown that i f Hn_-L i s an extension for A then H n - 1 = H n by showing that: (a) H n Q H n_ l f and Theorem 3.4 43 (b) En_\u00C2\u00B1 C H n. 00 By d e f i n i t i o n , H n = U h\u00C2\u00A3. Induction yi e l d s the desired k=0 re s u l t , as follows: a) Consider 0 6 H n. There are two cases: i) \u00C2\u00A9 e hg => e e Th(w) = h g - 1 c H n - 1 => \u00C2\u00A9 e H n_ 1. i i ) otherwise, assume h\u00C2\u00A3_-^ C H n - 1 ' Thus \u00C2\u00A9 6 h\u00C2\u00A3 => \u00C2\u00A9 6 Th(h n_ x U {w}) , for some 6 = A. I B ^ f m \u00E2\u0080\u00A2 \u00E2\u0080\u00A2 f B m n => A 6 hjj_x => A e H n-1 also, nB 1,...,nB m 0 ( h k _ l U Hn-l* => nB-,^ , . . . , i B m 0 H j ^ . Therefore, w e H n_ 1 => 0 6 H (hypothesis) (lemma 3.3) n-1 (H^ closed under Th( )) co b) As noted above, H n - 1 i s an extension => H n_ 1 = U E^. i=0 oo Consider 0 6 HN_1 (=> 9 G U Ej => ^ i . 6 S E;). i=0 Continuing by induction, i t i s shown that \u00C2\u00A9 \u00E2\u0082\u00AC H n as follows: i) 0 e E0 => \u00C2\u00A9 e w => \u00C2\u00A9 e hg => \u00C2\u00A9 e H n Therefore E n C H n. ii) Assume C H n for some i > 0. Theorem 3.4 44 Then 8 G => 9 6 T h f E ^ ) U {w| \u00E2\u0080\u0094 \u00E2\u0080\u0094 - 6 D, w A 6 ^i-X' i \u00E2\u0080\u00A2 r\",\u00C2\u00AEm ^ C a s e s : 1) 9 6 T h ( E ^ _ 1 ) => 9 6 H n ( h y p o t h e s i s and c l o s u r e ) A : B^ i . . . ,Bj^ 2) o t h e r w i s e , 0 6 {w| 6 D, v A 6 E ^ _ ^ , nB^,...,nBm 0 ^n-1^ A 6 Ei_\u00C2\u00B1 => A 6 H n ( h y p o t h e s i s ) I t was p r o v e d i n (a) above t h a t H n Q H n _ 1 . Thus nB 1,...,nB m 0 H^-,^ => nB 1,...,nB m 0 H\"n. T h e r e f o r e , by lemma 3.3, 0 6 H n . C o m b i n i n g (a) and (b) g i v e s t h e d e s i r e d r e s u l t , namely: H n - 1 = H n -QED The f o l l o w i n g c o r o l l a r y u n d e r l i n e s t h e s t a b i l i t y o f t h e method. C o r o l l a r y 3.5 I f A = (D,W) and a r e d e f i n e d as i n d e f i n i t i o n 3.1 t h e n : f o r a r b i t r a r y j > 0 Corollary 3.5 45 H j - 1 = H j => H j = H j + 1 -Proof H j-1 = H j = > H j i s a n extension. By Theorem 3.4, Hj = H j + 1 < An example may i l l u s t r a t e the algorithm. Consider the default theory, A = (D,W), with: D = { 6\u00C2\u00B1 = A : B , d>2 = A : -iB } B nB W = { A } This theory has two extensions: E-L = Th ( {A, B}) E 2 = Th({A,iB}) The f i r s t i t e r a t i o n of the algorithm results i n : H Q = Th({A}) hj = H 0 GDj = 0 Dj = {c^,^} At this point there are two ways to proceed, depending on whether o^ or o 2^ i s chosen in forming h^. Each case w i l l be considered in turn. 1) I f c^ were chosen: h{ = Th ( {A,B} ) GD{ = D{ = {c^} A l l succeeding h^ w i l l be i d e n t i c a l to h^, since there are no more e l i g i b l e defaults. Hence: oo , H i = U h| = Th ( {A,B} ) = E-!_. i=0 h\u00C2\u00A7 = Th ({A}) GDg = 0 D\u00C2\u00A7 = {d^} hi = Th ( {A,B} ) GDf = {d^} Dl = {c^} H 2 = Th({A,B}) = E 1 . C o r o l l a r y 3 . 5 46 Of c o u r s e , t h i s was t o be e x p e c t e d : s i n c e i s an e x t e n s i o n f o r A and H-^ = E ^ , Theorem 3 . 4 g u a r a n t e e s t h a t H 2 \u00E2\u0080\u00A2= H-^ ,. I t - c a n e a s i l y be s e e n t h a t t h e p r e s e n c e o f B i n p r e v e n t s t h e a p p l i c a t i o n o f c( 2 i n t h e g e n e r a t i o n o f H 2 and so p r o d u c e s t h e d e s i r e d r e s u l t . 2 ) I f 62 were c h o s e n : h{ = T h ( { A , - , B } ) GD{ = {rJ2} = {o^} A g a i n , t h e r e a r e no more e l i g i b l e d e f a u l t s , s o : E1 = T h ( { A , n B } ) = E 2 . h\u00C2\u00A7 = T h ({A}) GDQ h ^ = Th({A,HB}) GD^ H 2 = T h ( { A , n B } ) = E 2 . Thus t h e method i s c a p a b l e o f c o n v e r g i n g on e a c h o f t h e e x t e n s i o n s f o r A. C o m f o r t i n g as t h e r e s u l t s p r e s e n t e d may be, t h e y do n o t h i n g t o i n d i c a t e t h a t t h e method c o u l d e v e r a r r i v e a t an H n w h i c h i s , i n d e e d , an e x t e n s i o n . The f o l l o w i n g t h e o r e m p a r t i a l l y r e c t i f i e s t h i s , p r o v i n g t h a t f o r an a r b i t r a r y e x t e n s i o n , E , t h e r e i s a s e q u e n c e o f H^'s w h i c h c o n v e r g e s t o E . I n f a c t , t h e r e i s a s e q u e n c e w h i c h c o n v e r g e s i n a s i n g l e i t e r a t i o n . Theorem 3 . 6 L e t A = (D,W) be a d e f a u l t t h e o r y w i t h e x t e n s i o n E . T h e r e i s Theorem 3.6 47 a s e q u e n c e H Q , H-^ , \u00E2\u0080\u00A2.., H n - 1 ' H n ' d e f i n e < 3 a s P e r d e f i n i t i o n 3.1, s u c h t h a t H n _ 1 = H n = E . I n p a r t i c u l a r , t h e r e i s a s e q u e n c e s u c h t h a t H i = H 2 = E * P r o o f I f W i s i n c o n s i s t e n t , t h e n E = L. ( R e i t e r 1980, Cor 2.2) H 0 = Th(W) = L F o r a r b i t r a r y i > 0, h j = Th(W) = L C l e a r l y a l l h j Q L oo => H i = U h^ = L = E . j = 0 Hence assume t h a t W i s c o n s i s t e n t . The s e t o f g e n e r a t i n g d e f a u l t s f o r E w i t h r e s p e c t t o A i s d e f i n e d as f o l l o w s ( R e i t e r 1 9 80): A : , \u00E2\u0080\u00A2 \u00E2\u0080\u00A2 . ,BJJJ GD(E ,A) = { 6 D | A 6 E , n B^.^nB,,, 0 E } w Lemma 3.7 (below) shows t h a t a n o n - t r i v i a l s u b s e t o f t h e p o s s i b l e s e q u e n c e s o f H^'s d e f i n e d by d e f i n i t i o n 3.1 c a n be o b t a i n e d by l i m i t i n g t h e c h o i c e o f ^ a t \"f\" i n t h e d e f i n i t i o n t o an a r b i t r a r y member o f ((D^ - GD^) (~~)GD(E,A)). T h i s d e v i c e w i l l be employed t o c o m p l e t e t h e p r o o f . I t s u f f i c e s t o show t h a t H^ = E , s i n c e H^ = H 2 t h e n f o l l o w s d i r e c t l y f r o m Theorem 3.4. C l e a r l y , W C Hj_ C Th (W U CONSEQUENTS (GD (E,A) ) ) => E\u00C2\u00B1 C E . ( R e i t e r 1980, Thm 2.5) I t r e m a i n s t o show t h a t E C H]_. Theorem 3.6 48 D e f i n e as b e f o r e , and r e c a l l t h a t , s i n c e E i s an e x t e n s i o n co f o r A , E = U E ^ . i=0 C l e a r l y Eg C H 1 . F o r i > 0, assume C H p and c o n s i d e r w 6 E j _ + ] _ . T h e r e a r e two c a s e s : i ) w 6 Th(E\u00C2\u00A3 +-^) => w 6 ( h y p o t h e s i s and c l o s u r e ) . i i ) O t h e r w i s e , t h e r e i s a d e f a u l t , A : , . . . /BJJJ O = 6 D, A 6 E i f nB 1,...,nB m 0 E . w C l e a r l y , A G E and A G H-^ {E\u00C2\u00B1 C E , h y p o t h e s i s ) T h e r e f o r e , o' G GD ( E , A ) . A G H l f nB 1,...,nB m 0 ( H Q U H-^ => w G E-^. /(Lemma 3.3) I t r e m a i n s , t h e r e f o r e , t o show t h a t nB-L,...,nBm 0 (Hg U H-^ ) . I f t h i s i s n o t t r u e , t h e n t h e r e a r e two c a s e s : i ) 3 i - 6 Hg = Th(W) C E => - i B ^ 6 E ( c o n t r a d i c t i o n ) i i ) 3 i ' \"\u00C2\u00BB Bi 6 H i I t was shown above t h a t E^ Q E . = > -\"B^ 6 E ( c o n t r a d i c t i o n ) T h e r e f o r e , -iB l f...,nB m 0 (Hg U H^) . Thus E ^ + ^ C E\u00C2\u00B1. I t f o l l o w s by i n d u c t i o n t h a t E C H-^ . QED The above r e s u l t h i n g e s on t h e f a c t t h a t i t i s a l w a y s Theorem 3.6 49 p o s s i b l e t o r e s t r i c t t h e e l i g i b l e c h o i c e s o f d e f a u l t s t o t h o s e w h i c h , i n some s e n s e , \"must\" be made t o y i e l d t h e e x t e n s i o n i n q u e s t i o n . The f o l l o w i n g lemma shows t h a t t h i s r e s t r i c t i o n i s a l w a y s p o s s i b l e \u00E2\u0080\u0094 p r o v i d e d a l l p r e v i o u s c h o i c e s have been so r e s t r i c t e d \u00E2\u0080\u0094 w i t h o u t e l i m i n a t i n g a l l o f t h e p o s s i b i l i t i e s . Lemma 3.7 G i v e n a d e f a u l t t h e o r y , A = (D,W), w i t h an e x t e n s i o n , E , i f GD\ C GD (E,A) t h e n ( ( D J ; -GD\) DGD(E,A)) = $rf i f f ( D J - GD\) = 0 P r o o f (<=) T r i v i a l (=>) The p r o o f p r o c e e d s by i n d u c t i o n on i . N o t e : V i . ( h j U H Q ) = h\ (Hg = Th(W) C h\) As a n o t a t i o n a l c o n v e n i e n c e , t h e e l i g i b l e d e f a u l t s , ED^, a r e d e f i n e d as ( D | - GD^): t h e a p p l i c a b l e d e f a u l t s l e s s t h o s e w h i c h have a l r e a d y been a p p l i e d . i = 0 The i n d u c t i v e p r o o f f o r t h e i = 0 c a s e h i n g e s on t h e f o l l o w i n g o b s e r v a t i o n s : . A : B ^ , . . . , B j ^ i ) D j = [6\ 6 = 6 D, A 6 h j , n B l f . . . , - , B m 0 hj} w i i ) A 6 hg = Th(W) => A 6 E i i i ) n B i 0 E => nBi 0 hg Lemma 3.7 50 i v ) E D j = (Dj - GDJ) = (Dj - J2f> = DJ. Assume (GD (E,A) O EDJ) = 0 and EDJ ^ 0. A. s B X ' * * * ' .\u00C2\u00BB 3 \u00C2\u00ABJ - m 6 D, A 6 Th (W) , -iB l f . . . ^ B m 0 h j = Th(W) , and, for some i , -iB^ 6 E. R e c a l l t h a t , since E i s an extension for A, co E = U E. j = 0 (Reiter 1980, Thm 2.1) By i n d u c t i o n on j , i t w i l l be shown that -iB^ 0 E. C l e a r l y Eg = W C Th(W) => iB^^ 0 E n . Let Ej C Th(W) and consider E j ^ . C : F l f . . . , F r Let Dj = {6\ 6 = e D, c e E j , -iFlr. . . , n F r 0 E} E J + 1 = Th(Ej) U CONSEQUENTS(Dj) Th(Ej) C Th(W) (hypothesis) -jBi 6 E j + 1 A ~t&i 0 Th(W) => i B i 6 CONSEQUENTS (Dj) . But Dj C GD(E ,A) and Dj C DJ = EDJ = > Dj C (GD (E ,A) 0 EDj) => Dj = 0 => CONSEQUENTS(Dj) = 0 => E j + 1 = Th(Ej) C Th(W) and n B i 0 CONSEQUENTS(Dj) CO Thus -iBi 0 U E-! => I B J 0 E j = 0 J ( c o n t r a d i c t i o n ) ( c o n t r a d i c t i o n ) Lemma 3 . 7 51 T h e r e f o r e (GD(E,A) D EDJ) = 0 = > EDJ = 0. i > 0 F o r t h e i n d u c t i v e s t e p , a l l o w t h e c o n j e c t u r e t o h o l d f o r E D ] ^ and c o n s i d e r ED]| (i\u00C2\u00A3l) . Assume (GD(E,A) O ED\) = $ and ED]; jt 0. The d i s c u s s i o n below makes use o f t h e f o l l o w i n g i d e n t i t i e s : (GD(E,A) (~) EDj) = (GD (E ,A) O &\ - GDJ) ) = ( (GD (E ,A) - G D J ) (~) n\) = 0 ( h y p o t h e s i s ) A : , . . . , B m ED+ ^ => ^ O = 6 D s u c h t h a t o 6 ED+. w => A 6 A n B l f . . . ^ B m 0 h j . A 0 E V 3 i . n\u00C2\u00BBi 6 E . C l e a r l y , h } C E (GD]; C GD(E,A)) => A e E. T h e r e f o r e , i t must be t h a t nB^ 6 E . I f (GD (E,A) - GD\) = & t h e n I f 6 G GD (E,A) t h e n 6 6 GY)\ => CONSEQUENTS(GD(E,A) ) C h\ => (W U CONSEQUENTS (GD (E,A) ) )' Q h\ => E C h | ( c l o s u r e , R e i t e r 1980, Thm 2.5) => -iB^ 0 E ( c o n t r a d i c t i o n ) O t h e r w i s e 6 G D\ => d) 0 (GD (E,A) - GD\) Lemma 3.7 52 = > cj 0 GD(E,A) V A e GD\. Thus, i f ti S D ^ , t h e r e a r e two c a s e s : i ) 6 6 GD\ C GD(EA) => ^ I 0 E ( c o n t r a d i c t i o n ) i i ) c\u00C2\u00BB 0 G D ( E A ) => (DJDGD(EA)) =0 ( g i v e n ( i ) ) r /, ( C : F l f . . . , F r = >. {d| C 6 E . Assume t h a t D ] ; ^ 0 C : F x,...,F = > ( (6 = 6 D . A C 6 h + u A - i F p \u00E2\u0080\u00A2 \u00E2\u0080\u00A2 . , i F r 0 h\) => ^k. -,Fk \u00E2\u0082\u00AC E ) C : F-j_, . . . ,F r C o n s i d e r 6' = 6 ( E D + _ 1 f) G D ( E ,A) ) u I f t h e r e i s no such 6' t h e n , by h y p o t h e s i s , E D ^ = 0 => = h | _ x = > E D ] ; = 0 O t h e r w i s e : C 6 hl_\u00C2\u00B1 Q h j , T F l f . . . n F r 0 E B u t h j C E => -iFj_, . . . ,-!Fr 0 h];. T h e r e f o r e e D{ A -\u00C2\u00BB*\u00E2\u0080\u00A2]_, . . . ,nFr 0 E Lemma 3.7 53 => o' \u00E2\u0080\u00A2 e DAC e h|A ...., -,\u00C2\u00A5r 0 E => d>' G (D^ (~) GD (E,A) ) ( c o n t r a d i c t i o n ) T h e r e f o r e , D^ = 0 => ED^ = 0 QED G i v e n t h e o p t i m i s t i c n a t u r e o f t h e s e r e s u l t s , one m i g h t hope t o be a b l e t o s t r e n g t h e n them by showing t h a t a l l s e q u e n c e s o f H^'s c o n v e r g e on e x t e n s i o n s . U n f o r t u n a t e l y , t h i s i s n o t t r u e i n g e n e r a l , s i n c e i t would i m p l y t h a t a l l d e f a u l t t h e o r i e s have e x t e n s i o n s , w h i c h i s n o t t h e c a s e . (For example, t h e t h e o r y : W = { } iA A i B , : B A \" iC , : C A i A D = { A B C has no e x t e n s i o n . ) The weaker r e s u l t , t h a t a l l s e q u e n c e s o f H^'s c o n v e r g e p r o v i d e d t h a t A has an e x t e n s i o n , a l s o f a i l s t o h o l d f o r g e n e r a l d e f a u l t t h e o r i e s . The d e f a u l t t h e o r y : W = { A } A : B A i D A : D A i C B : C D = { d 0 = , d, = , 6 2 = } B D C h a s an e x t e n s i o n , E = T h ( { A , B , c } ) . The s e q u e n c e o f H j 1 s d e t e r m i n e d by c h o o s i n g : G D J = G D J _ 1 U {6k} j > 0, k = ( i - 1 ) mod 3 i s l e g a l a c c o r d i n g t o D e f i n i t i o n 3.1 b u t n e v e r c o n v e r g e s . I n g e n e r a l , t h e n , t h e most t h a t c o u l d be hoped f o r i s a t r a c t i b l e means o f d e t e r m i n i n g whether a p a r t i c u l a r s e q u e n c e o f H^'s w i l l n o t c o n v e r g e . G i v e n t h e f i n i t e n a t u r e o f D, t h e o n l y way f o r a s e q u e n c e o f H^'s n o t t o c o n v e r g e i s by t h e o c c u r r e n c e , 54 somewhere i n the sequence , o f an H n = H m , 0 < m < n-1 (^e for the sequence to c y c l e ) . W h i l e t h e o r e t i c a l l y p o s s i b l e , i t does not seem d e s i r a b l e to m a i n t a i n a complete l i s t o f the H^'s and compare each new element w i t h a l l o f i t s p r e d e c e s s o r s ! E x p e r i e n c e has shown t h a t the o c c u r r e n c e , a t any s t ep i n the c o n s t r u c t i o n o f H ^ , o f a c o n d i t i o n where GDj D i 1 S a r e l i a b l e i n d i c a t o r t h a t the sequence i s about, to c y c l e . I n t u i t i v e l y , t h i s c o n d i t i o n i n d i c a t e s t h a t the j u s t i f i c a t i o n s for a d e f a u l t , J , which has a l r e a d y been a p p l i e d , have been d e n i e d . T h u s , the consequent o f <\u00C2\u00A3 w i l l not be i n H^+i- T h i s i n f o r m a t i o n , toge ther w i t h the f a c t t h a t i t i s known t h a t t h e r e i s a sequence o f H^'s which converges immediate ly (ie w i t h o u t l o o p i n g ) , might be a p p l i e d by a d e p t h - f i r s t s earch for an e x t e n s i o n to i n d i c a t e the need for b a c k t r a c k i n g . I t has not been d e t e r m i n e d , however, whether t h i s r u l e always h o l d s or would serve o n l y as an h e u r i s t i c . The q u e s t i o n for w h i c h , i f any, c l a s s e s o f d e f a u l t t h e o r i e s every sequence o f H^'s i s guaranteed to converge on an e x t e n s i o n ( i f there i s one) for A remains open . Chapter 4 examines t h i s problem f u r t h e r , s u g g e s t i n g some p r o m i s i n g c a n d i d a t e s . A l l o f the r e s u l t s p r e s e n t e d above a p p l y e q u a l l y w e l l to c l o s e d and open d e f a u l t t h e o r i e s . To see t h i s , i t i s s u f f i c i e n t to observe t h a t the Herbrand U n i v e r s e for a f i n i t e d e f a u l t t h e o r y , A, over a f i n i t e a l p h a b e t w i t h no f u n c t i o n symbols , A , must be f i n i t e . From t h i s i t f o l l o w s t h a t CLOSED-DEFAULTS(A) must a l s o be f i n i t e . T h u s , a l l o f R e i t e r ' s r e s u l t s g e n e r a l i z i n g the n o t i o n o f e x t e n s i o n to a r b i t r a r y d e f a u l t t h e o r i e s can a l s o be a p p l i e d h e r e , f i n i t e n e s s r e f e r r e d t o R e i t e r ' s p a p e r f o r m a c h i n e r y i n v o l v e d . 55 n o t w i t h s t a n d i n g . The r e a d e r i s a d e t a i l e d d e s c r i p t i o n o f t h e C h a p t e r 4 D i r e c t i o n s f o r F u t u r e R e s e a r c h D u r i n g t h e c o u r s e o f t h e r e s e a r c h u n d e r l y i n g t h i s t h e s i s , a number o f p r o m i s i n g avenues f o r r e s e a r c h on r e l a t e d t o p i c s became a p p a r e n t . T h e s e r a n g e d f r o m e x t e n s i o n s o f t h e r e s u l t s p r e s e n t e d h e r e t o d e t e r m i n i n g t h e r e l a t i o n s h i p s between d e f a u l t l o g i c and t h e many o t h e r e x i s t i n g f o r m a l i s m s . Some o f t h e t o p i c s w h i c h w a r r a n t f u r t h e r e x p l o r a t i o n a r e o u t l i n e d below. I n c l u d e d i n t h e d i s c u s s i o n a r e p o s s i b l e a p p r o a c h e s w h i c h may p r o v e f r u i t f u l i n d e a l i n g w i t h t h e p r o b l e m s . 4.1 D e f a u l t T y pe H i e r a r c h i e s H i e r a r c h a l T a x o n o m i e s , o r t y p e h i e r a r c h i e s , a r e e x t r e m e l y common i n A I . The f a c t t h a t n o r m a l IS-A h i e r a r c h i e s a r e i s o m o r p h i c t o some u n d e r l y i n g f i r s t - o r d e r l o g i c i s now w i d e l y a c c e p t e d (Woods 1975, S c h u b e r t 1976, Hayes 1 9 7 7 ) . When e x c e p t i o n s a r e a l l o w e d w i t h i n t h e i n h e r i t a n c e s t r u c t u r e , however, t h e i r s e m a n t i c s a r e no l o n g e r so s t r a i g h t f o r w a r d . I t a p p e a r s t h a t s e m i - n o r m a l d e f a u l t t h e o r i e s c a n be u s e d t o r e p r e s e n t t y p e h i e r a r c h i e s w i t h e x c e p t i o n s . S i n c e t h e h i e r a r c h i e s a r e a c y c l i c , t h e u n d e r l y i n g d e f a u l t t h e o r i e s w i l l a l s o be a c y c l i c \u00E2\u0080\u0094 a l t h o u g h e x a c t l y what c o n s t i t u t e s an a c y c l i c 56 D e f a u l t T ype H i e r a r c h i e s 57 d e f a u l t t h e o r y i s n o t n e c e s s a r i l y o b v i o u s . D u r i n g t h e c o u r s e o f t h e r e s e a r c h r e p o r t e d h e r e i n , s e v e r a l a t t e m p t s were made t o d e f i n e j u s t t h i s . W h i l e a g e n e r a l , f o r m a l d e f i n i t i o n o f a c y c l i c d e f a u l t t h e o r i e s has y e t t o be o b t a i n e d , a c h a r a c t e r i z a t i o n w h i c h seems t o c a p t u r e t h e e s s e n t i a l f e a t u r e s has been f o u n d . As one m i g h t e x p e c t , g i v e n t h e w e l l - b e h a v e d n e s s o f n o r m a l d e f a u l t t h e o r i e s , t h e c e n t r a l f e a t u r e w h i c h must be d e a l t w i t h i s i n t h o s e p a r t s o f t h e j u s t i f i c a t i o n s w h i c h make i n d i v i d u a l d e f a u l t s n o n - n o r m a l . F o r t h e r e s t r i c t e d c l a s s o f s e m i - n o r m a l d e f a u l t t h e o r i e s w h i c h c o r r e s p o n d t o t y p e h i e r a r c h i e s w i t h e x c e p t i o n s , a l l d e f a u l t s must have t h e f o r m : A : B A C X A \u00E2\u0080\u00A2 \u00E2\u0080\u00A2 \u00E2\u0080\u00A2 A C M B and a l l f o r m u l a e i n W must be o f t h e f o r m : \" A DB\" o r \" A \" where A , B , and t h e C ^ s a r e p o s i t i v e o r n e g a t i v e l i t e r a l s . The r e l a t i o n s < and < a r e d e f i n e d as f o l l o w s : ci 6 D => A < B , - i C ^ < B ( 1 < i < m) ( A D B ) => A < B t o g e t h e r w i t h t h e u s u a l t r a n s i t i v i t y r e l a t i o n s . I f t h e s e r e l a t i o n s f o r m a p a r t i a l o r d e r on t h e a l p h a b e t , A, ( i e (V A \u00E2\u0082\u00AC A) -t ( A < A ) ) , t h e t h e o r y i s c a l l e d a c y c l i c . N o r m a l t h e o r i e s , w h i c h a l w a y s have e x t e n s i o n s , a r e a l l a c y c l i c . T h o s e t h e o r i e s w i t h o u t e x t e n s i o n s w h i c h have so f a r been p r e s e n t e d ( c f [ R e i t e r 1 9 8 0 , 1 9 8 1 ] ) a r e c y c l i c . T h i s s u g g e s t s t h a t a c y c l i c d e f a u l t t h e o r i e s may a l w a y s have a t l e a s t one e x t e n s i o n . I f t h i s p r o v e s t o be t h e c a s e , i t s h o u l d be p o s s i b l e t o p r e c i s e l y D e f a u l t T ype H i e r a r c h i e s 58 s p e c i f y t h e s e m a n t i c s o f any s e m a n t i c network i n f e r e n c e s y s t e m i n terms o f a s e m i - n o r m a l d e f a u l t t h e o r y . Thus one c o u l d d e t e r m i n e j u s t what i n f e r e n c e s t h e s y s t e m was j u s t i f i e d i n m a k i n g . S i m i l a r l y , p r o v i d i n g t h e a c y c l i c i t y c o n d i t i o n s were met, t h e s y s t e m c o u l d be a s s u r e d t h a t t h e r e was a l w a y s a t l e a s t one e x t e n s i o n f o r t h e t h e o r y i t was w o r k i n g w i t h . T h i s r e s u l t w o u l d be c o m f o r t i n g t o t h o s e u s i n g s u c h a s y s t e m . O b s e r v a t i o n o f t h e c o n d i t i o n s w h i c h c a u s e t h e p r o c e d u r e t o c y c l e l e a d s t o t h e c o n j e c t u r e t h a t , f o r t h e c l a s s o f t h e o r i e s d e s c r i b e d a b o v e , t h e p r o c e d u r e p r e s e n t e d i n C h a p t e r 3 a l w a y s c o n v e r g e s . T h i s would p r o v i d e a d e t e r m i n i s t i c p r o c e d u r e f o r d e t e r m i n i n g t h e e x t e n s i o n s o f s u c h t h e o r i e s . 4.2 P a r a l l e l I n h e r i t a n c e M a c h i n e s The work d e s c r i b e d i n t h i s t h e s i s o r i g i n a l l y d e r i v e d f r o m an a t t e m p t t o use d e f a u l t h i e r a r c h i e s t o s p e c i f y t h e s e m a n t i c s o f i n h e r i t a n c e and c a n c e l l a t i o n t h e r e o f i n NETL, a p a r a l l e l m a c h i n e a r c h i t e c t u r e f o r r e p r e s e n t i n g s e m a n t i c n e t w o r k s . T h e r e had been s e v e r a l e f f o r t s made [Fahlman e t a l 1981, T o u r e t z k y 1981] t o p r o v i d e a mechanism f o r d e t e r m i n i n g i n h e r i t a n c e u s i n g a p a r a l l e l marker p a s s i n g a l g o r i t h m w i t h c o s t p r o p o r t i o n a l t o t h e \" h e i g h t \" o f t h e n e t w o r k . T h e s e e f f o r t s were p l a g u e d by t h e d i s c o v e r y o f p e c u l i a r c a s e s w h i c h i n v a l i d a t e d e a c h newly p r o p o s e d marker p a s s i n g a l g o r i t h m . I t was hoped t h a t , by e x p r e s s i n g t h e ad hoc r u l e s o f NETL w i t h i n t h e f o r m a l framework o f d e f a u l t l o g i c , t h e P a r a l l e l I n h e r i t a n c e M a c h i n e s 59 u n d e r l y i n g p r i n c i p l e s m i g h t be i l l u m i n a t e d , t h u s p a v i n g t h e way f o r d e v e l o p i n g a p r o v a b l y c o r r e c t i n f e r e n c e mechanism. T h i s work i m m e d i a t e l y b r o u g h t e n c o u r a g i n g f r u i t . I t was shown t h a t NETL i n h e r i t a n c e s t r u c t u r e s c o u l d be e x p r e s s e d as m o n a d i c , s e m i - n o r m a l , d e f a u l t t h e o r i e s . The f a c t t h a t u n r e s t r i c t e d i n h e r i t a n c e s t r u c t u r e s c a u s e d p r o b l e m s f o r t h e i r p a r a l l e l m a r k e r - p a s s i n g a l g o r i t h m s was n o t i c e d by Fahlman e t a l , and t h e s o - c a l l e d \" n a i v e \" scheme was d i s c a r d e d . E x a m i n a t i o n o f t h e c o r r e s p o n d i n g d e f a u l t t h e o r i e s r e v e a l e d t h e s o u r c e o f t h e p r o b l e m : t h e u n r e s t r i c t e d t h e o r i e s c o u l d have more t h a n one ( p o s s i b l y o r t h o g o n a l ) e x t e n s i o n . NETL's i n h e r i t a n c e mechanism had been t r y i n g t o d e r i v e a s e t o f b e l i e f s , i n one p a r a l l e l p a s s w i t h o u t l o o k a h e a d , w h i c h w o u l d a l l b e l o n g t o one o f t h e p o s s i b l e e x t e n s i o n s . S i n c e e x t e n s i o n membership i s n o t a l o c a l l y d e t e r m i n e d p r o p e r t y , i t was a p p a r e n t t h a t t h i s w o u l d be i m p o s s i b l e . NETL's a l l o w a b l e i n h e r i t a n c e s t r u c t u r e s were t h e n r e s t r i c t e d t o p r o h i b i t nodes f r o m w h i c h a l t e r n a t e p a t hways c o u l d l e a d t o c o n f l i c t i n g c o n c l u s i o n s . The e f f e c t o f t h e s e r e s t r i c t i o n s was t o e n s u r e t h a t t h e c o r r e s p o n d i n g d e f a u l t t h e o r y had e x a c t l y one e x t e n s i o n . A t t e m p t s t o d e v e l o p a p r o o f t h e o r y f o r t h e d e f a u l t l o g i c , so r e s t r i c t e d , w h i c h w o u l d c a p t u r e t h e p a r a l l e l i s m o f NETL met w i t h f r u s t r a t i o n . I t t u r n e d o u t t h a t any p a r a l l e l p r o o f t h e o r y w h i c h c o u l d c o r r e c t l y d e a l w i t h c a s e s l i k e t h a t shown i n f i g u r e 4.1 c o u l d n o t d e a l w i t h t h o s e l i k e f i g u r e 4.2, even t h o u g h when a c t i v a t e d f o r a p a r t i c u l a r A (eg a ) , b o t h have a u n i q u e e x t e n s i o n (namely: T h ( { A ( a ) , B ( a ) , C ( a ) , D ( a ) } ) ) . P a r a l l e l I n h e r i t a n c e M a c h i n e s 60 NETL G r a p h D e f a u l t T h e o r y W = U(a) } D = |A(x) : B (x) , B (x) : C (x) , C (x) ; D(x) , B(x) C ( x ) D(x) A(x) : E ( x ) , E ( x ) : -iF (x) A i D ( x ) } E ( x ) i F ( x ) J F i g u r e 4.1 - D must be a c t i v a t e d b e f o r e E . NETL G r a p h D e f a u l t T h e o r y W = {A(a) } D = |A(x) ; B (x) , B (x) : C (x) , C (x) : D (x) , B(x) C ( x ) D(x) A(x) : E(x) , E (x) : -iF (x) A i E (x) i E(x) n F ( x ) ' F i g u r e 4.2 \u00E2\u0080\u0094 E must be a c t i v a t e d b e f o r e D. T h i s i s b e c a u s e , i n F i g u r e 4.1, t h e \" m a r k e r s \" must r e a c h D by t h e t i m e t h e y r e a c h E . I n F i g u r e 4.2, t h e o p p o s i t e i s t r u e . Due t o t h e l o c a l i t y o f r e f e r e n c e i n NETL's p a r a l l e l marker p r o p a g a t i o n , t h e r e q u i r e d p r o p a g a t i o n p a t t e r n i s i m p o s s i b l e t o d e t e r m i n e i n p a r a l l e l . A new v e r s i o n o f i n h e r i t a n c e i n NETL has been d e v e l o p e d w h i c h d i s a l l o w s s u c h c o n s t r u c t s . T o u r e t z k y (1981) s t a t e s t h a t t h e added r e s t r i c t i o n s r e s u l t i n a p r o v a b l y c o r r e c t scheme. I f t h i s i s s o , i t w i l l be i n s t r u c t i v e t o d e t e r m i n e how t h e r e s t r i c t i o n s on w e l l - f o r m e d n e s s o f NETL i n h e r i t a n c e h i e r a r c h i e s w i l l a f f e c t t h e e x p r e s s i v e power o f t h e u n d e r l y i n g d e f a u l t l o g i c (and h e n c e o f N E T L ) . T h i s i n v e s t i g a t i o n has n o t y e t been u n d e r t a k e n . T r u t h M a i n t e n a n c e 61 4.3 T r u t h M a i n t e n a n c e Anyone f a m i l i a r w i t h t h e b e l i e f r e v i s i o n l i t e r a t u r e (see [ D o y l e and London 1980] f o r a s u r v e y ) w i l l n o t i c e c e r t a i n s i m i l a r i t i e s between t h e r e l a x a t i o n p r o c e s s c a r r i e d o u t by s u c h s y s t e m s d u r i n g \" t r u t h m a i n t e n a n c e \" and t h e i t e r a t i o n s o f t h e p r o c e d u r e p r e s e n t e d h e r e . The s i m i l a r i t y i s a l l t h e more c o m p e l l i n g when t h e i n - and o u t - h y p o t h e s e s i n t h e TMS j u s t i f i c a t i o n s a r e v i e w e d as t h e p r e r e q u i s i t e s and j u s t i f i c a t i o n s , r e s p e c t i v e l y , o f a d e f a u l t t h e o r y . I t may be t h a t a f o r m a l u n d e r s t a n d i n g o f t h e t r u t h m a i n t e n a n c e p r o c e s s c a n be r e a l i z e d by e x p l i c i t l y d e t a i l i n g t h i s c o r r e s p o n d e n c e . The g o a l o f t h i s r e s e a r c h would be t o show t h a t s u c h s y s t e m s a r e e s s e n t i a l l y c o n v e r g i n g on e x t e n s i o n s f o r some u n d e r l y i n g d e f a u l t t h e o r y . 4.4 T h e o r e t i c a l A n a l y s i s As has been m e n t i o n e d , t h e r e has been a d e a r t h o f f o r m a l s t u d y o f t h e r e l a t i o n s h i p s between t h e c a p a b i l i t i e s p r o v i d e d by t h e v a r i o u s a p p r o a c h e s . Due t o t h e l e v e l o f i n t e r e s t i n knowledge r e p r e s e n t a t i o n and r e a s o n i n g , t h e r e has been a p r o l i f e r a t i o n o f i d e a s . U n f o r t u n a t e l y , p r o p o n e n t s o f t h e s e i d e a s have n o t a l w a y s p r o v i d e d t h e d e g r e e o f r i g o u r f o r w h i c h one m i g h t hope. New schemes a r e c o n c e i v e d w i t h o u t c l e a r d e m o n s t r a t i o n s t h a t t h e y a r e s u p e r i o r t o (or even s i g n i f i c a n t l y T h e o r e t i c a l A n a l y s i s 62 d i f f e r e n t from) t h o s e a l r e a d y e x t a n t . R i g o u r o u s c o m p a r i s o n s o f a p p r o a c h e s would s e r v e n o t o n l y t o d e m o n s t r a t e w h i c h a r e b e s t s u i t e d t o p a r t i c u l a r p r o b l e m s , b u t t o p o i n t o u t w e a k n e s s e s . T h i s s t u d y m i g h t l e a d t o t h e abandonment o f some and t h e improvement o f o t h e r s t o make them more u n i v e r s a l l y a p p l i c a b l e . I t seems c l e a r t h a t much o f t h e work i n t h e f i e l d i s c l o s e l y i n t e r t w i n e d \u00E2\u0080\u0094 p e r h a p s n o t s u r p r i s i n g l y , c o n s i d e r i n g t h a t e v e r y -one i n v o l v e d has t h e same s e t o f p r o b l e m s w i t h w h i c h t o d e a l . I f t h i s i n t e r t w i n i n g c a n be u n r a v e l e d , i t s h o u l d p r o v i d e i n s i g h t i n t o o t h e r , more a p p r o p r i a t e , ways o f a t t a c k i n g t h e p r o b l e m s . A p p r o a c h i n g t h e p r o b l e m f r o m a d i f f e r e n t a n g l e , t h e r e has been a r i c h t r a d i t i o n o f s t u d y , d a t i n g back t o A r i s t o t l e , o f t h e p r o p e r t i e s o f t h e v a r i o u s m o d a l i t i e s ( c f [Lemmon 1 9 7 7 ] ) . The i n v e s t i g a t i o n s o f McDermott (1982) s u g g e s t t h a t t h e r e may be ways t o a p p l y t h e c l a s s i c a l modal l o g i c s t o t h e p r o b l e m s a d d r e s s e d by n o n - m o n o t o n i c and d e f a u l t l o g i c s . T h e r e a r e l i k e l y t o be many c o n t r i b u t i o n s w h i c h modal l o g i c c a n make t o t h i s domain o f i n q u i r y . D e f a u l t L o g i c a v o i d s t h e i n t r o d u c t i o n o f m o d a l i t i e s i n t o t h e l a n g u a g e . As n o t e d i n C h a p t e r 2, t h i s r e s u l t s i n a d v a n t a g e s and d i s a d v a n t a g e s . T h e r e i s , as y e t , no c h a r a c t e r i z a t i o n o f t h e c o s t s and b e n e f i t s o f s u c h an a p p r o a c h . F o r example, D e f a u l t L o g i c ' s i n a b i l i t y t o combine d e f a u l t s may be r e m e d i a b l e w i t h o u t s e r i o u s l y d i s t o r t i n g t h e f a b r i c o f t h e l o g i c . The i m p l i c a t i o n s o f s u c h a l t e r a t i o n s i n v i t e f u r t h e r i n v e s t i g a t i o n . C h a p t e r 5 C o n c l u s i o n 5.1 E v a l u a t i o n o f R e s u l t s The f o l l o w i n g d i s c u s s i o n p l a c e s t h i s work i n p e r s p e c t i v e . T h e r e a r e a v a r i e t y o f c r i t e r i a w h i c h c a n be a p p l i e d when d e t e r m i n i n g t h e s i g n i f i c a n c e o f t h e s e or any o t h e r t h e o r e t i c a l r e s u l t s . The m a i n d i m e n s i o n s c o n s i d e r e d w i l l be t h e power and g e n e r a l i t y o f t h e method and i t s a p p l i c a b i l i t y t o common p r o b l e m s . The i n t e n t i o n i s p r o v i d e an i n t u i t i o n a b o u t t h e s t r e n g t h s and s h o r t c o m i n g s w h i c h have been e n c o u n t e r e d . 5.1.1 F i n i t e n e s s R e s t r i c t i o n s As has been m e n t i o n e d , t h e method p r e s e n t e d i s a p p l i c a b l e o n l y t o d e f a u l t t h e o r i e s c o n s i s t i n g o f a f i n i t e s e t o f d e f a u l t s o v e r a f i n i t e a l p h a b e t . To t h e l o g i c i a n , t h i s may seem t o be a d i s q u i e t i n g s h o r t c o m i n g . In b o t h d a t a b a s e t h e o r y and common t y p e / I S - A h i e r a r c h i e s , however, t h e domain o f i n t e r e s t u s u a l l y i s (or i s t r e a t e d t o be) f i n i t e . The c a s e has been made i n t h i s t h e s i s and e l s e w h e r e ( c f R e i t e r 1978, 1978a, 1980, 1981) t h a t d e f a u l t l o g i c p r o v i d e s a s u i t a b l e f o r m a l i s m f o r d e a l i n g w i t h many o f t h e common p r o b l e m s e n c o u n t e r e d i n t h e s e a r e a s . I t c a n F i n i t e n e s s R e s t r i c t i o n s 64 be s e e n t h a t t h e r e i s a l a r g e c l a s s o f i n t e r e s t i n g p r o b l e m s t o w h i c h t h e method may be a p p l i e d . 5.1.2 I n f i n i t e T h e o r i e s I t may s t i l l be o f i n t e r e s t t o c o n s i d e r whether t h e r e i s a method f o r c o n s t r u c t i n g e x t e n s i o n s w h i c h i s n o t s u b j e c t t o f i n i t e n e s s r e s t r i c t i o n s . ^ T h e r e i s a t l e a s t one: R e i t e r (1980) has shown t h a t t h e r e i s a s e q u e n c e E g , E-^, ... s u c h t h a t oo U E- = E i f f t h e r e i s an e x t e n s i o n , E . F u r t h e r m o r e , he has i=0 d e m o n s t r a t e d t h a t E = Th(W U CONSEQUENTS(GD(E ,A) ) ) , where GD(E,A) a r e t h e g e n e r a t i n g d e f a u l t s o f E f r o m A d e s c r i b e d i n C h a p t e r 3. From t h i s , i t i s n o t d i f f i c u l t t o show t h a t t h e s e q u e n c e o f h | o b t a i n e d as i n D e f i n i t i o n 3.1, e x c e p t a d d i n g co , (GD(E,A) O (Dj - G D j ) ) a t each s t e p ( a t -[) , y i e l d s U h+ = E i=0 (=H-^) . The o n l y drawback o f t h i s a p p r o a c h i s t h a t i t i s c i r c -u l a r . E must be known t o d e t e r m i n e GD(E,A). T h i s i s n o t , t h e n , a c o m p u t a t i o n a l l y f e a s i b l e a p p r o a c h . The e x i s t e n c e o f one method f o r a r r i v i n g a t t h e e x t e n s i o n s o f an i n f i n i t e d e f a u l t t h e o r y may s u g g e s t t h a t t h e r e a r e o t h e r , more f e a s i b l e , a p p r o a c h e s . E x p e r i e n c e has shown t h a t t h e i m m e d i a t e l y a p p a r e n t o r p r o m i s i n g methods a l l f a i l t o a c h i e v e t h e d e s i r e d r e s u l t . T h i s a p p e a r s t o be b e c a u s e any n o n - c i r c u l a r method p o w e r f u l enough t o o b t a i n t h e r e s u l t c o r r e s p o n d i n g t o G i v e n t h a t e x t e n s i o n s a r e n o t g e n e r a l l y r e c u r s i v e l y e n u m e r a b l e , t h i s q u e s t i o n must be r e s t r i c t e d t o t h o s e t h e o r i e s w i t h r e c u r s i v e , o r a t l e a s t r e c u r s i v e l y e n u m e r a b l e , e x t e n s i o n s . _. I n f i n i t e T h e o r i e s 65 Lemma 3.3 f o r t h e i n f i n i t e c a s e c a n n o t y i e l d t h a t c o r r e s p o n d i n g t o Theorem 3.6, and v i c e v e r s a . Any p r o c e d u r e w h i c h g u a r a n t e e s i n c l u d i n g e v e r y a p p l i c a b l e d e f a u l t seems u n a b l e t o f i n d a l l e x t e n s i o n s . T h i s seems t o be a c o n s e q u e n c e o f t h e i n t e r a c t i o n s between d e f a u l t s , and o f n o n - m o n o t o n i c i t y . Of c o u r s e , an a l g o r i t h m c o u l d c o n s i s t o f a b r e a d t h - f i r s t s e a r c h f o r \" R e i t e r ' s S e q u e n c e \" , b u t i t i s n o t c l e a r what v a l u e b r e a d t h - f i r s t s e a r c h has i n a domain w i t h a p o t e n t i a l l y i n f i n i t e b r a n c h i n g f a c t o r . W h i l e t h i s does n o t c o n s t i t u t e a p r o o f , h o p e f u l l y t h e r e a d e r i s l e f t w i t h an i m p r e s s i o n o f t h e i m p r o b a b i l i t y o f o v e r c o m i n g t h e s e l i m i t a t i o n s w i t h i n t h e c o n f i n e s o f any t r a d i t i o n a l , d e t e r m i n i s t i c m odel o f c o m p u t a t i o n . T h e s e p e s s i m i s t i c i n d i c a t i o n s and t h e wide a p p l i c a b i l i t y o f t h e f i n i t e method p r o v i d e l i t t l e m o t i v a t i o n f o r p u r s u i n g t h e m a t t e r f u r t h e r . 5.1.3 C o m p u t a t i o n a l C o n s i d e r a t i o n s The q u e s t i o n o f t h e c o m p u t a t i o n a l u t i l i t y o f t h e r e s u l t s i s p e r h a p s t h e h a r d e s t t o a d d r e s s . Any f o r m a l i s m r o o t e d , as t h i s one i s , i n f i r s t - o r d e r l o g i c i s bound t o be f r a u g h t w i t h c o m p u t a t i o n a l l y e x p e n s i v e o p e r a t i o n s . As t h e method s t a n d s , i t must compute t h e l o g i c a l c l o s u r e o f each h j , o f w h i c h t h e r e a r e an i n f i n i t e number. Of c o u r s e , i f t h e t h e o r y i s f i n i t e , a l l beyond some f i n i t e number w i l l be i d e n t i c a l and need n o t be computed. C o m p u t i n g t h e c l o s u r e i s s t i l l a p o t e n t i a l l y e x p e n s i v e , o r even n o n - t e r m i n a t i n g , o p e r a t i o n . C o m p u t a t i o n a l C o n s i d e r a t i o n s 66 I t may be p o s s i b l e t o h e u r i s t i c a l l y l i m i t t h i s c o m p u t a t i o n , d e r i v i n g o n l y \" r e l e v a n t \" p o r t i o n s o f t h e e x t e n s i o n . F o r example, a l l t a u t o l o g i e s a r e c o n t a i n e d i n e v e r y e x t e n s i o n \u00E2\u0080\u0094 b u t t h e y r a r e l y need t o be computed. T h e r e may be i n t e r e s t i n g domains where c l o s u r e i s n o t n e c e s s a r y . IS-A h i e r a r c h i e s w i t h e x c e p t i o n s i m m e d i a t e l y s u g g e s t t h e m s e l v e s , g i v e n t h e ways i n w h i c h t h e s e have t r a d i t i o n a l l y been employed. A n o t h e r way t o a d d r e s s t h i s p r o b l e m i s t o r e f o r m u l a t e t h e p r o c e d u r e s l i g h t l y . The c o m p u t a t i o n o f t h e l o g i c a l c l o s u r e i n t h e c o n s t r u c t i o n o f H n and each h^ c a n be a v o i d e d i f t h e d e f i n i t i o n o f i s r e p l a c e d w i t h : / / A : B-i , . . . ,Bm DI = {6\ 6 = \u00E2\u0080\u0094 e D, hj f- A, w ( h j U H^_1) Y -iBlf...,-,Bm} S i n c e A must be f i n i t e , t h e r e f e r e n c e s t o p r o v a b i l i t y (|-) and u n p r o v a b i l i t y (Y) a r e a l l d e c i d a b l e , and t h e p r o c e d u r e becomes an a l g o r i t h m . The r e s u l t i n g H n , s h o u l d t h e a l g o r i t h m c o n v e r g e , i s no l o n g e r an e x t e n s i o n , s i n c e e x t e n s i o n s must be l o g i c a l l y c l o s e d . T h ( H n ) w i l l be an e x t e n s i o n . F o r common a p p l i c a t i o n s , however, H n may be s u f f i c i e n t . E v e n w i t h t h i s r e f o r m u l a t i o n , c o n s i s t e n c y t e s t s a r e e x p e n s i v e and i n d i s p e n s i b l e ( R e i t e r 1 9 8 0 ) . T h e r e i s a g r e a t d e a l o f work b e i n g done on ways t o c i r c u m v e n t t h e p r o b l e m s p r e s e n t e d b o t h by t h e c o m b i n a t o r i a l e x p l o s i o n and t h e i n h e r e n t u n d e c i d a b i l i t y o f t h e u n d e r l y i n g s y s t e m s . T h e s e i n c l u d e t h e o r e m p r o v e r s w h i c h c o n s t r a i n t h e e x p l o s i o n (c_f C - O r d e r e d L i n e a r R e s o l u t i o n [ R e i t e r 1 9 7 1 ] , SL R e s o l u t i o n [ K o w a l s k i and Kuehner 1 9 7 1 ] ) , and v a r i o u s C o m p u t a t i o n a l C o n s i d e r a t i o n s 67 h e u r i s t i c a p p r o a c h e s s u c h as r e s o u r c e l i m i t e d c o m p u t a t i o n ( c f KRL [Bobrow and W i n o g r a d 1977, W i n o g r a d 1 9 8 1 ] ) . I t i s beyond t h e s c o p e o f t h i s t h e s i s t o e n t e r i n t o a d i s c u s s i o n o f s u c h m ethods. I t r e m a i n s t o be se e n whether t e c h n i q u e s w i l l be f o u n d w h i c h c a n make d e f a u l t r e a s o n i n g i n g e n e r a l , and t h e s e r e s u l t s i n p a r t i c u l a r , c o m p u t a t i o n a l l y a t t r a c t i v e . F i n a l l y , t h e f a c t t h a t Theorem 3.6 shows t h a t e x t e n s i o n s c a n a l w a y s be a r r i v e d a t i n a s i n g l e i t e r a t i o n s u g g e s t s t h a t t h e p r o c e d u r e i s t o o e l a b o r a t e and c o u l d be s i m p l i f i e d . Not e v e r y s e q u e n c e c o n v e r g e s i m m e d i a t e l y , however. The p r o c e d u r e o u t l i n e d i s g e n e r a l enough t o r e c o v e r f r o m n o n - o p t i m a l c h o i c e s o f w h i c h d e f a u l t s t o a p p l y . I t was a l s o d e s i g n e d t o be r o b u s t enough t o w i t h s t a n d t h e \" d i s c o v e r y \" o f new c o n s e q u e n c e s o f a t h e o r y \u00E2\u0080\u0094 t h e t y p e o f e f f e c t w h i c h m i g h t be e x p e c t e d were t h e r e q u i r e d c o m p u t a t i o n s h e u r i s t i c a l l y l i m i t e d i n some f a s h i o n . 5.2 Summary A s u r v e y o f f o r m a l i s m s f o r n o n - m o n o t o n i c r e a s o n i n g has been p r e s e n t e d , p r o v i d i n g a s k e t c h o f t h e \" s t a t e o f t h e a r t \" i n t h e f i e l d . R e i t e r \" s l o g i c f o r d e f a u l t r e a s o n i n g has been d i s c u s s e d i n d e t a i l . A p r o c e d u r e f o r d e t e r m i n i n g t h e e x t e n s i o n s o f g e n e r a l f i n i t e d e f a u l t t h e o r i e s has been d e m o n s t r a t e d . The p o t e n t i a l i m p a c t o f t h e p r o c e d u r e on some o f t h e o t h e r r e s e a r c h i n t h e f i e l d has been e x p l o r e d , i n d i c a t i n g some p r o m i s i n g a r e a s f o r f u t u r e r e s e a r c h . G r o u n d s f o r c a u t i o u s Summary 6 8 o p t i m i s m a b o u t t h e t r a c t i b i l i t y o f d e f a u l t t h e o r i e s c a p a b l e o f r e p r e s e n t i n g a wide v a r i e t y o f common s i t u a t i o n s have been p r o v i d e d . T h i s o p t i m i s m may n o t t u r n o u t t o be w e l l - f o u n d e d , b u t i t i s hoped t h a t t h i s t h e s i s may p r o v i d e t h e groundwork f o r f u r t h e r d e v e l o p m e n t i n t h i s a r e a . B i b l i o g r a p h y Bobrow, D.G. and W i n o g r a d , T. (197 7 ) , \"An O v e r v i e w o f KRL-0, a Knowledge R e p r e s e n t a t i o n L a nguage\", C o g n i t i v e S c i e n c e 1 ( 1 ) . C l a r k , K.L. (1 9 7 8 ) , \" N e g a t i o n a s F a i l u r e \" , i n L o g i c and D a t a b a s e s , H. G a l l a i r e and J . M i n k e r ( e d s . ) , P lenum P r e s s , New Y o r k . Codd, E . F . (1972), \" R e l a t i o n a l C o m p l e t e n e s s o f D a t a B a s e S u b l a n g u a g e s \" , i n R. R u s t i n ( e d . ) , D a t a B a s e S y s t e m s , P r e n t i c e - H a l l . D a v i s , M. (1 9 8 0 ) , \"The M a t h e m a t i c s o f N o n - M o n o t o n i c R e a s o n i n g \" , A r t i f i c i a l I n t e l l i g e n c e 13, N o r t h - H o l l a n d . D o y l e , J . (197 9 ) , A T r u t h M a i n t e n a n c e S y s tem , A l Memo 521, MIT A r t i f i c i a l I n t e l l i g e n c e L a b , C a m b r i d g e , Mass. D o y l e , J . and Lon d o n , P. (1980 ) , A S e l e c t e d D e s c r i p t o r - I n d e x e d B i b l i o g r a p h y t o t h e L i t e r a t u r e on B e l i e f R e v i s i o n , A l Memo 56 8, MIT, C a m b r i d g e , Mass. F a h l m a n , S.E. (1 9 7 9 ) , NETL; A S y s t e m f o r R e p r e s e n t i n g and U s i n g R e a l - W o r l d Knowledge, MIT P r e s s , C a m b r i d g e , Mass. F a h l m a n , S.E., T o u r e t z k y , D.S., and von Roggen, W. (1 9 8 1 ) , \" C a n c e l l a t i o n i n a P a r a l l e l S e m a n t i c Network\", P r o c . S e v e n t h I n t e r n a t i o n a l J o i n t C o n f e r e n c e on A r t i f i c i a l I n t e l l i g e n c e . G r i c e , H.P. (1 9 7 5 ) , \" L o g i c and C o n v e r s a t i o n \" , i n S y n t a x and S e m a n t i c s , V o l 3: Sp e e c h A c t s , P. C o l e and J . L . Morgan ( e d s . ) , A c a d e m i c P r e s s . H a y e s , P . J . (197 3 ) , \"The Frame P r o b l e m and R e l a t e d P r o b l e m s i n A r t i f i c i a l I n t e l l i g e n c e \" , i n A r t i f i c i a l and Human T h i n k i n g , A. E l i t h o r n and D. J o n e s ( e d s . ) , J o s s e y - B a s s I n c . , San F r a n c i s c o . H a y e s , P . J . (197 7 ) , \" I n D e f e n s e o f L o g i c \" , P r o c . F i f t h I n t e r n a t i o n a l J o i n t C o n f e r e n c e on A r t i f i c i a l I n t e l l i g e n c e . H e w i t t , C. (197 2 ) , D e s c r i p t i o n and T h e o r e t i c a l A n a l y s i s ( U s i n g Schemata) o f PLANNER; A Language f o r P r o v i n g Theorems and M a n i p u l a t i n g M o d e l s i n a Rob o t , A l Memo 251, MIT P r o j e c t MAC, C a m b r i d g e , Mass. Hughes, G.E. and C r e s s w e l , M.J. (1968 ) , An I n t r o d u c t i o n t o M o d a l L o g i c , Methuen and Co. L t d . , L ondon. 69 70 K o w a l s k i , R.A. and Ku e h n e r , D. (1971 ) , \" L i n e a r R e s o l u t i o n w i t h S e l e c t i o n F u n c t i o n \" , A r t i f i c i a l I n t e l l i g e n c e 2, N o r t h - H o l l a n d . K r a m o s i l , I . (197 5 ) , \"A No t e on D e d u c t i o n R u l e s w i t h N e g a t i v e P r e m i s e s \" , P r o c . F o u r t h I n t e r n a t i o n a l J o i n t C o n f e r e n c e on A r t i f i c i a l I n t e l l i g e n c e . Lemmon, E . J . (1 9 7 7 ) , An I n t r o d u c t i o n t o M o d a l L o g i c , w i t h Dana S c o t t , K. S e g e r b e r g ( e d . ) , A m e r i c a n P h i l o s o p h i c a l Q u a r t e r l y , Monograph No. 11, O x f o r d . M c A l l e s t e r , D.A. (1978 ) , A T h r e e - V a l u e d T r u t h M a i n t e n a n c e S y s t e m , AI Memo 473, MIT, C a m b r i d g e , Mass. M c A l l e s t e r , D.A. (1980 ) , An O u t l o o k On T r u t h M a i n t e n a n c e , AI Memo 551, MIT, C a m b r i d g e , Mass. M c C a r t h y , J . (1 9 7 7 ) , \" E p i s t e m o l o g i c a l P r o b l e m s o f A r t i f i c i a l I n t e l l i g e n c e \" , P r o c . F i f t h I n t e r n a t i o n a l J o i n t C o n f e r e n c e on A r t i f i c i a l I n t e l l i g e n c e . M c C a r t h y , J . (198 0 ) , \" C i r c u m s c r i p t i o n \u00E2\u0080\u0094 A Form o f N o n - M o n o t o n i c R e a s o n i n g \" , A r t i f i c i a l I n t e l l i g e n c e 13, N o r t h - H o l l a n d . M c C a r t h y , J . and Ha y e s , P . J . (1969), \"Some P h i l o s o p h i c a l P r o b l e m s f r o m t h e S t a n d p o i n t o f A r t i f i c i a l I n t e l l i g e n c e \" , i n M a c h i n e I n t e l l i g e n c e 4, B. M e l t z e r and D. M i c h i e ( e d s . ) , E d i n b u r g h U n i v e r s i t y P r e s s , E d i n b u r g h . McDermott, D. and D o y l e , J . (198 0 ) , \"Non-Monotonic L o g i c I \" , A r t i f i c i a l I n t e l l i g e n c e 13, N o r t h - H o l l a n d . M cDermott, D. (1982 ) , \"Non-Monotonic L o g i c I I \" , J.ACM 2 9 ( 1 ) . M e n d e l s o n , E . (196 4 ) , I n t r o d u c t i o n t o M a t h e m a t i c a l L o g i c , Van N o s t r a n d R e i n h o l d , New Y o r k . M i n s k y , M. ( 1 9 7 5 ) , \"A Framework f o r R e p r e s e n t i n g Knowledge\", i n The P s y c h o l o g y o f Computer V i s i o n , P. W i n s t o n ( e d . ) , M c G r a w - H i l l , New Y o r k . R a p h a e l , B. (1 9 7 1 ) , \"The Frame P r o b l e m i n P r o b l e m - S o l v i n g \" , i n A r t i f i c i a l I n t e l l i g e n c e and H e u r i s t i c Programming, N.V. F i n d l e r and B. M e l t z e r ( e d s . ) , E d i n b u r g h U n i v e r s i t y P r e s s , E d i n b u r g h . R e i t e r , R. (197 8 ) , \"On C l o s e d W o r l d D a t a B a s e s \" , i n L o g i c and D a t a b a s e s , H. G a l l a i r e and J . M i n k e r ( e d s . ) , Plenum P r e s s , New Y o r k . R e i t e r , R. (1 9 7 8 a ) , \"On R e a s o n i n g By D e f a u l t \" , P r o c . S e c o n d Symp. on T h e o r e t i c a l I s s u e s i n N a t u r a l Language P r o c e s s i n g , U r b a n n a , I l l i n o i s . 71 R e i t e r , R. ( 1 9 8 0 ) , \"A L o g i c F o r D e f a u l t R e a s o n i n g \" , A r t i f i c i a l I n t e l l i g e n c e ( 1 3 ) , N o r t h - H o l l a n d . R e i t e r , R. and C r i s c u o l o , G. (1981), \"On I n t e r a c t i n g D e f a u l t s \" , P r o c . S e v e n t h I n t e r n a t i o n a l J o i n t C o n f e r e n c e on A r t i f i c i a l I n t e l l i g e n c e . R e i t e r , R. ( 1 9 8 1 a ) , \"Towards a L o g i c a l R e c o n s t r u c t i o n o f R e l a t i o n a l D a t a b a s e T h e o r y \" , M a n u s c r i p t . R o b e r t s , R.B. and G o l d s t e i n , I . (1977), The FRL M a n u a l , AI Memo 409, MIT, C a m b r i d g e , Mass. R o b i n s o n , J.A. ( 1 9 6 5 ) , \"A M a c h i n e O r i e n t e d L o g i c B a s e d on t h e R e s o l u t i o n P r i n c i p l e \" , J.ACM 12. R o u s s e l , P. ( 1 9 7 5 ) , PROLOG, Ma n u e l de R e f e r e n c e e t d ' U t i l i s a t i o n , Group d 1 I n t e l l i g e n c e A r t i f i c i e l l e , U.E.R. de M a r s e i l l e , F r a n c e . S a n d e w a l l , E . ( 1 9 7 2 ) , \"An A p p r o a c h t o t h e Frame P r o b l e m and I t s I m p l e m e n t a t i o n \" , i n M a c h i n e I n t e l l i g e n c e 7, B. M e l t z e r and D. M i c h i e ( e d s . ) , E d i n b u r g h U n i v e r s i t y P r e s s , E d i n b u r g h . S c h u b e r t , L.K. ( 1 9 7 6 ) , \" E x t e n d i n g t h e E x p r e s s i v e Power o f S e m a n t i c N e t w o r k s \" , A r t i f i c i a l I n t e l l i g e n c e 7 ( 2 ) , N o r t h - H o l l a n d . T o u r e t z k y , D. (1981), p e r s o n a l c o m m u n i c a t i o n . W i n o g r a d , T. ( 1 9 8 0 ) , \" E x t e n d e d I n f e r e n c e Modes i n R e a s o n i n g \" , A r t i f i c i a l I n t e l l i g e n c e 13, N o r t h - H o l l a n d . Woods, W.A. ( 1 9 7 5 ) , \"What's i n a L i n k ? \" , R e p r e s e n t a t i o n and U n d e r s t a n d i n g , A c a d e m i c P r e s s . APPENDIX A D i c t i o n a r y o f Symbols Symbol I n t e r p r e t a t i o n O S e t i n t e r s e c t i o n U S e t u n i o n S e t d i f f e r e n c e 0 The empty s e t { } The empty s e t C P r o p e r s u b s e t Not a p r o p e r s u b s e t C S u b s e t Not a s u b s e t 6 I s an e l e m e n t o f 0 I s n o t an e l e m e n t o f | S e t q u a l i f i c a t i o n ( r e a d \" s u c h t h a t \" ) i f f I f and o n l y i f => I t f o l l o w s t h a t D L o g i c a l I m p l i c a t i o n A L o g i c a l And V L o g i c a l Or -\u00C2\u00BB L o g i c a l N o t 3 E x i s t e n t i a l q u a n t i f i e r V U n i v e r s a l q u a n t i f i e r 72 73 P r e c e e d i n g q u a n t i f i e r s b i n d t o t h e end o f t h e s e n t e n c e o r f i r s t e n c l o s i n g r i g h t p a r e n t h e s i s P r o v a b i l i t y r e l a t i o n N o n - p r o v a b i l i t y "@en . "Thesis/Dissertation"@en . "10.14288/1.0051826"@en . "eng"@en . "Computer Science"@en . "Vancouver : University of British Columbia Library"@en . "University of British Columbia"@en . "For non-commercial purposes only, such as research, private study and education. Additional conditions apply, see Terms of Use https://open.library.ubc.ca/terms_of_use."@en . "Graduate"@en . "Finite default theories"@en . "Text"@en . "http://hdl.handle.net/2429/23138"@en .