UBC Theses and Dissertations

UBC Theses Logo

UBC Theses and Dissertations

The linear resolution theorem prover Chan, Nelson Hin-Fai 1984

Your browser doesn't seem to have a PDF viewer, please download the PDF to view this item.

Item Metadata

Download

Media
831-UBC_1984_A6_7 C44.pdf [ 3.43MB ]
Metadata
JSON: 831-1.0051861.json
JSON-LD: 831-1.0051861-ld.json
RDF/XML (Pretty): 831-1.0051861-rdf.xml
RDF/JSON: 831-1.0051861-rdf.json
Turtle: 831-1.0051861-turtle.txt
N-Triples: 831-1.0051861-rdf-ntriples.txt
Original Record: 831-1.0051861-source.json
Full Text
831-1.0051861-fulltext.txt
Citation
831-1.0051861.ris

Full Text

THE LINEAR RESOLUTION THEOREM PROVER by NELSON HIN-FAI^CHAN B . S c , U n i v e r s i t y Of Western O n t a r i o , 1982 A THESIS SUBMITTED IN PARTIAL FULFILMENT OF THE REQUIREMENTS FOR THE DEGREE OF MASTER OF SCIENCE in THE FACULTY OF GRADUATE STUDIES Department Of Computer Science We accept t h i s t h e s i s as conforming to the r e q u i r e d ^ t a n d a r d THE UNIVERSITY OF BRITISH COLUMBIA October 1984 (c) Nelson H i n - F a i Chan, 1984 In p r e s e n t i n g t h i s t h e s i s 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 U n i v e r s i t y of B r i t i s h Columbia, I agree that the L i b r a r y s h a l l make i t f r e e l y a v a i l a b l e f o r r e f e r e n c e and study. I f u r t h e r agree that p e r m i s s i o n f o r e x t e n s i v e copying of t h i s t h e s i s f o r s c h o l a r l y purposes may be granted by the Head of my Department or by h i s or her r e p r e s e n t a t i v e s . I t i s understood that copying or p u b l i c a t i o n of t h i s t h e s i s f o r f i n a n c i a l gain s h a l l not be allowed without my w r i t t e n p e r m i s s i o n . Department of Computer Science The U n i v e r s i t y of B r i t i s h Columbia 2075 Wesbrook Place Vancouver, Canada V6T 1W5 Date: October 15, 1984 A b s t r a c t A r e s o l u t i o n - b a s e d theorem prover (LRTP) has been b u i l t on the PROLOG/MTS system. The LRTP i s designed f o r studying the performance of three r e s o l u t i o n s t r a t e g i e s , namely, l i n e a r input r e s o l u t i o n , l i n e a r r e s o l u t i o n , and ordered l i n e a r d e duction. It allows the user to perform experiments on the three s t r a t e g i e s i n combination with o t h e r s . Furthermore, the user has c o n t r o l over the environment i n which the theorem i s proved. The number of u n i f i c a t i o n s i n v o l v e d i n the search f o r a proof i s used as a measure of performance. i i i T able of Contents 1 . I n t r o d u c t i o n 1 1.1 H i s t o r i c a l Backgounds Of Automatic Deduction 2 1 . 2 O u t l i n e 3 2 . Logic 5 2.1 P r o p o s i t i o n a l L o g i c 5 2.2 F i r s t - o r d e r Logic 8 2.3 L o g i c As A R e p r e s e n t a t i o n Scheme 10 2.4 D e s c r i p t i v e Adequacy Of F i r s t - o r d e r Logic 11 2.5 D e c i s i o n Problem For F i r s t - o r d e r Logic 12 3. The R e s o l u t i o n P r i n c i p l e 14 3.1 The R e s o l u t i o n P r i n c i p l e For P r o p o s i t i o n a l Logic 14 3.2 The R e s o l u t i o n P r i n c i p l e For F i r s t - o r d e r Logic 15 3.2.1 Conversion Of Wffs To Clauses 15 3.2.2 S u b s t i t u t i o n And U n i f i c a t i o n 18 3.2.3 F a c t o r i n g 20 3.2.4 D e f i n i t i o n Of Resolvent For F i r s t - o r d e r Logic 21 4. R e s o l u t i o n R e f u t a t i o n s 23 4.1 B a s i s Of R e f u t a t i o n s 23 4.2 The B a s i c A l g o r i t h m For R e s o l u t i o n R e f u t a t i o n 24 4.3 R e s o l u t i o n S t r a t e g i e s 26 4.3.1 B r e a d t h - f i r s t S t r a t e g y 27 4.3.2 S e t - o f - s u p p o r t S t r a t e g y 28 4.3.3 L i n e a r R e s o l u t i o n 30 4.3.4 L i n e a r Input R e s o l u t i o n And U n i t R e s o l u t i o n 32 4.3.5 Ordered L i n e a r Deduction 34 i v 4.4 D e l e t i o n S t r a t e g i e s 37 4.4.1 D e l e t i o n Of T a u t o l o g i e s . . 38 4.4.2 Subsumption 39 5. The L i n e a r R e s o l u t i o n Theorem Prover 40 5.1 O r g a n i z a t i o n Of The LRTP 41 5.1.1 The Database 41 5.1.2 The Command I n t e r p r e t e r 42 5.1.3 The T r a n s l a t o r '. 42 5.1.4 The R e f u t a t i o n Module 43 5.1.5 The D e l e t i o n Module 46 5.1.6 The U n i f i c a t i o n Module 47 5.2 The LRTP Versus The P r o l o g I n t e r p r e t e r 47 5.2.1 Completeness 48 5.2.2 U n i f i c a t i o n 48 5.2.3 Termination 49 5.2.4 D e l e t i o n S t r a t e g i e s . 49 5.2.5 Measure Of Performance 49 5.2.6 S h o r t e s t L i n e a r R e f u t a t i o n 49 6. C o n c l u s i o n 50 BIBLIOGRAPHY 52 APPENDIX A - LRTP User's Manual 54 APPENDIX B - LRTP Program L i s t i n g 65 L i s t of F i g u r e s v F i g u r e 1 - I l l u s t r a t i o n of B r e a d t h - f i r s t S t r a t e g y 29 F i g u r e 2 - I l l u s t r a t i o n of S e t - o f - s u p p o r t S t r a t e g y 29 F i g u r e 3 - R e f u t a t i o n produced by a L i n e a r R e s o l u t i o n 31 F i g u r e 4 - S i m p l i f i e d form of a L i n e a r Deduction.. 31 F i g u r e 5 - I n c o r p o r a t i o n of S e t - o f - s u p p o r t S t r a t e g y i n t o a L i n e a r R e s o l u t i o n 32 F i g u r e 6 - I l l u s t r a t i o n of a Unit R e s o l u t i o n 33 F i g u r e 7 - I l l u s t r a t i o n of a OL-deduction 36 F i g u r e 8 - Search t r e e generated by r e s o l u t i o n 38 F i g u r e 9 - I n t e r n a l o r g a n i z a t i o n of the LRTP 41 v i Acknowledgement I would l i k e to thank Dr. R. R e i t e r f o r s u p e r v i s i n g my r e s e a r c h and f o r h i s comments on t h i s document. Thanks a l s o to Dr. H. Abramson f o r reading and commenting on the f i n a l d r a f t . 1 Chapter 1. I n t r o d u c t i o n When an Al system has a complete d e s c r i p t i o n of the o b j e c t s , p r o p e r t i e s and r e l a t i o n s of a problem s i t u a t i o n , then i t can answer any q u e s t i o n by e v a l u a t i o n . However, there are some q u e r i e s that r e q u i r e the system to be able to deduce answers. For i n s t a n c e , suppose the system was t o l d that " A l l b i r d s have wings" and " A l l r o b i n s are b i r d s " . If we then ask i t "Do r o b i n s have wings ?", the system can answer the query by means of deduction, without having to check whether each " i n d i v i d u a l r o b i n has wings or not. I t has been a c e n t r a l problem i n Al re s e a r c h to make computers deduce from given bodies of f a c t s . Any attempts to address t h i s problem r e q u i r e choosing f i r s t , a r e p r e s e n t a t i o n f o r the given f a c t s and secondly, methods f o r drawing c o n c l u s i o n s . McCarthy and Hayes[l969] d i v i d e d the Al problem i n t o two p a r t s : the e p i s t e m o l o g i c a l part and the h e u r i s t i c p a r t . The former p a r t was d e f i n e d as determining "what kinds of f a c t s about the world are a v a i l a b l e to an observer with given o p p o r t u n i t i e s to observe, how these f a c t s can be represented i n the memory of a computer, and what r u l e s permit l e g i t i m a t e c o n c l u s i o n s to be drawn from these f a c t s " [McCarthy,1977]. The l a t t e r p a r t d e a l s with the is s u e of p r o c e s s i n g , of us i n g the knowledge once a r e p r e s e n t a t i o n scheme has been chosen. Throughout t h i s a r t i c l e , f i r s t - o r d e r l o g i c i s used as the r e p r e s e n t a t i o n scheme, whereas the r e s o l u t i o n p r i n c i p l e i s used 2 as the r u l e of i n f e r e n c e . 1.1 H i s t o r i c a l Backgrounds Of Automatic Deduction Automatic deduction, or mechanical theorem-proving, has been an important su b j e c t i n A l s i n c e i t s e a r l i e s t day. In f a c t , the d e s i r e to f i n d a g e n e r a l d e c i s i o n procedure to prove theorems dates back to Leibniz(1646-1716); i t was f u r t h e r r e v i v e d by Peano and subsequently by H i l b e r t . The foundation of mechanical theorem-proving was e s t a b l i s h e d by Herbrand i n 1930, however h i s method was i m p r a c t i c a l to apply u n t i l the i n v e n t i o n of computers. Gilmore[1960] was one of the persons who attempted to implement Herbrand's procedure on a computer. A few months l a t e r , h i s method was improved by Davis and Putnam[1960], but t h e i r improvement was s t i l l i n s u f f i c i e n t . A major breakthrough i n the development of automatic deduction techniques was made by Robinson i n 1965. In h i s landmark paper, he i n t r o d u c e d a simple and l o g i c a l l y complete method f o r proving theorems i n f i r s t - o r d e r p r e d i c a t e c a l c u l u s . T h i s method i s much more e f f i c i e n t than the e a r l i e r procedures. Since then, many refinements were proposed to f u r t h e r improve i t s performance. Robinson's procedure and those r e f i n e d ones are c a l l e d r e s o l u t i o n procedures s i n c e a l l of them are based on the same r u l e of i n f e r e n c e , the r e s o l u t i o n p r i n c i p l e . The e a r l y r e s e a r c h of automatic theorem-proving was c o n s i d e r e d as e x e r c i s e s i n expert p r o b l e m - s o l v i n g : the Logic T h e o r i s t proposed by Newell and Simon[l956] was regarded as an expert i n p r o p o s i t i o n a l l o g i c and G e l e r n t e r ' s 3 theorem-prover[1963] an expert in elementary geometery. However, with the i n t r o d u c t i o n of r e s o l u t i o n , a t t i t u d e s toward automatic deduction was d r a m a t i c a l l y changed. T h i s i s because the r e s o l u t i o n method was so powerful that i t c o u l d be used to b u i l d a completely domain-independent pr o b l e m - s o l v e r . 1.2 O u t l i n e T h i s t h e s i s i n v o l v e s implementing some r e f i n e d proof procedures, d e r i v e d from the r e s o l u t i o n p r i n c i p l e , to prove theorems in f i r s t - o r d e r l o g i c . Since f i r s t - o r d e r l o g i c i s used as the r e p r e s e n t a t i o n scheme f o r t h i s t h e s i s , Chapter 2 i s devoted to the i n t r o d u c t i o n of l o g i c . I t c o n s i s t s of two p a r t s : the f i r s t p a r t d e c r i b e s p r o p o s i t i o n a l l o g i c and the second p a r t f i r s t - o r d e r l o g i c (extension of p r o p o s i t i o n a l l o g i c ) . Chapter 3 i n t r o d u c e s the r e s o l u t i o n p r i n c i p l e . Again, i t has two major p a r t s . The f i r s t p a r t i s concerned with the r e s o l u t i o n p r i n c i p l e f o r p r o p o s i t i o n a l l o g i c . And then, the p r i n c i p l e i s extended to f i r s t - o r d e r l o g i c i n the second p a r t . Chapter 4 i n t r o d u c e s the concept of r e f u t a t i o n and how v a r i o u s r e s o l u t i o n s t r a t e g i e s can be a p p l i e d i n a r e f u t a t i o n system. Chapter 5 d e s c r i b e s the o r g a n i z a t i o n of the theorem-prover (LRTP) being implemented, and then a comparison between the LRTP and the P r o l o g system f o l l o w . 4 Chapter 6 c o n c l u d e s what has been implemented i n the LRTP and g i v e s s u g g e s t i o n f o r f u r t h e r r e s e a r c h . 5 Chapter 2. Logic The study of reasoning and knowledge o r i g i n a t e s with the a n c i e n t Greeks. F o l l o w i n g t h e i r e a r l y e f f o r t s , the study was f o r m a l i z e d i n the l a t t e r h a l f of the n i n e t e e n t h century and has s i n c e developed i n t o the p h i l o s o p h i c a l and mathematical study of l o g i c . 2.1 P r o p o s i t i o n a l Logic P r o p o s i t i o n a l l o g i c i s the simplest form of l o g i c . A p r o p o s i t i o n i s a d e c l a r a t i v e sentence that can be e i t h e r true or f a l s e , but not both. For example, "The book i s red" and "One p l u s one equals two" are p r o p o s i t i o n s . For convenience, symbols can be used to denote p r o p o s i t i o n s and are c a l l e d atoms. We can combine simple p r o p o s i t i o n s to form compound p r o p o s i t i o n s by using f i v e l o g i c a l c o n n e c t i v e s . These c o n n e c t i v e s a r e : ->(not), \ / ( o r ) , A ( a n d ) , -> ( i f . . t h e n ) , and <-> ( i f and only i f ) . The meanings of the f i v e c o n n e c t i v e s are as f o l l o w s : If G and H are formulas, -•G i s true i f f G i s f a l s e , G V H i s true i f f e i t h e r G or H i s true or both are t r u e , G A H i s true i f f both G and H are t r u e , G->H i s true i f f H i s t r u e or G i s f a l s e , G<->H i s true i f f both G and H are true or both are f a l s e . 6 Note that (GVH) and (GA H) are r e s p e c t i v e l y , c a l l e d the d i s j u n c t i o n and the c o n j u n c t i o n of G and H. An e x p r e s s i o n that r e p r e s e n t s a p r o p o s i t i o n or a compound p r o p o s i t i o n i s c a l l e d a well-formed formula. D e f i n i t i o n . Well-formed formulas ( w f f ) , or formulas f o r s h o r t , are d e f i n e d r e c u r s i v e l y as f o l l o w s : 1. An atom i s a formula (atomic formula). 2. I f G and H are formulas, then (-G), ( G V H ) , (GAH), (G->H), and (G<->H) are formulas. 3. A l l formulas are generated by a p p l y i n g the above r u l e s . If A1,A2,...,An are atoms o c c u r r i n g i n a formula G, then an i n t e r p r e t a t i o n of G i s an assignment of t r u t h v a l u e s to A1,..,An in which every A i i s a s s i g n e d e i t h e r T ( t r u t h ) or F ( f a l s e h o o d ) , but not both. Once the i n t e r p r e t a t i o n i s determined, the t r u t h value of G can be e v a l u a t e d . If i t i s e v a l u a t e d to T, then G i s s a i d to be true under (or in) the i n t e r p r e t a t i o n , otherwise G i s s a i d to be f a l s e under the i n t e r p r e t a t i o n . In mathematics as w e l l as i n d a i l y l i f e , we o f t e n have to decide whether a statement f o l l o w s from some other statements. T h i s leads to the concept of " l o g i c a l consequence" which i s d e f i n e d as f o l l o w s : D e f i n i t i o n . Given formulas F1,F2,..,Fn and a formula G, G i s s a i d to be a l o g i c a l consequence of F1,...,Fn (or G 7 l o g i c a l l y f o l l o w s from F1,..,Fn) i f and only i f f o r any i n t e r p r e t a t i o n I i n which F l A F 2 A A F n i s t r u e , G i s a l s o t r u e . F1,F2,...,Fn are c a l l e d axioms (or premises) of G. D e f i n i t i o n . If G i s a l o g i c a l consequence of F1,..,Fn, the formula ((F1 A...A Fn)->G) i s c a l l e d a theorem , and G i s a l s o c a l l e d the c o n c l u s i o n of the theorem. (G i s sometimes r e f e r r e d to as a query i n the context automatic d e d u c t i o n ) . A demostration that a theorem i s true i s c a l l e d a proof of the theorem. L o g i c i a n s seem to be p a r t i c u l a r l y i n t e r e s t e d i n formulas which are true under a l l i n t e r p r e t a t i o n s and those which are f a l s e under a l l i n t e r p r e t a t i o n s . These two kinds of formulas are r e s p e c t i v e l y c a l l e d v a l i d formulas and u n s a t i s f i a b l e (or  i n c o n s i s t e n t ) formulas. We note that a formula i s v a l i d i f and only i f i t s negation i s u n s a t i s f i a b l e . In the r e s o l u t i o n methods that w i l l be d i s c u s s e d i n l a t e r c h a p t e r s , i t i s necessary to transform a wff to i t s e q u i v a l e n t c o n j u n c t i v e normal form which i s d e f i n e d as f o l l o w s . D e f i n i t i o n . A l i t e r a l i s an atom or the negation of an atom. D e f i n i t i o n . A c l a u s e i s a d i s j u n c t i o n of l i t e r a l s . A c l a u s e i s an u n i t c l a u s e i f and only i f i t c o n s i s t s of 8 only one l i t e r a l . D e f i n i t i o n . A formula i s s a i d to be i n c o n j u n c t i v e  normal form i f and only i f i t has the form L l A . . . A L n , n>1, where each L1,..,Ln i s a c l a u s e . We have e s t a b l i s h e d the background for p r o p o s i t i o n a l l o g i c and now we can extend i t to f i r s t - o r d e r l o g i c . 2.2 F i r s t - o r d e r Logic F i r s t - o r d e r l o g i c i s an ex t e n s i o n of p r o p o s i t i o n a l l o g i c in the sense that the framework of p r o p o s i t i o n a l l o g i c i s s t i l l r e t a i n e d , but the n o t i o n s of p r o p o s i t i o n i s extended to i n c l u d e p r e d i c a t e s and q u a n t i f i e r s . A p r e d i c a t e , i s a statement about s p e c i f i c o b j e c t s (or i n d i v i d u a l s ) or r e l a t i o n between these o b j e c t s . More p r e c i s e l y , i t i s a mapping that maps a l i s t of constants to T or F. For example, LESS i s a p r e d i c a t e . LESS(3 ,5) i s T but•LESS(5,3) i s F. Arguments of p r e d i c a t e s are c a l l e d terms , which i s d e f i n e d r e c u r s i v e l y as f o l l o w s : 1. A constant i s a term. 2. A v a r i a b l e i s a term. 3. I f f i s an n-place f u n c t i o n symbol, and t 1 , . . , t n are terms, then f ( t 1 , . . , t n ) i s a term. 4. A l l terms are generated by a p p l y i n g the above r u l e s . 9 We c a l l a term c o n t a i n i n g no v a r i a b l e s a ground term. Throughout t h i s a r t i c l e , we s h a l l only use x, y, and z to represent v a r i a b l e s . Having d e f i n e d terms, we can now d e f i n e an atom in f i r s t - o r d e r l o g i c as P ( t 1 , . . t n ) , where P i s p r e d i c a t e symbol and t 1 , . . , t n are terms. We can b u i l d up more complex formula using the f i v e l o g i c a l c o n n e c t i v e s given in S e c t i o n 2.1. Furthermore, v a r i a b l e s i n a p r e d i c a t e are c h a r a c t e r i z e d by two q u a n t i f i e r s , namely the u n i v e r s a l q u a n t i f i e r and the e x i s t e n t i a l q u a n t i f i e r . If x i s a v a r i a b l e , then (x) i s read as " f o r a l l x" and (Ex) i s read as "there e x i s t s an x". I t should be noted that f i r s t - o r d e r l o g i c permits only q u a n t i f i c a t i o n over i n d i v i d u a l s but not p r e d i c a t e s and f u n c t i o n s . The scope of a q u a n t i f i e r o c c u r r i n g i n a formula i s d e f i n e d as the formula to which the q u a n t i f i e r a p p l i e s . For example, the scope of the u n i v e r s a l q u a n t i f i e r and e x i s t e n t i a l q u a n t i f i e r i n the formula (x) (R(x)->(Ey)Q(x,y)) are (R(x)->(Ey)Q(x,y)) and (Q(x,y)) r e s p e c t i v e l y . A formula W i s s a i d to be c l o s e d i f and only i f every occurrence of a v a r i a b l e x i n W i s i n the scope of (x) or (Ex). Such an x i s bound by the corresponding q u a n t i f i e r . A v a r i a b l e i s f r e e i f and only i f i t i s not bound by any q u a n t i f i e r s . We s h a l l now d e f i n e an i n t e r p r e t a t i o n of a formula i n f i r s t - o r d e r l o g i c . D e f i n i t i o n . An i n t e r p r e t a t i o n of a formula W c o n s i s t s of 10 a nonempty domain D and the f o l l o w i n g assignments: 1. Assignment of an element in D to each constant in W. 2. Assignment of a mapping, from D" to D, to each n-place f u n c t i o n symbol in W. 3. Assignment of a mapping, from D"\ to {T,F}, to each n-place p r e d i c a t e symbol i n W. Having d e f i n e d i n t e r p r e t a t i o n f o r f i r s t - o r d e r l o g i c , we can extend the r e s t of the d e f i n i t i o n s i n S e c t i o n 2.1 i n a s i m i l a r way. We s h a l l c l o s e t h i s s e c t i o n by g i v i n g an example to i l l u s t r a t e how deduction can be a p p l i e d i n the context of f i r s t - o r d e r l o g i c . Suppose we have the f o l l o w i n g two formulas in our database, (x) ROBIN(x) -> BIRD(x) (x) BIRD(x) -> HASWINGS(x), then from these two formulas, we can conclude, by means of l o g i c a l d eduction, that the f o l l o w i n g formula must a l s o be t r u e : (x) ROBIN(x) -> HASWINGS(x) 2.3 Logic As A R e p r e s e n t a t i o n Scheme The most important f e a t u r e of l o g i c - b a s e d r e p r e s e n t a t i o n s i s that there i s a set of i n f e r n e c e r u l e s by which f a c t s that are known to be t r u e can be used to d e r i v e other f a c t s that must a l s o be t r u e . As a r e s u l t , deductions based on these r u l e s are guaranteed c o r r e c t to an extent that other r e p r e s e n t a t i o n schemes have not yet been able to do. 11 From the example presented at the end of the previous s e c t i o n , i t i s not hard to r e a l i z e that there i s a s p e c i f i c r u l e of i n f e r e n c e that allows us to t r e a t deductions as s y n t a c t i c m a n i p u l a t i o n s of l o g i c a l formulas. T h i s makes the d e r i v a t i o n of new formulas from o l d e a s i l y mechanizable. Using l o g i c as a r e p r e s e n t a t i o n scheme f a c i l i t a t e s the s e p a r a t i o n of r e p r e s e n t a t i o n and p r o c e s s i n g , s i n c e l o g i c makes no commitment to the kinds of processes that w i l l a c t u a l l y make deduc t i o n s . In other words, l o g i c - b a s e d r e p r e s e n t a t i o n a l system allows knowledge"to be represented independently of i t s use. Another important p r o p e r t y of l o g i c i s i t s mo d u l a r i t y . L o g i c a l a s s e r t i o n s can be added to a database without a f f e c t i n g each other, whereas i n some other r e p r e s e n t a t i o n a l systems, a d d i t i o n of a new f a c t might a f f e c t the kinds of deductions that can be made. A f t e r a l l , l o g i c i s a p r e c i s e and n a t u r a l way to express c e r t a i n n o t i o n s . 2.4 D e s c r i p t i v e Adequacy Of F i r s t - o r d e r Logic A l o g i c - b a s e d r e p r e s e n t a t i o n formalism allows us to express many kinds of g e n e r a l i z a t i o n . With a knowledge base c o n t a i n i n g such g e n e r a l i z a t i o n s and with the use of deduction, the system can manipulate e x p r e s s i o n s i n the r e p r e s e n t a t i o n formalism and permit l o g i c a l l y complex q u e r i e s to be made, even when i t cannot e v a l u a t e a query d i r e c t l y . In order to capture these kinds of g e n e r a l i z a t i o n s , a r e p r e s e n t a t i o n a l system must, at l e a s t , be powerful enough to do 1 2 the f o l l o w i n g [ B a r r and Feigenbaum,1982]: 1. Say that some i n d i v i d u a l possesses a c e r t a i n p r o p e r t y without s p e c i f y i n g which i n d i v i d u a l i t i s : (Ex) P(x); 2. Say that a l l the i n d i v i d u a l s of a c e r t a i n c l a s s share a c e r t a i n p r o p e r t y without s p e c i f y i n g what those i n d i v i d u a l s of that c l a s s a r e : (x) P(x)->Q(x); 3. Say that at l e a s t one of the two statements i s true without s p e c i f y i n g the t r u t h v a l u e s of the statements: PVQ; 4. Say e x p l i c i t l y that a statement i s f a l s e , i n s t e a d of simply not saying that i t i s t r u e : -"P. Any r e p r e s e n t a t i o n formalism t h a t can capture these notions w i l l be at l e a s t an ext e n s i o n of c l a s s i c a l f i r s t - o r d e r l o g i c . In other words, c l a s s i c a l f i r s t - o r d e r l o g i c i s the minimal language that possesses the necessary e x p r e s s i v e power. 2.5 D e c i s i o n Problem For F i r s t - o r d e r L o g i c In p r o p o s i t i o n a l l o g i c , the v a l i d i t y of a formula can be e a s i l y determined by the t r u t h t a b l e method i n which the t r u t h v a l u e s of the formula are e v a l u a t e d f o r a l l p o s s i b l e i n t e r p r e t a t i o n s . U n f o r t u n a t e l y , i n f i r s t - o r d e r l o g i c , one cannnot always compute whether or not a wff i s v a l i d when q u a n t i f i e r s occur. I t was proved by Church[l936] and Turing[1936] that there i s no general d e c i s i o n procedure to check the v a l i d i t y of formulas of f i r s t - o r d e r l o g i c ; f o r t h i s reason, f i r s t ^ o r d e r l o g i c i s s a i d to 1 3 be undecidable. However, there are proof procedures (e.g. r e s o l u t i o n ) which can v e r i f y that a formula i s v a l i d i f indeed i t i s v a l i d . On the other hand, when these procedures are a p p l i e d to i n v a l i d formulas, they may never termi n a t e . Thus, f i r s t - o r d e r l o g i c i s s a i d to be semidecidable. 1 4 Chapter 3. The R e s o l u t i o n P r i n c i p l e The r e s o l u t i o n p r i n c i p l e i s a r u l e of i n f e r e n c e that can be used to d e r i v e the l o g i c a l consequences of two formulas which are r e l a t e d i n an a p p r o p r i a t e way. Since i t s a p p l i c a t i o n i n v o l v e s only s y n t a c t i c m anipulation of formulas, i t p r o v i d e s us with a u s e f u l t o o l to prove theorems i n a p u r e l y mechanical way. We s h a l l f i r s t c o n s i d e r the r e s o l u t i o n p r i n c i p l e f o r p r o p o s i t i o n a l l o g i c , then we s h a l l extend i t to f i r s t - o r d e r l o g i c . 3.1 The R e s o l u t i o n P r i n c i p l e For P r o p o s i t i o n a l Logic Suppose P, Q, and R are p r o p o s i t i o n s . A c e n t r a l r u l e of in f e r e n c e i n l o g i c , modus ponens, says that i f (P->Q) and P are true then we can conclude that Q i s t r u e . An extension of t h i s i s the cha i n r u l e , which says that i f (P->Q) and (Q->R) are tr u e , then we can conclude that (P->R) i s t r u e . E x p r e s s i n g (P->Q), (Q->R) and (P->R) i n c l a u s e form, we have (-"PVQ) and (-'QVR) gi v e r i s e to ("'PVR). In terms of r e s o l u t i o n , (-'PVR) i s the r e s o l v e n t of ("'PVQ) and (-'QVR), and i t i s formed by the d i s j u n c t i o n of i t s parent c l a u s e s , namely (""PVQ) and (""Qv/R), followed by the c a n c e l l a t i o n of the complementary p a i r Q and ""Q. In g e n e r a l , the r e s o l u t i o n p r i n c i p l e i s s t a t e d as f o l l o w s : "For any two c l a u s e s C1 and C2, i f there i s a l i t e r a l LI i n C1 that i s complementary to a l i t e r a l L2 i n C2, then d e l e t e L1 and L2 from C1 and C2 r e s p e c t i v e l y , and c o n s t r u c t the d i s j u n c t i o n of 15 the remaining c l a u s e s . The c o n s t r u c t e d c l a u s e i s a r e s o l v e n t of C1 and C2." An important property of a r e s o l v e n t i s that any r e s o l v e n t of two c l a u s e s C1 and C2 i s a l o g i c a l consequence of C1 and C2. 3.2 The R e s o l u t i o n P r i n c i p l e For F i r s t - o r d e r L o g i c In the previous s e c t i o n , we observe that two important processes have to be performed when a p p l y i n g the r e s o l u t i o n p r i n c i p l e to d e r i v e c o n c l u s i o n s . The f i r s t process i s the c o n v e r s i o n of f i r s t - o r d e r l o g i c wffs to t h e i r l o g i c a l l y e q u i v a l e n t forms c l a u s e s . (Although not a l l r e s o l u t i o n procedures r e q u i r e the c o n v e r s i o n to be done, many of them work only with wffs i n c l a u s e form). The next important process i s to f i n d a l i t e r a l in a c l a u s e which i s complementary to a l i t e r a l i n another c l a u s e . Both of these processes, e s p e c i a l l y the l a t t e r , one, are very simple i n the context of p r o p o s i t i o n a l l o g i c . However, due to the e x i s t e n c e of q u a n t i f i e r s , these processes become more complicated i n f i r s t - o r d e r l o g i c and they w i l l be d i s c u s s e d i n d e t a i l i n the next two s e c t i o n s . 3.2.1 Conversion Of Wffs To Clauses A c l a u s e i s d i s j u n c t i o n of l i t e r a l s . The c l a u s e form of wff was i n t r o d u c e d by Davis and Putnam[1960]. I t can shown that each wff i n f i r s t - o r d e r l o g i c has a unique c l a u s e form and thus, i t i s o f t e n r e f e r r e d to as the standard form cf formulas. More im p o r t a n t l y , i t can be proved t h a t i f a wff l o g i c a l l y f o l l o w s from a set of wffs S, then i t a l s o l o g i c a l l y f o l l o w s from the 16 set of c l a u s e s obtained by c o n v e r t i n g the wffs i n S to c l a u s e form. B a s i c a l l y , the co n v e r s i o n process can be broken down i n t o the f o l l o w i n g sequence of steps [ N i l s s o n , 1 9 8 0 ] : 1. E l i m i n a t e i m p l i c a t i o n symbols A l l occurrences of the -> and <-> symbols i n a wff are e l i m i n a t e d by making the s u b s t i t u t i o n of - ,X1VX2 f o r X1->X2 and (X1 A X2 ) V ( ~"X1 A -*X2 ) for X1<->X2. 2. Reduce scopes of negation symbols We make each negation symbol, ->, to apply to at most one atomic formula. T h i s goal can be achieved by making use of the f o l l o w i n g e q u i v a l e n c e s r e p e a t e d l y : -"(-•X) i s e q u i v a l e n t to X MX1VX2) i s e q u i v a l e n t to -X1A-X2 (XI A X2 ) i s e q u i v a l e n t to -X1V-X2 -•(Ex)P(x) i s e q u i v a l e n t to (x)-'P(x) -'(x)P(x) i s e q u i v a l e n t to (Ex)-"P(x) 3. Standardize v a r i a b l e s S t a n d a r d i z i n g v a r i a b l e s i s to rename v a r i a b l e s u n i f o r m l y such that each q u a n t i f i e r has i t s own unique v a r i a b l e . For example, we w r i t e (x)P(x)->(y)Q(y) i n s t e a d of (x)P(x)->(x)Q(x). 4. E l i m i n a t e e x i s t e n t i a l q u a n t i f i e r s 1 7 To e l i m i n a t e an e x i s t e n t i a l q u a n t i f i e r with no u n i v e r s a l q u a n t i f i e r s i n f r o n t of i t , we simply r e p l a c e the v a r i a b l e by a constant, f o r example, (Ex)P(x) i s re p l a c e d by P ( a ) . That i s , we i n s t a n t i a t e the c l a i m that an x e x i s t s by choosing a p a r t i c u l a r constant a to take i t s p l a c e . However, when we have a formula such as ( y ) ( E x ) P ( x , y ) , then we cannot r e p l a c e x by an a r b i t r a r y constant because the x that e x i s t s might depend on the value of y. We l e t t h i s dependence be e x p l i c i t l y d e f i n e d by some f u n c t i o n of y which maps each value of y i n t o x that " e x i s t s " . Such a f u n c t i o n i s c a l l e d a Skolem  funct i o n . Thus, we r e p l a c e ( x ) ( y ) ( E z ) P ( x , y , z ) by ( x ) ( y ) P ( x , y , f ( x , y ) ) , where f i s a Skolem f u n c t i o n . 5. Convert to prenex normal form A wff i s i n prenex normal form i f and only i f the wff c o n s i s t s of a s t r i n g of q u a n t i f i e r s c a l l e d a p r e f i x f o l l o w e d by a q u a n t i f i e r - f r e e formula c a l l e d a matrix. Since we have a l r e a d y removed a l l the e x i s t e n t i a l q u a n t i f i e r s by s k o l e m i z a t i o n , so we only have to move a l l the u n i v e r s a l q u a n t i f i e r s to the f r o n t of the wff. 6. E l i m i n a t e u n i v e r s a l q u a n t i f i e r s Since a l l the v a r i a b l e s i n the wffs must be bound, we are assured that a l l the v a r i a b l e s remaining at t h i s stage are u n i v e r s a l l y q u a n t i f i e d . Thus, we may e l i m i n a t e the e x p l i c i t occurrence of u n i v e r s a l q u a n t i f i e r s and assume that a l l v a r i a b l e s i n the matrix are u n i v e r s a l l y 18 q u a n t i f i e d . 7. Put matrix i n c o n j u n c t i v e normal form T h i s can be done by rep e a t e d l y a p p l y i n g one of the d i s t r i b u t i v e laws, namely, by r e p l a c i n g e x p r e s s i o n s of the form X 1 V ( X 2 A X 3 ) by (X1 VX2 ) A (X1 V x3 ) . 8. E l i m i n a t e A, symbols By r e p e a t e d l y r e p l a c i n g e x p r e s s i o n s of the form (X1A X2) with the set of wffs {X1,X2}, we w i l l o b t a i n a f i n i t e set of wffs, each of which i s a c l a u s e . 9. Rename v a r i a b l e s The l a s t step, which i s a l s o c a l l e d s t a n d a r d i z i n g v a r i a b l e s a p a r t , i s to rename v a r i a b l e symbols so that no v a r i a b l e symbol appears i n more than one c l a u s e . By f o l l o w i n g steps 1-7, we can s u c c e s s f u l l y convert a wff to i t s c o n j u n c t i v e normal form. By the commutative law of c o n j u n c t i o n ( s t e p 8), we can c o n s i d e r a wff i n c o n j u n c t i v e normal form as a set of c l a u s e s . S i m i l a r l y , by the commutative law of d i s j u n c t i o n , we can view a c l a u s e as a set of l i t e r a l s . 3.2.2 S u b s t i t u t i o n And U n i f i c a t i o n In proving theorems i n v o l v i n g q u a n t i f i e d formulas, i t i s o f t e n necessary to make ex p r e s s i o n s i d e n t i c a l by s u b s t i t u t i n g terms f o r v a r i a b l e s . The process of f i n d i n g such s u b s t i t u t i o n 19 i s extremely important in Al and i s c a l l e d u n i f i c a t i o n . (We note that u n i f i c a t i o n i s more general than pattern-matching because pattern-matching processes t y p i c a l l y do not allow v a r i a b l e s to occur i n both e x p r e s s i o n s ) . A s u b s t i t u t i o n i s a f i n i t e set of ordered p a i r s {t1/v1,..,tn/vn}, where every v i i s a v a r i a b l e , every t i i s a term d i f f e r e n t from v i , and no two elements i n the set have the same v a r i a b l e a f t e r the s t r o k e symbol. (The s u b s t i t u t i o n that c o n s i s t s of no elements i s c a l l e d the empty s u b s t i t u t i o n ). If E i s an e x p r e s s i o n and s={t1/v1,..,tm/vm} i s a s u b s t i t u t i o n , then Es i s a s u b s t i t u t i o n i n s t a n c e of E which i s obtained by r e p l a c i n g s i m u l taneously each occurrence of the v a r i a b l e v i i n E by the term t i . For example, l e t E=P(x,y,z) and s={a/x, f ( b ) / y , c/z}, then E s = P ( a , f ( b ) , c ) . The composition of two s u b s t i t u t i o n s s1 and s2 i s denoted by s1s2, which i s that s u b s t i t u t i o n obtained by a p p l y i n g s2 to the terms of s1 and then adding any p a i r s of s2 having v a r i a b l e s not o c c u r r i n g among the v a r i a b l e s of s1. Thus, {g(x,y)/z} {a/x,b/y,c/w,d/z} = {g(a,b)/z,a/x,b/y,c/w}. A set {E1,..,Ek} of e x p r e s s i o n s i s u n i f i a b l e i f there e x i s t s a s u b s t i t u t i o n s, c a l l e d a u n i f i e r , such that E1s=E2s=...Eks. Furthermore, a u n i f i e r u f o r a set {E1,..,Ek} of e x p r e s s i o n s i s a most g e n e r a l u n i f i e r i f and only i f f o r each u n i f i e r s1 f o r the s e t , there i s a s u b s t i t u t i o n s2 such that s1=us2. For example, c o n s i d e r the set { P ( x ) , P ( f ( y ) ) } , the most gen e r a l u n i f i e r u={f(y)/x} and i f si={f(a)/x,a/y} then s2={a/y}. 20 There i s an a l g o r i t h m , the u n i f i c a t i o n algorithm[Robinson,1965], which f i n d s the most general u n i f i e r of a set of u n i f i a b l e e x p r e s s i o n s or r e p o r t s f a i l u r e when the ex p r e s s i o n s are not u n i f i a b l e . In a d d i t i o n to the r e c u r s i v e "matching" process, the a l g o r i t h m a l s o i n c l u d e s a check, an occur check , to ensure that no v a r i a b l e can be s u b s t i t u t e d by a term c o n t a i n i n g that same v a r i a b l e . The reason why occur check i s necessary can be i l l u s t r a t e d by the f o l l o w i n g example. Consider two e x p r e s s i o n s , P(x) and P ( f ( x ) ) , i n order to u n i f y them, we have to s u b s t i t u t e x by f ( x ) , which i s f ( f ( x ) ) , which i s f ( f ( f ( x ) ) ) , and so on. As a r e s u l t , x has to be s u b s t i t u t e d by some kind of i n f i n i t e s t r u c t u r e . According to the formal d e f i n i t i o n of u n i f i c a t i o n , t h i s kind of " i n f i n i t e term" should never come to e x i s t and t h i s can be guaranteed by performing an occur check. 3.2.3 F a c t o r i n g Having introduced the notio n s of u n i f i c a t i o n , we can now co n s i d e r another important process c a l l e d f a c t o r i n g . The o b j e c t i v e of f a c t o r i n g i s to remove redundant l i t e r a l s i n a c l a u s e . Thus, i f we c o n s i d e r a c l a u s e as a set of l i t e r a l s , then f a c t o r i n g i s simply an a p p l i c a t i o n of u n i f i c a t i o n to a c l a u s e , s i n c e there i s no redundant elements i n a s e t . D e f i n i t i o n . If two or more l i t e r a l s (with the same sign) of a c l a u s e C have a most general u n i f i e r g, then Cg i s c a l l e d a f a c t o r of C. Furthermore, Cg i s an u n i t f a c t o r of C i f Cg i s an u n i t c l a u s e . 21 For i n s t a n c e , l e t C=P( x) V P( f (y) ) V _,Q( x) . The f i r s t two l i t e r a l s have a most general u n i f i e r g={f(y)/x}. Hence, Cg=P( f (y) ) V " 1Q(f (y) ) i s a f a c t o r of C. Sometimes a c l a u s e may have more than one f a c t o r . For example, i f C=P(x)V P ( f ( x ) ) V P ( f ( a ) ) , then both P ( f ( a ) ) V P ( f ( f ( a ) ) and P ( a ) V P ( f ( a ) ) are f a c t o r s of C. 3.2.4 D e f i n i t i o n Of Resolvent For F i r s t - o r d e r L o g i c Having in t r o d u c e d the concepts of u n i f i c a t i o n and f a c t o r i n g , we can now extend the r e s o l u t i o n p r i n c i p l e f o r p r o p o s i t i o n a l l o g i c to f i r s t - o r d e r l o g i c . D e f i n i t i o n . Let C1 and C2 be two c l a u s e ( c a l l e d parent c l a u s e s ) with no v a r i a b l e s i n common. Let L1 and L2 be two l i t e r a l s i n C1 and C2, r e s p e c t i v e l y . If LI and ->L2 have a most g e n e r a l u n i f i e r g, then the c l a u s e , or set of l i t e r a l s (Clg - L 1 g ) U ( C 2 g - L2g) i s c a l l e d a b i n a r y r e s o l v e n t of C1 and C2. The l i t e r a l s L1 and L2 are c a l l e d l i t e r a l s r e s o l v e d upon. D e f i n i t i o n . A r e s o l v e n t of (parent) c l a u s e s C1 and C2 i s one of the f o l l o w i n g b i n a r y r e s o l v e n t s : 1. a b i n a r y r e s o l v e n t of C1 and C2, 2. a b i n a r y r e s o l v e n t of C1 and a f a c t o r of C2, 2. a b i n a r y r e s o l v e n t of a f a c t o r of C1 and C2, 4. a b i n a r y r e s o l v e n t of a f a c t o r of C1 and a f a c t o r of C2. 22 For example, R ( g ( g ( a ) ) V Q(b) i s r e s o l v e n t of P ( x ) V P ( f ( y ) ) V R ( g ( y ) ) and - P ( f ( g ( a ) ) ) V Q(b). We note that the r e s o l v e n t d e f i n e d above s t i l l p r e s e r v e s the important p r o p e r t y of being a l o g i c a l consequence of i t s parent c l a u s e s . The r e s o l u t i o n p r i n c i p l e i s f o r generating r e s o l v e n t s from a set of c l a u s e s . Since a r e s o l v e n t of two c l a u s e s i s a l s o a l o g i c a l consequence of them, the r e s o l u t i o n p r i n c i p l e can be used as an i n f e r e n c e r u l e f o r p r o v i n g theorems. Although the r e s o l u t i o n p r i n c i p l e i s e f f i c i e n t and easy to apply, u n l i m i t e d a p p l i c a t i o n s of r e s o l u t i o n may cause many i r r e l e v a n t c l a u s e s to be generated. In the next chapter, we s h a l l examine some s t r a t e g i e s which r e s t r i c t the a p p l i c a t i o n of r e s o l u t i o n so as to improve i t s e f f i c i e n c y . 23 Chapter 4. R e s o l u t i o n R e f u t a t i o n s If a formula G does l o g i c a l l y f o l l o w from a set of axioms A, then the set formed by the union of {-'G} and A must be u n s a t i s f i a b l e . That i s , they must l e a d to a c o n t r a d i c t i o n . T h i s c o n t r a d i c t i o n i s represented by an empty c l a u s e i n r e s o l u t i o n . A r e s o l u t i o n r e f u t a t i o n , or proof by c o n t r a d i c t i o n , i s a deduction of an empty c l a u s e ( c o n t r a d i c t i o n ) using the r e s o l u t i o n p r i n c i p l e as a r u l e of i n f e r e n c e . 4.1 Ba s i s Of R e f u t a t i o n s Before i n t r o d u c i n g the r e s o l u t i o n a l g o r i t h m , we s h a l l b r i e f l y c o n s i d e r some theorems which form the foundation of the a l g o r i t h m . The f o l l o w i n g theorems assume that F1,..,Fn, and G are formulas. Theorem. (Deduction Theorem) G i s a l o g i c a l consequence of F1,..,Fn i f and only i f the formula ((F1 A..A Fn)->G) i s v a l i d . From the deduction theorem, we can d e r i v e the f o l l o w i n g theorem. Theorem. G i s a l o g i c a l consequence of F1,..,Fn i f and only i f ( ( F 1 A . . A F n A nG) i s i n c o n s i s t e n t . 24 Theorem. (Completeness of R e s o l u t i o n P r i n c i p l e ) A set S of c l a u s e s i s u n s a t i s f i a b l e i f and only i f there i s a deduction of the empty c l a u s e from S. Thus, i f we l e t S be the set of c l a u s e s obtained by a p p l y i n g the procedures, d e s c r i b e d i n s e c t i o n 3.2.1, to the formula (F1 A . . A F n A n G ) , then we can conclude that G i s a l o g i c a l consequence of F1,..,Fn i f and only i f we can produce a deduction of the empty c l a u s e from S by a p p l y i n g the r e s o l u t i o n p r i n c i p l e . T h i s forms the b a s i s of the r e s o l u t i o n r e f u t a t i o n a l g o r i t h m presented in the f o l l o w i n g s e c t i o n . 4.2 The B a s i c A l g o r i t h m For R e s o l u t i o n R e f u t a t i o n A r e s o l u t i o n r e f u t a t i o n procedure i s a procedure which produces r e f u t a t i o n s by a p p l y i n g the r e s o l u t i o n p r i n c i p l e to an u n s a t i s f i a b l e set of c l a u s e s . I t i n v o l v e s generating new c l a u s e s , c a l l e d r e s o l v e n t s , from the set of c l a u s e s which i s obtained by c o n v e r t i n g the axioms and the negated c o n c l u s i o n of the theorem to c l a u s e form. These r e s o l v e n t s are then added to the set of c l a u s e s from which they have been d e r i v e d , and new r e s o l v e n t s are d e r i v e d . T h i s process i s repeated u n t i l an empty cl a u s e i s found. The f o l l o w i n g i s a general r e s o l u t i o n r e f u t a t i o n a l g o r i t h m [ N i l s s o n , 1 9 8 0 ] which w i l l generate the empty c l a u s e i f the set S (the base set) of c l a u s e s i s u n s a t i s f i a b l e . 25 1. CLAUSES <- S 2. While the empty c l a u s e i s not in CLAUSES 3. begin 4. S e l e c t a c l a u s e C i , from CLAUSES 5. S e l e c t a c l a u s e C j , from CLAUSES such that there i s a l i t e r a l i n Cj which i s a complement to one in C i 6. Compute a r e s o l v e n t R i j of Ci and Cj 7. CLAUSES <- CLAUSES U {Rij} 8. end. A l g o r i t h m 4.1 I t can be proved t h a t the a l g o r i t h m i s sound ( i . e . i t w i l l not i n d i c a t e that nontheorems are t r u e ) . Moreover, i t i s complete i n the sense that i t i s guaranteed to d e r i v e the empty c l a u s e from an u n s a t i s f i a b l e set of c l a u s e s . However, due to the inherent semidecidable p r o p e r t y of f i r s t - o r d e r l o g i c , the r e s o l u t i o n procedure may not terminate when i t i s a p p l i e d to some s a t i s f i a b l e set of c l a u s e s . For example, co n s i d e r S={P(a) ,-"P(x) V P( f (x))} , the r e s o l u t i o n procedure w i l l generate r e s o l v e n t s P ( f ( a ) ) , P ( f ( f ( a ) ) ) , P ( f ( f ( f ( a ) ) ) ) , and so on. In t h i s case, the procedure does not terminate and i t i s easy to v e r i f y t h a t S i s s a t i s f i a b l e . In the f o l l o w i n g s e c t i o n , we s h a l l examine some r e s o l u t i o n s t r a t e g i e s and we s h a l l f r e q u e n t l y r e f e r to a l g o r i t h m 4.1. 26 4.3 R e s o l u t i o n S t r a t e g i e s The r e s o l u t i o n r e f u t a t i o n a l g o r i t h m presented i n the l a s t s e c t i o n i s a very general one because the s e l e c t i o n c r i t e r i a are not s t a t e d i n steps 4 and 5. If we perform those s e l e c t i o n s on a random b a s i s , then the process of s e a r c h i n g f o r a r e f u t a t i o n can be extremely time-consuming. In f a c t , the search space generated i n t h i s manner grows e x p o n e n t i a l l y with the number of c l a u s e s i n S, the base s e t . Ever s i n c e the i n t r o d u c t i o n of the r e s o l u t i o n p r i n c i p l e by Robinson[1965], many r e s o l u t i o n s t r a t e g i e s (both complete and incomplete) have been proposed to reduce the search space by d e f i n i n g some s e l e c t i o n c r i t e r i a f o r the c l a u s e s . A r e s o l u t i o n s t r a t e g y i s s a i d to be complete i f i t s use r e s u l t s i n a procedure that can always d e r i v e the empty c l a u s e from an u n s a t i s f i a b l e set of c l a u s e s . In other words, a s t r a t e g y i s complete i f i t s a p p l i c a t i o n p r e s e r v e s the completeness of the b a s i c r e s o l u t i o n a l g o r i t h m . (The completeness of a s t r a t e g y should not be confused with the l o g i c a l completeness of the r e s o l u t i o n p r i n c i p l e ) . When we c o n s i d e r a r e s o l u t i o n s t r a t e g y we would l i k e i t to be complete. N e v e r t h e l e s s , e f f i c i e n c y i s a l s o important i n mechanical theorem-proving. U n f o r t u n a t e l y , sometimes we can achieve only one goal at the expense of l o s i n g , or s e v e r e l y degrading, the other. However, i f a refinement of r e s o l u t i o n i s e f f i c i e n t and powerful enough to prove a l a r g e c l a s s of theorems, even though i t i s not complete, i t may s t i l l be u s e f u l . We s h a l l look at two such s t r a t e g i e s i n S e c t i o n 4 . 3 . 4 . 27 In the f o l l o w i n g s e c t i o n s , we s h a l l examine a few r e s o l u t i o n s t r a t e g i e s and some of them can be combined with o t h e r s to f u r t h e r improve the performance. Examples of r e s o l u t i o n r e f u t a t i o n s , f o r i l l u s t r a t i n g the use of each s t r a t e g y , w i l l be represented as a d e r i v a t i o n graph (or r e f u t a t i o n t r e e ) . The nodes in such a graph are l a b e l l e d by c l a u s e s ; i n i t i a l l y , there i s a node for every c l a u s e i n the base set S. When two c l a u s e s produce a r e s o l v e n t , we c r e a t e a new node and l a b e l i t by that r e s o l v e n t . T h i s new node have edges l i n k i n g i t to the p a i r of nodes whose l a b e l s are the parent c l a u s e s of the r e s o l v e n t . (A r e f u t a t i o n t r e e , which i s part of a d e r i v a t i o n graph, has a root node l a b e l l e d by NIL, the empty c l a u s e ) . Before we proceed to d i s c u s s v a r i o u s r e s o l u t i o n s t r a t e g i e s , we give the f o l l o w i n g d e f i n i t i o n which w i l l be used i n the d i s c u s s i o n . D e f i n i t i o n . A f i r s t - l e v e l r e s o l v e n t i s one between two c l a u s e s i n the base s e t . In g e n e r a l , an i - t h l e v e l  r e s o l v e n t i s one whose deepest parent i s an ( i - l ) - t h l e v e l r e s o l v e n t . I f the empty c l a u s e i s one of the i - t h l e v e l r e s o l v e n t s , then i i s the l e n g t h of the proof, or the height of the r e f u t a t i o n t r e e . 4.3.1 B r e a d t h - f i r s t S t r a t e g y The b r e a d t h - f i r s t s t r a t e g y i s complete and i t i s guaranteed to f i n d the s h o r t e s t proof i f S i s u n s a t i s f i a b l e , but 28 u n f o r t u n a t e l y , i t i s g r o s s l y i n e f f i c i e n t . In t h i s s t r a t e g y , a l l the f i r s t - l e v e l r e s o l v e n t s are generated f i r s t , and i f the empty c l a u s e i s not among them, then a l l the s e c o n d - l e v e l r e s o v l e n t s w i l l be generated, and so on. Thus, t h i s method i s a l s o known as the l e v e l - s a t u r a t i o n method. F i g u r e 1 shows the r e f u t a t i o n gragh produced by a b r e a d t h - f i r s t s t r a t e g y when S={-'L(x,T) V H(x) , -L(x ,V) V H ( x ) , L (J , T) V L (J , V) , -•H(J)}, and ~"H(J) i s the negation of the query. We note that the empty c l a u s e NIL, i s among the t h i r d - l e v e l r e s o l v e n t s . 4.3.2 Set - o f - s u p p o r t S t r a t e g y The s e t - o f - s u p p o r t s t r a t e g y was proposed by Wos, Robinson, and Carson[1965]. In the b r e a d t h - f i r s t s t r a t e g y as w e l l as the s t r a t e g i e s that w i l l be 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 , we t y p i c a l l y do not d i s t i n g u i s h the negated query from the axioms when we s e l e c t a p a i r of c l a u s e s from S ( i n Steps 4 and 5 of a l g o r i t h m 4.1). But the set of axioms i s u s u a l l y s a t i s f i a b l e , so the s e t - o f - s u p p o r t s t r a t e g y suggests at l e a s t one parent of each r e s o l v e n t be chosen from the set of support which c o n s i s t s of the negated query and the c l a u s e s that are d e r v i e d from i t . I t can proved that the s e t - o f - s u p p o r t s t r a t e g y i s complete. Moreover, i t i s u s u a l l y more e f f i c i e n t than the unconstrained b r e a d t h - f i r s t s t r a t e g y s i n c e i t reduces the number of r e s o l v e n t s being generated at each l e v e l , and consequently, the number of c l a u s e s that can be r e s o l v e d . T h i s can be e a s i l y v e r i f i e d by comparing f i g u r e 1 with f i g u r e 2. However, l i k e most r e s t r i c t i v e s t r a t e g i e s , the s e t - o f - s u p p o r t s t r a t e g y o f t e n i n c r e a s e s t h e depth a t wh i c h the empty c l a u s e i s f i r s t produced, -H(J) -L(x,T) V H(x) - L ( x , V ) V H ( x ) L ( J , T) V L ( J , V) - L ( J , T ) H ( J 1 H ( J ) H ( J ) H ( J ) L ( J , T ) L ( J , V ) L ( J , T ) L ( J , V ) NIL F i g u r e 1 - I l l u s t r a t i o n of B r e a d t h - f i r s t S t r a t e g y -H(J) -L(x,T) V H(x) - L ( x , V ) V H ( x ) L ( J , T ) V L ( J ,V) H ( J ) NIL H ( J ) NIL F i g u r e 2 - I l l u s t r a t i o n of S e t - o f - s u p p o r t S t r a t e g y 30 4.3.3 L i n e a r R e s o l u t i o n L i n e a r r e s o l u t i o n was independently proposed by Loveland[1970] and Luckham[1970]. A l i n e a r r e s o l u t i o n i n v o l v e s s e l e c t i n g a c l a u s e , c a l l e d top c l a u s e , r e s o l v e s i t a g a i n s t another c l a u s e i n S to o b t a i n a r e s o l v e n t , and r e s o l v e s t h i s r e s o l v e n t a g a i n s t some other c l a u s e s i n S u n t i l the empty c l a u s e i s o b t a i n e d . In terms of a l g o r i t h m 4.1, once we have s e l e c t e d a top c l a u s e , then f o r subsequent s e l e c t i o n s i n step 4, we always choose the "newest" r e s o l v e n t as one of the parent c l a u s e s f o r f u r t h e r d e r i v a t i o n u n t i l an empty c l a u s e i s o b t a i n e d . We s h a l l c a l l the top c l a u s e and a l l the r e s o l v e n t s c e n t e r c l a u s e s , and the r e s t of the c l a u s e s i n v o l v e d in the proof are c a l l e d s i d e  c l a u s e s . In a d d i t i o n to the completeness of l i n e a r r e s o l u t i o n , l i n e a r deduction a l s o has a very simple s t r u c t u r e . F i g u r e 3 shows a l i n e a r r e f u t a t i o n f o r our example problem i n s e c t i o n 4.3.1. In f a c t , the r e f u t a t i o n t r e e f o r l i n e a r r e s o l u t i o n i s so simple that i t can be f u r t h e r reduced to a path as shown in f i g u r e 4. 31 -L(x,T) V H ( x ) - L ( x , V ) V H(x) L(J,T) V L ( J , V ) L ( J , V ) V H(J) L(J,V) H(J) -•L(x,T)V H(x) -H(J) -•L(x,V) V H(x) "•H (J) NIL NIL F i g u r e 3. R e f u t a t i o n t r e e produced by a l i n e a r r e s o l u t i o n F i g u r e 4. S i m p l i f i e d form of a l i n e a r deduction Notice that we c o u l d a l s o i n c o r p o r a t e the s e t - o f - s u p p o r t s t r a t e g y i n t o l i n e a r r e s o l u t i o n by simply choosing the negated query, -"H(J), as the top c l a u s e ( F i g u r e 5). Once we have made our c h o i c e of top c l a u s e , l i n e a r r e s o l u t i o n a l l o w s us to remove step 4 from the a l g o r i t h m , which f u r t h e r r e s t r i c t s the number of p o s s i b l e r e s o l u t i o n s at any given time. Moreover, i n c o r p o r a t i o n of the s e t - o f - s u p p o r t s t r a t e g y does not destroy the completeness of l i n e a r r e s o l u t i o n , however, i t s t i l l cannot produce the s h o r t e s t proof as i n the b r e a d t h - f i r s t s t r a t e g y . 32 -H(J) - L ( x , T ) V H ( X ) ->L( J,T) L(J,T) V L ( J , V ) L(J,V) -'L(x,V)V H(x) H( j ) -H(J) NIL F i g u r e 5 - I n c o r p o r a t i o n of the s e t - o f - s u p p o r t i n t o a l i n e a r r e s o l u t i o n 4.3.4 L i n e a r Input R e s o l u t i o n And U n i t R e s o l u t i o n A l l the s t r a t e g i e s d i s c u s s e d i n the pr e v i o u s s e c t i o n s are complete, now we s h a l l c o n s i d e r two incomplete but e f f i c i e n t refinements of r e s o l u t i o n : l i n e a r input r e s o l u t i o n and u n i t r e s o l u t i o n . L i n e a r input r e s o l u t i o n i s a subcase of l i n e a r r e s o l u t i o n in the sense that i t i s the same as l i n e a r r e s o l u t i o n except that i t does not allow p r e v i o u s l y d e r i v e d r e s o l v e n t s to be used as s i d e c l a u s e s i n a r e f u t a t i o n . In terms of the a l g o r i t h m 4.1, t h i s simply means the removal of step 7, i n a d d i t i o n to the m o d i f i c a t i o n made i n the pre v i o u s s e c t i o n . As a r e s u l t , the s i z e of CLAUSES remains cons t a n t , and thus the number of p o s s i b l e r e s o l u t i o n s i s g r e a t l y reduced. On the other hand, i t can be shown that l i n e a r input r e s o l u t i o n i s incomplete due to 33 the f a c t t h a t s i d e c l a u s e s a r e r e s t r i c t e d t o members of the base s e t . F i g u r e 3 shows a l i n e a r i n p u t r e f u t a t i o n of our example problem. U n i t r e s o l u t i o n i s e s s e n t i a l l y an e x t e n s i o n of the o n e - l i t e r a l r u l e of D a v i s and Putnam[1960], and i t was e x t e n s i v e l y used by Wos, Ca r s o n , and R o b i n s o n [ 1 9 6 4 ] . A u n i t r e s o l u t i o n i s a r e s o l u t i o n i n which a r e s o l v e n t i s o b t a i n e d by u s i n g a t l e a s t one u n i t p a r e n t c l a u s e , or a u n i t f a c t o r of a p a r e n t c l a u s e . The r a t i o n a l e b e h i n d i t i s t h a t , i n o r d e r t o d e r i v e an empty c l a u s e from a u n s a t i s f i a b l e s e t of c l a u s e s , one must o b t a i n s u c c e s s i v e l y s h o r t e r c l a u s e s , and u n i t r e s o l u t i o n p r o v i d e s a means f o r p r o g r e s s i n g toward s h o r t e r c l a u s e s r a p i d l y . I t i s perhaps i m p o r t a n t t o note t h a t u n i t r e s o l u t i o n i s e q u i v a l e n t t o l i n e a r i n p u t r e s o l u t i o n s i n c e theorems t h a t can be proved by one can a l s o be proved by the o t h e r . F i g u r e 6 shows a r e f u t a t i o n produced by means of u n i t r e s o l u t i o n w i t h the s e t of c l a u s e s S = { P ( x ) V - Q ( x , y ) V R ( f ( x ) , y ) , - P ( a ) , Q ( a , b ) , - R ( f ( a ) , b ) } . P(x) V ->Q(x,y) V R ( f (x) ,y) -P(a) - Q ( a , y ) V R ( f ( a ) , y ) - R ( f ( a ) , b ) -Q(a,b) Q(a,b) NIL F i g u r e 6 - I l l u s t r a t i o n of a u n i t r e s o l u t i o n 34 4.3.5 Ordered L i n e a r Deduction In the l a s t s e c t i o n , we observe that l i n e a r input r e s o l u t i o n a l l o w s us to d e l e t e step 7 from a l g o r i t h m 4.1 to improve e f f i c i e n c y . U n f o r t u n a t e l y , the removal of step 7 d e s t r o y s the completeness of l i n e a r r e s o l u t i o n . However, l i n e a r r e s o l u t i o n can be m o d i f i e d i n a way that allows us to a t t a i n almost the same e f f i c i e n c y (by d e l e t i n g step 7) while s t i l l r e t a i n i n g i t s property of completeness. T h i s method makes use of the concept of ordered c l a u s e and.the i n f o r m a t i o n of r e s o l v e d l i t e r a l s . An ordered c l a u s e i s a sequence of d i s t i n c t l i t e r a l s . As a c l a u s e , an ordered c l a u s e i s a l s o i n t e r p r e t a t e d as a d i s j u n c t i o n of a l l the l i t e r a l s i n the ordered c l a u s e . The only d i f f e r e n c e i s that the order of l i t e r a l s i n a c l a u s e i s immaterial, while the order of l i t e r a l s i n an ordered c l a u s e i s d e l i b e r a t e l y s p e c i f i e d . With the concept of ordered c l a u s e i n mind, we can now r e s o l v e the l i t e r a l s i n a given c l a u s e one by one (say from l e f t to r i g h t ) . Since we only c o n s i d e r one l i t e r a l at a time> the number of c l a u s e s that can be r e s o l v e d with the given c l a u s e i s o b v i o u s l y reduced. Although the i n t r o d u c t i o n of ordered c l a u s e d e s t r o y s the completeness of some r e s o l u t i o n methods, i t does not a f f e c t l i n e a r r e s o l u t i o n . In r e s o l u t i o n , when a r e s o l v e n t i s obtained, l i t e r a l s r e s o l v e d upon are d e l e t e d . But, Loveland[1968, 1969a, b, 1972] and Kowalski and Kuehner[1971] d i s c o v e r e d that these l i t e r a l s can p r o v i d e i n f o r m a t i o n to improve l i n e a r r e s o l u t i o n . In f a c t , by r e c o r d i n g t h i s i n f o r m a t i o n a p p r o p r i a t e l y , we c o u l d d e f i n e a 35 necessary and s u f f i c i e n t c o n d i t i o n under which a s i d e c l a u s e must be a c e n t e r c l a u s e generated p r e v i o u s l y . The a l g o r i t h m that employs both the concept of ordered c l a u s e and the i n f o r m a t i o n of r e s o l v e d l i t e r a l s i s c a l l e d OL-deduction (ordered l i n e a r d e d u c t i o n ) . Before p r e s e n t i n g the p r e c i s e a l g o r i t h m of OL-deduction[Chang and Lee,1973], we f i r s t d i s c u s s the mechanism of r e c o r d i n g the i n f o r m a t i o n of r e s o l v e d l i t e r a l s . Suppose P V Q and -'QVR are ordered c l a u s e s . R e s o l v i n g them produces an ordered r e s o l v e n t PVR. Since the l i t e r a l s r e s o l v e d upon, namely Q and ""Q, are complementary to each other, we need only r e c o r d one of them, say Q. Now we can s t o r e the i n f o r m a t i o n by r e p r e s e n t i n g the ordered r e s o l v e n t as RVPVfQ] . The framed l i t e r a l , [Qj i n .this case, does not p a r t i c i p a t e i n r e s o l u t i o n , i t i s merely for r e c o r d i n g that Q has been r e s o l v e d upon. We s h a l l d e l e t e a framed l i t e r a l i f i t i s not preceded by an unframed l i t e r a l . Moreover, no t a u t o l o g y i s allowed i n ordered l i n e a r d e duction. Returning to the example where S={ _ ,H(J), - |L(x,T) V H ( x ) , -•L(x,V) V H(x) , L( J,T) V L( J,V)} . An ordered l i n e a r deduction i s shown i n f i g u r e 7. 36 ""H (J) - L ( x , T ) V H(x) -L(J,T)VhH(j) L(J,T) V L ( J , V ) L(J,V) v h L ( J . T W h H t J ) ' -L(x,V) V H(x) H( J) y(L( J,V)lv'hL( J.T)|vhH( J)j r e d u c t i o n NIL F i g u r e 7 - I l l u s t r a t i o n of a OL-deduction No t i c e t h a t i f we remove the framed l i t e r a l s from the f i r s t and second r e s o l v e n t s i n f i g u r e 7, then they are e x a c t l y the same as those i n f i g u r e 5. However, the l a s t ordered r e s o l v e n t H (J) V [ L (uVVJf V h L (J , T )1 V hH (J )j i s a s p e c i a l one because the f i r s t l i t e r a l of t h i s c l a u s e i s complementary to one of i t s framed l i t e r a l s . T h i s kind of c l a u s e i s c a l l e d r e d u c i b l e ordered  c l a u s e . Whenever a r e d u c i b l e ordered c l a u s e i s generated, we can be sure t h a t the f i r s t l i t e r a l can be r e s o l v e d by using a c e n t e r c l a u s e as the s i d e c l a u s e (examine f i g u r e 5 to confirm t h i s ) . T h i s means t h a t , i n s t e a d of s e a r c h i n g f o r that center c l a u s e to o b t a i n the next r e s o l v e n t , we c o u l d simply d e l e t e the f i r s t l i t e r a l from the ordered c l a u s e to o b t a i n i t . As a consequence, we do not have to s t o r e any r e s o l v e n t s being - generated, which o b v i o u s l y c u t s down the number of p o s s i b l e r e s o l u t i o n s ; w hile at the same time, the completeness of l i n e a r r e s o l u t i o n i s s t i l l p r e served. In terms of the a l g o r i t h m 4.1, 37 we can d e l e t e step 7, as i n the l i n e a r input s t r a t e g y . We s h a l l d i s c u s s the d e t a i l s of performing step 6 a f t e r i n t r o d u c i n g the f o l l o w i n g d e f i n i t i o n . D e f i n i t i o n . If two or more unframed l i t e r a l s (with the same sign) of an ordered c l a u s e C have a most general u n i f i e r g, an ordered f a c t o r of C can be obtained from the sequence Cg by removing a l l i d e n t i c a l unframed l i t e r a l s except the rightmost one, and by d e l e t i n g every framed l i t e r a l not f o l l o w e d by an unframed l i t e r a l i n the remaining c l a u s e . Suppose a l i t e r a l L1 i n a c e n t e r c l a u s e C1 i s complementary to a l i t e r a l L2 i n a s i d e c l a u s e C2, then the ordered r e s o l v e n t i s computed as f o l l o w s : - o b t a i n the c l a u s e R1, by appending C1 to C2, - frame the l i t e r a l L1 i n R1 and d e l e t e L2 from R1 to o b t a i n R2, - o b t a i n the ordered f a c t o r of R2 i f there i s one, i f the r e s u l t i n g c l a u s e i s r e d u c i b l e , reduce i t by removing the l e f t m o s t l i t e r a l and d e l e t e any framed l i t e r a l s f o l l o w i n g i t . 4.4 D e l e t i o n S t r a t e g i e s From a l g o r i t h m 4.1, we can observe that the number of p o s s i b l e r e s o l u t i o n s grows e x p o n e n t i a l l y with the s i z e of the set CLAUSES. Thus, the s m a l l e r the set CLAUSES i s , the more 38 e f f i c i e n t the r e s o l u t i o n i s . D e l e t i o n s t r a t e g i e s are s t r a t e g i e s which e l i m i n a t e two kind of c l a u s e s , namely t a u t o l o g i e s and subsumed c l a u s e s . Although d e l e t i o n s t r a t e g i e s are complete only i f they are used with the b r e a d t h - f i r s t s t r a t e g y , i n c o r p o r a t i n g these s t r a t e g i e s i n t o other r e s o l u t i o n methods improves the performance of the methods s i g n i f i c a n t l y . F i g u r e 8 shows a search t r e e generated by a p p l y i n g a l g o r i t h m 4.1 to the set of c l a u s e s S={PvQ, ""PVQ, -•PV-'Q, P V Q ) . 4.4.1 D e l e t i o n Of T a u t o l o g i e s A c l a u s e i s a t a u t o l o g y i f there i s a complementary p a i r of l i t e r a l s i n the c l a u s e . For example, P(x) V _ ,P(x) v Q(y) i s a P V Q NIL F i g u r e 8 - Search t r e e generated by r e s o l u t i o n t a u t o l o g y . Since t a u t o l o g i e s are t r u e under a l l 39 i n t e r p r e t a t i o n s , removing them from a set w i l l not a f f e c t the u n s a t i s f i a b i l i t y of the r e s t of the s e t . By examining f i g u r e 8, one can observe that the rightmost subtree of the top c l a u s e PVQ w i l l not be generated i f t h i s d e l e t i o n s t r a t e g y i s a p p l i e d . 4.4.2 Subsumption Subsumption i s the process f o r d i s c a r d i n g a c l a u s e that d u p l i c a t e s or i s l e s s g e n e r a l than another c l a u s e . By d e f i n i t i o n , a c l a u s e C subsumes another c l a u s e D i f and only i f there i s a s u b s t i t u t i o n s such that Cs i s a subset of D, and D i s c a l l e d a subsumed c l a u s e . For i n s t a n c e , c o n s i d e r two c l a u s e s P(x) and P ( a ) , P(a) i s subsumed by P(x) and thus i t w i l l be d e l e t e d by subsumption. Again, r e f e r to f i g u r e 8, we can observe that the subtree, whose root i s l a b e l l e d by Q at the t h i r d l e v e l , w i l l not be generated i f subsumption i s a p p l i e d . The process of d i s c a r d i n g r e s o l v e n t s which are subsumed by c l a u s e s i n the set CLAUSES i s c a l l e d forward subsumption, whereas the process of d i s c a r d i n g c l a u s e s i n the set CLAUSES which are subsumed by newly generated r e s o l v e n t i s c a l l e d backward subsumption. The next chapter d e s c r i b e s the implementation of the theorem-prover LRTP, and we s h a l l see how these s t r a t e g i e s are a p p l i e d i n the LRTP. 40 Chapter 5. The L i n e a r R e s o l u t i o n Theorem Prover The L i n e a r R e s o l u t i o n Theorem Prover (LRTP), w r i t t e n i n P r o l o g , was intended to be an experimental t o o l f o r studying the performance of three r e s o l u t i o n s t r a t e g i e s , namely, l i n e a r r e s o l u t i o n , l i n e a r input r e s o l u t i o n , and ordered l i n e a r d e d uction. In a d d i t i o n , i t a l s o allows the user t o p e r f o r m experiments on these s t r a t e g i e s i n combination with other s t r a t e g i e s . In the LRTP, the performance of a s t r a t e g y (or a combination of s t r a t e g i e s ) i s measured i n terms of the number of u n i f i c a t i o n s r e q u i r e d i n the search of a r e f u t a t i o n i n a given s e t t i n g . The performance can be e v a l u a t e d f o r three v a l u e s , which represent the number of u n i f i c a t i o n s i n v o l v e d i n r e s o l u t i o n ; and i n the two d e l e t i o n s t r a t e g i e s . In a d d i t i o n to these s t a t i s t i c s , the proof ( i f there i s one) i s a l s o p r i n t e d . On the other hand, i f no proof can be found i n the given s e t t i n g , the LRTP w i l l r e p o r t f a i l u r e . 41 5.1 O r g a n i z a t i o n Of The LRTP The LRTP i s composed of a database and f i v e modules which i n c l u d e the command i n t e r p r e t e r , the t r a n s l a t o r , the r e f u t a t i o n module, the d e l e t i o n module, the u n i f i c a t i o n module. F i g u r e 9 - I n t e r n a l o r g a n i z a t i o n of the LRTP The i n t e r a c t i o n between these modules and the database i s shown in F i g u r e 9. The arrows i n d i c a t e the d i r e c t i o n s of access, i n v o k a t i o n or dataflow. 5.1.1 The Database There are two major components i n the database. The f i r s t one c o n s i s t s of the i n f o r m a t i o n of the parameters r e q u i r e d f o r s e t t i n g up the environment i n which r e s o l u t i o n s are performed. The i n f o r m a t i o n i s obtained from the user through i n t e r a c t i o n s with the command i n t e r p r e t e r . D e t a i l s of how the parameters a f f e c t the r e s o l u t i o n s performed i n the LRTP w i l l be d i s c u s s e d i n s e c t i o n 5.1.4. 42 The second component c o n s i s t s of the " s e t " of c l a u s e s S which may or may not be u n s a t i s f i a b l e . (Notice that the LRTP makes no d i s t i n c t i o n between the negated query and the axioms). Each of the c l a u s e s i n S i s t r e a t e d as an ordered c l a u s e , and furthermore, the " s e t " S i t s e l f i s t r e a t e d as an ordered  database. In other words, the LRTP t r e a t s the set of ordered c l a u s e s as a l i s t of ordered c l a u s e s . The o r d e r i n g of the ordered c l a u s e s in the database matches the order in which they are entered by the user through the t r a n s l a t o r . I t i s important to note that the i n c o r p o r a t i o n of the concept of ordered database w i l l not a f f e c t the completeness of r e s o l u t i o n i f the search f o r r e f u t a t i o n i s ai d e d by a b a c k t r a c k i n g mechanism (which i s provided by the PROLOG/MTS i n t e r p r e t e r ) . A f t e r a l l , t r e a t i n g S as an ordered database renders d e t e r m i n i s t i c the s e l e c t i o n i n v o l v e d in step 5 of the a l g o r i t h m 4.1. 5.1.2 The Command I n t e r p r e t e r The command i n t e r p r e t e r i s an i n t e r f a c e with the user. I t s ba s i c f u n c t i o n i s to accept commands from the user and executes them, mostly by in v o k i n g other modules. Among these modules, the most important one i s the r e f u t a t i o n module which performs r e s o l u t i o n s . By e n t e r i n g the a p p r o p r i a t e commands to the command i n t e r p r e t e r , the user can a l s o access or modify the in f o r m a t i o n s t o r e d i n the database. 5.1.3 The T r a n s l a t o r When the user i s s u e s the command to enter c l a u s e s i n t o the 43 database, the command i n t e r p r e t e r w i l l t r a n s f e r c o n t r o l to the t r a n s l a t o r [ C l o c k s i n and Mellish,1981] i n which a wff w i l l be accepted and converted to i t s c l a u s e form u s i n g the a l g o r i t h m d e s c r i b e d i n s e c t i o n 3.2.1. When the c o n v e r s i o n i s done, the d e l e t i o n s t r a t e g i e s module w i l l be invoked to f i l t e r any t a u t o l o g i e s or subsumed c l a u s e s . The remaining c l a u s e s are t r e a t e d as ordered c l a u s e s and are added to the ordered database. The whole process i s repeated u n t i l the user has no more c l a u s e s to e n t e r . F i n a l l y , c o n t r o l i s t r a n s f e r r e d back to the command i n t e r p r e t e r . 5.1.4 The R e f u t a t i o n Module T h i s module i s the most important p a r t of the LRTP. B a s i c a l l y , i t i s a r e f u t a t i o n system which operates i n an environment t a i l o r e d by the users to meet t h e i r own needs.-Besides sea r c h i n g f o r the proof, t h i s module a l s o records the number of u n i f i c a t i o n s i n v o l v e d i n f a c t o r i n g and r e s o l v i n g c l a u s e s . We s h a l l now d i s c u s s the parameters i n v o l v e d i n the r e s o l u t i o n environment. 5.1.4.1 S e l e c t i o n Of R e s o l u t i o n S t r a t e g i e s There are three s t r a t e g i e s i n c o r p o r a t e d i n the r e f u t a t i o n system. These three s t r a t e g i e s are l i n e a r r e s o l u t i o n , l i n e a r input r e s o l u t i o n , and ordered l i n e a r d e d u c t i o n . Although they are b u i l t w i t h i n the same framework, each of them works independently; i t i s up to the user to s e l e c t which one to apply. 44 5.1.4.2 Switches For D e l e t i o n S t r a t e g i e s In a d d i t i o n to the s e l e c t i o n of r e s o l u t i o n s t r a t e g i e s , the user has the o p t i o n s of combining two d e l e t i o n s t r a t e g i e s , d e l e t i o n of t a u t o l o g i e s and forward subsumption, with any one of the three r e s o l u t i o n s t r a t e g i e s t h a t the user has s e l e c t e d . These o p t i o n s are p r o v i d e d to the user as two switches: one f o r forward subsumption and the other f o r d e l e t i o n of t a u t o l o g i e s . These switches are independent of each other and they can be turned on or o f f at the d i s c r e t i o n of the user. When the switch f o r a d e l e t i o n s t r a t e g y i s turned on, then that p a r t i c u l a r s t r a t e g y w i l l be a p p l i e d d u r i n g the search f o r a r e f u t a t i o n . However, the user should be aware of the incompleteness of d e l e t i o n s t r a t e g i e s as mentioned i n s e c t i o n 4.4. 5.1.4.3 Choice Of Top Clause One important f e a t u r e of the LRTP i s that i t allows the user to choose the top c l a u s e f o r the l i n e a r d e d u c t i o n . As d i s c u s s e d i n s e c t i o n 4.3.3, we can combine the s e t - o f - s u p p o r t s t r a t e g y with l i n e a r deduction by simply choosing the top c l a u s e from the set of support. Thus, even though the LRTP i t s e l f does not d i s t i n g u i s h between the negated query and the axioms, the user can s t i l l employ the s e t - o f - s u p p o r t s t r a t e g y by s e l e c t i n g an a p p r o p r i a t e top c l a u s e . 5.1.4.4 Choice Of Depth Bound Due to the semidecidable p r o p e r t y of f i r s t - o r d e r l o g i c , the LRTP may not terminate when i t i s given an i n v a l i d formula. 45 Furthermore, s i n c e the LRTP adopts the d e p t h - f i r s t s t r a t e g y (as i s the PROLOG/MTS i n t e r p r e t e r ) , i t may not terminate even i f the given formula i s v a l i d . As an example of t h i s , the l e f t m o s t branch of the t r e e shown in f i g u r e 8 can be i n f i n i t e , and as a r e s u l t , an unbound d e p t h - f i r s t search may not terminate. Thus, in order to a v o i d the non-termination problem, we must provide a depth bound f o r the t r e e s e a r c h i n g . In the LRTP, the choice of the depth bound i s l e f t to the user to allow maximum f l e x i b i l i t y . Furthermore, the depth bound i s used to reduce the search space by ensuring that the number of unframed l i t e r a l s i n a center c l a u s e C of a l i n e a r deduction i s always l e s s than the d i f f e r e n c e between the depth bound and the l e v e l of C. 5.1.4.5 Switch For Shortest L i n e a r R e f u t a t i o n By examining the search t r e e i n f i g u r e 8, one can e a s i l y d i s c o v e r that there are four branches ( i n f a c t there are more) l e a d i n g to the empty c l a u s e . Suppose we c a l l the path l e a d i n g to NIL., , proof 1, and the path l e a d i n g to NIL 2, proof 2, and so on. Then proof 1 and proof 2 are of l e n g t h 4, whereas proof 3 and proof 4 are of length 5 and 6 r e s p e c t i v e l y . Thus, i f the user e n t e r s 6 f o r the depth bound of the search, then the LRTP w i l l r e t u r n proof 4. If the depth bound i s 4 then i t w i l l r e t u r n e i t h e r proof 1 or proof 2, depending on the o r d e r i n g of the c l a u s e s i n the•database. Thus, by decrementing the depth bound, one can f i n d the s h o r t e s t l i n e a r r e f u t a t i o n . However, t h i s r e q u i r e s the LRTP to r e p e a t e d l y search over the same branches that have been generated b e f o r e . (Notice that t h i s s h o r t e s t l i n e a r r e f u t a t i o n i s not n e c e s s a r i l y the s h o r t e s t 4 6 r e f u t a t i o n which can o n l y be o b t a i n e d by the b r e a d t h - f i r s t s t r a t e g y ) . For the u s e r ' s c o n v e n i e n c e , the LRTP has a l r e a d y automated t h i s p r o c e s s and i t i s p r o v i d e d t o the user as an o p t i o n ( s w i t c h ) . However, i t i s automated i n a way t h a t i s more e f f i c i e n t than the one suggested i n the p r e v i o u s p a r a g r a p h . When the s w i t c h f o r s h o r t e s t l i n e a r r e f u t a t i o n i s t u r n e d on, the LRTP w i l l f i r s t t r y t o f i n d a p r o o f w i t h i n the g i v e n depth bound. I f one e x i s t s , i t i s r e c o r d e d and t h e n , the LRTP w i l l c o n t i n u e w i t h the s e a r c h , r i g h t a t the p o i n t where the p r e v i o u s p r o o f i s found, and s i m u l t a n e o u s l y s e t t i n g t he depth bound t o one l e s s than the l e n g t h of the most r e c e n t p r o o f o b t a i n e d . When t h e r e i s more than one s h o r t e s t l i n e a r r e f u t a t i o n , the LRTP w i l l s i m p l y r e t u r n the f i r s t one t h a t i t f i n d s . In our example, i f the c l a u s e number of P V Q i s s m a l l e r than t h a t of •'PVQ, then p r o o f 1 w i l l be r e t u r n e d ; o t h e r w i s e p r o o f 2 w i l l be r e t u r n e d i n s t e a d . 5.1.5 The D e l e t i o n Module The d e l e t i o n module can be in v o k e d by the t r a n s l a t o r and the r e f u t a t i o n module. When the user i s e n t e r i n g c l a u s e s , t h i s module w i l l be i n v o k e d by the t r a n s l a t o r t o e l i m i n a t e any t a u t o l o g i e s and subsumed c l a u s e s . The o r d e r of p e r f o r m i n g the r e q u i r e d o p e r a t i o n s i s : f i r s t , d e l e t i o n of t a u t o l o g i e s , s e c o n d l y , f o r w a r d subsumption, and f i n a l l y , backward subsumption. We note t h a t the a p p l i c a t i o n of backward subsumption i m p l i e s t h a t a c l a u s e which has a l r e a d y been added 47 to the database may s t i l l be d e l e t e d i f i t i s subsumed by a new c l a u s e entered by the user. During the search f o r a proof, the d e l e t i o n module may be invoked by the r e f u t a t i o n module, depending on the s t a t u s of the switches as d i s c u s s e d i n s e c t i o n 5.1.4.2. If one or both switches are on, then the d e l e t i o n module w i l l be invoked, and the number of u n i f i c a t i o n s i n v o l v e d w i l l be recorded as a measure of performance. Regardless of whether the switches are on or not, backward subsumption i s not performed during r e s o l u t i o n . 5.1.6 The U n i f i c a t i o n Module Since u n i f i c a t i o n done i n the PROLOG/MTS i n t e r p r e t e r does not i n c l u d e the occurs check, the u n i f i c a t i o n i s r e b u i l t to i n c l u d e t h i s i n the LRTP. There are four o c c a s i o n s when u n i f i c a t i o n i s r e q u i r e d . The u n i f i c a t i o n module i s invoked by the r e f u t a t i o n module f o r f a c t o r i n g and r e s o l v i n g c l a u s e s d u r i n g r e s o l u t i o n . Moreover, u n i f i c a t i o n i s a l s o i n v o l v e d i n i d e n t i f y i n g t a u t o l o g i e s and subsumed c l a u s e s . T h i s i m p l i e s that the u n i f i c a t i o n module i s invoked by the d e l e t i o n module when one or both of the switches fo r the d e l e t i o n s t r a t e g i e s are on. 5.2 The LRTP Versus The P r o l o g I n t e r p r e t e r Although both the LRTP and the Pr o l o g system are r e s o l u t i o n theorem-provers, they d i f f e r i n many ways. A fundamental 48 d i f f e r e n c e is that the LRTP i s intended as an a i d to study the performance of r e s o l u t i o n s t r a t e g i e s , whereas the Prol o g i n t e r p r e t e r i s b u i l t to provide a p r a c t i c a l programming system. In terms of e v a l u a t i n g the performance of r e s o l u t i o n s t r a t e g i e s , the f o l l o w i n g f e a t u r e s are l a c k i n g i n the Prol o g system but are p r o v i d e d i n the LRTP. 5.2.1 Completeness The P r o l o g system i s based on l i n e a r input r e s o l u t i o n which i s an incomplete r e s o l u t i o n s t r a t e g y as d i s c u s s e d i n s e c t i o n 4.3.4. Furthermore, the Prol o g system i s designed f o r r e s o l u t i o n with Horn c l a u s e s o n l y . Horn clauses[Horn,1951] are a s u b c l a s s of wffs i n f i r s t - o r d e r l o g i c : i t i s the c l a s s of c l a u s e s with at most one unnegated literal. On the other hand, the LRTP o f f e r s a v a r i e t y of s t r a t e g i e s which can be e i t h e r complete or incomplete. Moreover, any wffs i n f i r s t - o r d e r l o g i c are l e g i t i m a t e e x p r e s s i o n s f o r the LRTP. Consequently, e x i s t e n t i a l q u a n t i f i c a t i o n i s allowed i n the LRTP (but not i n the Prol o g system). 5.2.2 U n i f i c a t i o n As a l r e a d y mentioned i n s e c t i o n 5.1.6, the u n i f i c a t i o n i n most P r o l o g implementations does not i n c l u d e the occurs check as the formal d e f i n i t i o n of u n i f i c a t i o n r e q u i r e s . While the LRTP i s b u i l t on top of the PROLOG/MTS system, the u n i f i c a t i o n i n the LRTP i s r e b u i l t to i n c l u d e the occurs check f o r the sake of completeness. 49 5.2.3 Termination B a s i c a l l y , P r o l o g adopts the unbound d e p t h - f i r s t s t r a t e g y . As a r e s u l t , the r e s o l u t i o n may not terminate. On the other hand, a depth bound i s i n c o r p o r a t e d i n t o the LRTP and consequently, t e r m i n a t i o n i s guaranteed. 5.2.4 D e l e t i o n S t r a t e g i e s The LRTP allows any one of the three r e s o l u t i o n s t r a t e g i e s being implemented to combine with any one or both of the two d e l e t i o n s t r a t e g i e s , namely, d e l e t i o n of t a u t o l o g i e s and subsumption. Furthermore, these two s t r a t e g i e s are a l s o a p p l i e d to f i l t e r any " i m p u r i t i e s " i n the wffs entered by the user. On the other hand, these s t r a t e g i e s are not implemented in the P r o l o g system. 5.2.5 Measure Of Performance As a t o o l f o r s t u d y i n g the performance of r e s o l u t i o n s , the LRTP r e p o r t s the number of u n i f i c a t i o n s i n v o l v e d i n searching f o r a r e f u t a t i o n as a measure of performance; whereas no q u a n t i t a t i v e measure of performance i s provided i n the P r o l o g system. 5.2.6 S h o r t e s t L i n e a r R e f u t a t i o n The LRTP p r o v i d e s the user an o p t i o n to o b t a i n the s h o r t e s t l i n e a r r e f u t a t i o n , which i s not p r o v i d e d i n the P r o l o g system. 50 Chapter 6. Conclusion The LRTP has been s u c c e s s f u l l y implemented. I t appears to be a u s e f u l experimental t o o l f o r studying the performance of the three l i n e a r r e s o l u t i o n s t r a t e g i e s : l i n e a r r e s o l u t i o n , l i n e a r input r e s o l u t i o n , and ordered l i n e a r d eduction, and t h e i r combinations with other s t r a t e g i e s , i . e . the s e t - o f - s u p p o r t s t r a t e g y , subsumption and d e l e t i o n of t a u t o l o g i e s . Furthermore, one can de v i s e a l a r g e v a r i e t y of experiments by manipulating the parameters of the r e s o l u t i o n environment. One major drawback of the LRTP i s that a l l wffs have to be converted to c l a u s e form before r e s o l u t i o n s can be performed. Although the c l a u s e form p r e s e r v e s the l o g i c a l p r o p e r t i e s of the o r i g i n a l wff, the c o n t r o l i n f o r m a t i o n f o r the search process i s l o s t a f t e r the c o n v e r s i o n . In p a r t i c u l a r , the i n f o r m a t i o n which guides the use of wffs i n a forward-chaining or or backward-chaining manner i s l o s t . For example, suppose we have a formula P->Q. If we use i t i n the forward-chaining manner, then the g o a l i s to generate Q, given P i s t r u e . I f i t i s used in a backward-chaining manner, as i n the P r o l o g i n t e r p r e t e r , then the g o a l i s to generate P, given Q i s t r u e . In any case, we proceed i n one d i r e c t i o n o n l y . However, i f we convert i t to c l a u s e form, which i s - ' P v Q , then the deduction process i s a b i d i r e c t i o n a l search p r o c e s s . As a r e s u l t , the searches i n v o l v e d are h i g h l y redundant. Thus, i n order to perform r e s o l u t i o n i n a more e f f i c i e n t 51 way, we have to i n c o r p o r a t e some s p e c i f i c c o n t r o l i n f o r m a t i o n i n the r e s o l u t i o n system to l e a d the search process i n the " r i g h t " d i r e c t i o n . However, i n c o r p o r a t i o n of s p e c i f i c c o n t r o l i n f o r m a t i o n may dest r o y the domain-independent property of the r e s o l u t i o n system. 52 BIBLIOGRAPHY Barr , A., and Feigenbaum, E.A.(1982): The Handbook of A r t i f i I n t e l l i g e n c e , V o l . 1 , W i l l i a m Kaufmann Inc., Los A l t o s , C a l i f o r n i a . Chang, C , and Lee, R.C.(1973): Symbolic Logic and Mechanica Theorem Pro v i n g , New York, Academic Press. Church, A.(1936): "An u n s o l v a b l e problem of number theory", Amer. J . Math. (58), pp.345-363. C l o c k s i n , W.F., and M e l l i s h , C.S.(1981): Programming i n P r o l S p r i n g e r - V e r l a g , New York. D a v i s , M. and Putnam, H.(1960): "A computing procedure f o r q u a n t i f i c a t i o n theory", J.ACM(7) No.3, pp.201-215. G e l e r n t e r , H .(l963): " R e a l i z a t i o n of a geometry theorem-prov machine", Proceedings of an I n t e r n a t i o n a l Conference on Information P r o c e s s i n g , P a r i s : UNESCO House, pp.273-282 Gilmore, P.C.(1960): "A proof method for q u a n t i f i c a t i o n theo i t s j u s t i f i c a t i o n and r e a l i z a t i o n " , IBM J . of Research Development (4) No.1, pp.28-35. Goebel, R . O 9 8 0 ) : PROLOG/MTS User's Manual, TM80-2, Dept. o Comp. Sc., Univ. of B r i t . C o l . Herbrand, J.(1930): " I n v e s t i g a t i o n s i n proof theory: the p r o p e r t i e s of the p r o p o s i t i o n s " , From Frege to Godel: a Source Book i n Mathematical Logic ( J . van H e i j e n o o r t , ed.), Havard Univ. Press, Cambridge, Massachusetts. Horn, A.(1951): "On sentence which are true of d i r e c t unions a l g e b r a s " , J . of Symbolic L o g i c (16) No.1, pp.14-21. Kowalski, R. , and Kuehner, D.(1971): "Linear R e s o l u t i o n with 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 , Vol.2, pp 227-260. Loveland, D.W.(1968): "Mechanical theorem proving by model e l i m i n a t i o n " , J . ACM(15), No.2, pp.236-251. Loveland, D.W.(1969a): "A s i m p l i f i e d format f o r the model e l i m i n a t i o n theorem-proving procedure", J . ACM(16) No. pp.349-363. 53 Loveland, D.W.(1969b): "Theorem provers combining model e l i m i n a t i o n and r e s o l u t i o n " , Machine I n t e l l i g e n c e , V o l . (B. M e l t z e r and D. M i c h i e , eds.), American E l s e v i e r , York, pp.73-86. Loveland, D.W.(1970): "A l i n e a r format f o r r e s o l u t i o n " , Proc IRIA Symp. Automatic Demostration, S p r i n g e r - V e r l a g , Ne York, pp.147-162. Loveland, D.W.(1972): "A u n i f y i n g view of some l i n e a r Herbra procedures", J . ACM(19), No.2, pp.366-384. Luckham, D.(1970): "Refinements i n r e s o l u t i o n theory", Proc. IRIA Symp. Automatic Demostration, V e r s a i l e s , France, 1968, S p r i n g e r - V e r l a g , New York, pp.163-190. McCarthy, J.(1977): " E p i s t e m o l o g i c a l Problems of A r t i f i c i a l I n t e l l i g e n c e " , IJCAI 5, pp.1038-1044. McCarthy, J . , and Hayes, P.J.(1969): "Some p h i l o s o p h i c a l problems from the standpoint of a r t i f i c i a l i n t e l l i g e n c e D. M i c h i e and B. M e l t z e r (eds.), Machine I n t e l l i g e n c e Edinburgh: Edinburgh Univ. Press, pp.463-582. Newell, A., and Simon, H.A.(1956): "The l o g i c theory machine IRE T r a n s a c t i o n s on Information t h e o r y ( 2 ) : pp.61-79. N i l s s o n , N.J.(1980): P r i n c i p l e s of A r t i f i c i a l I n t e l l i g e n c e , A l t o , C a l i f o r n i a , T i o g a . Robinson, J.A.(1965): "A machine o r i e n t e d l o g i c based on the r e s o l u t i o n p r i n c i p l e " , J . ACM(12), No.1, pp.23-41. T u r i n g , A.M.(1936): "On computable numbers, with an a p p l i c a t to the entscheindungs-problem", Proc. London Maths Soc 42, pp.230-265. Wos, L., Carson, D., and Robinson, G.A.(1964): "The u n i t p r e f e r e n c e s t r a t e g y i n theorem p r o v i n g " , Proc. AFIPS 1 F a l l J o i n t Comput. Conf.(26), pp.616-621. Wos, L., Robinson, G.A., and Carson, D.F.(1965): " E f f i c i e n c y completeness of the set of support s t r a t e g y i n theorem p r o v i n g " , J . ACM(12), No.4, pp.536-541. 54 Appendix A - LRTP User's Manual 1 Overview The L i n e a r R e s o l u t i o n Theorem Prover (LRTP) i s b u i l t on top of the PROLOG/MTS system. I t i s intended to be an experimental t o o l f o r studying the performance of three r e s o l u t i o n s t r a t e g i e s , namely, l i n e a r r e s o l u t i o n , ordered l i n e a r deduction, and l i n e a r input r e s o l u t i o n . The f i r s t two are complete s t r a t e g i e s whereas the l a s t one i s incomplete. In a d d i t i o n , the LRTP a l s o allows the user to perform experiments on the three s t r a t e g i e s i n combination with o t h e r s . Furthermore, the user has c o n t r o l over the environment i n which a theorem i s proved. If a proof i s found under the given s e t t i n g , i t w i l l be p r i n t e d together with the number of u n i f i c a t i o n s i n v o l v e d i n the search f o r the p r o o f . T h i s number i s broken i n t o three values which represent the numbers of u n i f i c a t i o n s i n v o l v e d in r e s o l u t i o n and i n the two d e l e t i o n s t r a t e g i e s . Based on these s t a t i s t i c s , one can e v a l u a t e the performance of a s t r a t e g y (or a combination of s t r a t e g i e s ) i n a designated s e t t i n g . On the other hand, the LRTP w i l l r e p o r t f a i l u r e i f no proof can be found. For a d e t a i l e d d e s c r i p t i o n of the i n t e r n a l o r g a n i z a t i o n of the LRTP, the reader can r e f e r to Chapter 5 of the t h e s i s . 55 2 Using The LRTP The LRTP i s an i n t e r a c t i v e theorem prover which can be invoked by the f o l l o w i n g command: $SOURCE NHFC:LRTP Once the LRTP i s invoked, the command i n t e r p r e t e r w i l l prompt the user to enter a command. (A command menu can be obtained by i s s u i n g the HELP command). A l l the responses to the command i n t e r p r e t e r w i l l be converted to uppercase and a l l inputs to the LRTP must end with a p e r i o d . The three commands by which the user e x i t s the LRTP a r e : PROLOG, MTS, and STOP. A d e t a i l e d d e s c r i p t i o n of the three commands can be found i n s e c t i o n 4.4 of the manual. The s i z e of the workspace taken up by the LRTP i s 256 MTS v i r t u a l pages (1 page = 4K b y t e s ) . T h i s workspace c o n t a i n s the database of wffs i n t h e i r c l a u s e form, the d e r i v a t i o n t r e e c o n s t r u c t e d during the search f o r a proof and the theorem prover i t s e l f . The two user i n t e r f a c e s of the LRTP are the t r a n s l a t o r and the command i n t e r p r e t e r , and they w i l l be d i s c u s s e d i n the f o l l o w i n g two s e c t i o n s . 3 The T r a n s l a t o r When the user e n t e r s the WFF (or the PROVE command when the system i s f i r s t l oaded), c o n t r o l w i l l be t r a n s f e r r e d to the t r a n s l a t o r . The t r a n s l a t o r i s r e s p o n s i b l e f o r c o n v e r t i n g wffs to t h e i r c l a u s e forms and i n s e r t i n g them i n t o the database i f 56 they are n e i t h e r t a u t o l o g i e s nor subsumed c l a u s e s . When a c l a u s e i s added to the database, i t w i l l be p r i n t e d along with i t s c l a u s e number. Since a c l a u s e number i n d i c a t e s the c u r r e n t p o s i t i o n of a cl a u s e i n the database, i t may be a f f e c t e d by backward subsumption. On the other hand, i f a c l a u s e i s a t a u t o l o g y or a subsumed c l a u s e , i t w i l l not be added to the database and a r e j e c t i o n message w i l l be p r i n t e d . 3.1 Clause Syntax In The LRTP Apart from the n o t a t i o n a l d i f f e r e n c e s , the concept of wffs in the LRTP i s the same as i n p r e d i c a t e c a l c u l u s . The f o l l o w i n g summarizes the n o t a t i o n a l d i f f e r e n c e s between the two. In t h i s summary, F, F l , and F2 represent any wffs and x any v a r i a b l e . P r e d i c a t e C a l c u l u s Syntax . LRTP Syntax -F -F F1 A F2 F1 $ F2 F 1 V F 2 F1 # F2 F1 -> F2 F1 => F2 F1 <-> F2 F1 = F2 (x) F a l l ( * x , F ) (Ex) F . e x i s t s ( * x , F ) For i n s t a n c e , (x)(animal(x)->(Ey)motherof(x,y)) i n p r e d i c a t e c a l c u l u s i s e q u i v a l e n t to a l l ( * x , a n i m a l ( * x ) = > e x i s t s ( * y , m o t h e r o f ( * x , * y ) ) ) i n the LRTP. Since the LRTP does not perform any syntax checking, the user should be very c a r e f u l when e n t e r i n g a wff (use ATTN f o r e r r o r r e c o v e r y ) . In a d d i t i o n to the above syntax r u l e s , each 57 v a r i a b l e i n the formula must be unique and bound. Furthermore, f u n c t i o n symbol fx and constant symbol cs (where x i s an i n t e g e r ) should be avoided s i n c e these two types of symbols are used i n s k o l e m i z a t i o n and subsumption check. F i n a l l y , when NIL ( f o l l o w e d by a pe r i o d ) i s entered, the t r a n s l a t o r w i l l e x i t and a l i s t of c l a u s e s i n the database w i l l be p r i n t e d . N o t i c e that there i s no lowercase to uppercase c o n v e r s i o n done i n the t r a n s l a t o r , thus the atom NIL should be entered e x a c t l y as i t i s . 4 The Command I n t e r p r e t e r The command i n t e r p r e t e r i s the major user i n t e r f a c e through which commands are i n t e r p r e t e d . A c c o r d i n g to the f u n c t i o n s of the commands, we can d i v i d e them i n t o three groups: database commands, environment commands, and e x i t commands. In a d d i t i o n to these three groups of commands, we a l s o have the PROVE command.by which a theorem can be proved. 4.1 The PROVE Command And A u t o - i n i t i a l i z a t i o n Of Parameters Of a l l the LRTP commands, the PROVE command i s the most important s i n c e i t i s the one which a c t u a l l y i n i t i a t e s the search f o r a proof . During the search, the LRTP f r e q u e n t l y i n t e r r o g a t e s the valu e s of the s i x parameters of the environment so as to assure that the r e f u t a t i o n i s performed i n the p r e s p e c i f i e d way. The s i x parameters i n c l u d e the r e s o l u t i o n method, the top c l a u s e , the depth bound, and switches f o r t a u t o l o g y check, subsumption check, and s h o r t e s t l i n e a r 58 r e f u t a t i o n . When the user i s s u e s the PROVE command, the LRTP w i l l check whether the s i x parameters have t h e i r own a s s i g n e d v a l u e s . If not, i t w i l l r e p e a t e d l y prompt the user to a s s i g n a value f o r each u n i n i t i a l i z e d parameter. Once every parameter has a value , the LRTP w i l l proceed to search f o r a proof i n the s p e c i f i e d environment. When the LRTP i s f i r s t invoked, i t i s more convenient to use the PROVE command to i n i t i a l i z e the parameters than to is s u e the s i x environment commands one by one (see S e c t i o n 4.3). Furthermore, i f there i s no c l a u s e i n the database, the PROVE command w i l l invoke the t r a n s l a t o r to accept wffs from the user (see S e c t i o n 3 ) . 4.2 Database Commands Database commands r e f e r to the commands which maintain the l i s t of c l a u s e s i n the database. There are four such commands: WFF T h i s command invokes the t r a n s l a t o r to convert wffs to cl a u s e forms and i n s e r t s them to the database. D e t a i l s of t h i s command can be found i n S e c t i o n 3. DELETE When t h i s command i s used, the system w i l l prompt the user to enter a c l a u s e number. Let t h i s number be n. The system w i l l then remove the n-th c l a u s e ( i f i t e x i s t s ) from the database. Since a c l a u s e number i n d i c a t e s the c u r r e n t p o s i t i o n of the c l a u s e i n the database, removal of the n-th c l a u s e w i l l cause a l l the 5 9 c l a u s e numbers which are g r e a t e r than n to be decreased by 1. To av o i d d e l e t i n g a c l a u s e by mistake, the user i s advi s e d to check the c l a u s e number by the LIST command (d e s c r i b e d below) before using the DELETE command. LIST T h i s command p r i n t s the l i s t of c l a u s e s i n the database. In a d d i t i o n to the c l a u s e s , t h e i r p o s i t i o n s ( c l a u s e numbers) i n the database are a l s o i n d i c a t e d . CLEAR Th i s command removes a l l the the c l a u s e s from the database. 4.3 Environment Commands The environment commands are used f o r s e t t i n g the parameters of the environment i n which r e f u t a t i o n i s performed. There are a l t o g e t h e r s i x a d j u s t a b l e parameters i n the environment of the LRTP, and t h e i r v a l u e s can be d i s c l o s e d by the ENV command. For each parameter, there i s a command which allows the user to a d j u s t i t s v a l u e . METHOD When t h i s command i s entered, the system w i l l prompt the user to s e l e c t one of the f o l l o w i n g methods f o r p r o v i n g the theorem: FOLR - Ordered L i n e a r R e s o l u t i o n using Frames to re c o r d i n f o r m a t i o n of r e s o l v e d l i t e r a l s OLR - Ordered L i n e a r R e s o l u t i o n (without frames) LIR - L i n e a r Input R e s o l u t i o n Note that i f FOLR i s chosen, the switch f o r t a u t o l o g y 60 check w i l l be turned on a u t o m a t i c a l l y s i n c e t a u t o l o g y i s not allowed to e x i s t i n t h i s method. TAUT T h i s i s the command to change the switch value f o r ta u t o l o g y check. When t h i s command i s entered, the system w i l l prompt the user to respond with 'Y' or ' N' . Answers other than 'Y', 'YES', or 'ON' w i l l be regarded as 'N'. Note t h a t , however, the system w i l l not accept 'N' when FOLR has been chosen as the r e s o l u t i o n method. SUBSUME The user can use t h i s command to change the switch value f o r subsumption check. Again, only 'Y', 'YES', or 'ON' are c o n s i d e r e d as a f f i r m a t i v e answers. Forward subsumption w i l l be performed when t h i s switch i s on. TOP T h i s command causes the system to prompt the user f o r the top c l a u s e number. If that number corresponds to a c l a u s e in the database, the c l a u s e w i l l be used as the top c l a u s e i n the deduction. SHORT When t h i s command i s entered, the system w i l l prompt the user to set the switch f o r o b t a i n i n g the s h o r t e s t l i n e a r r e f u t a t i o n ( i f there i s one). To turn the switch on, one has to enter 'Y', 'YES', or 'ON', any other response w i l l t u rn the switch o f f . STEPS T h i s command i s used f o r s e t t i n g the depth bound of the search f o r the p r o o f . 61 4.4 E x i t Commands There are three commands that allow the user to e x i t the LRTP and they are d e s c r i b e d below: PROLOG When t h i s command i s used, the system w i l l e x i t and re t u r n to l e v e l of the PROLOG/MTS i n t e r p r e t e r , l e a v i n g the LRTP loaded, and the workspace i n t a c t . The LRTP can be re - e n t e r e d by using LRTP as a goal c l a u s e . MTS STOP T h i s command i s e q u i v a l e n t to the PROLOG command except that the system r e t u r n s to the MTS command l e v e l r a t h e r than the PROLOG/MTS i n t e r p r e t e r l e v e l . Consequently, the system can be re-e n t e r e d with a MTS r e s t a r t command. The e f f e c t of t h i s command i s to release; a l l workspace storage, and to unload both the LRTP and the PROLOG/MTS i n t e r p r e t e r . 62 5 Sample Terminal Session #$r plog:v2_prolog par=ws=256 #Execution begins PROLOG/MTS 0.2 Please enter a command: {Type "HELP" fo r a s s i s t a n c e ] PROVE. Enter a wff : {terminate input of wffs by NIL] P#Q. The wff has been converted t o : 1 : P#Q Enter a wff : {terminate input of wffs by NIL] -P#Q. The wff has been converted t o : 2: -P#Q Enter a wff : {terminate input of wffs by NIL] -P#-Q. The wff has been converted t o : 3: -P#-Q Enter a wff : {terminate input of wffs by NIL] P#-Q. The wff has been converted t o : 4: P#-Q Enter a wff : {terminate input of wffs by NIL] NIL. C l a u s e ( s ) i n c u r r e n t database :-1 : P#Q 2: -P#Q 3: -P#-Q 4: P#-Q S e l e c t one of the f o l l o w i n g methods:-FOLR - Ordered L i n e a r R e s o l u t i o n with Frame OLR - Ordered L i n e a r R e s o l u t i o n LIR - L i n e a r Input R e s o l u t i o n OLR. Tautology Check ? Y/N Y. Subsumption Check ? Y/N N. S h o r t e s t l i n e a r proof ? Y/N N. Max. no. of steps : 6. 63 Top c l a u s e no. : 1 . (1) P#Q has been chosen as top cl a u s e Proof: {length of proof = 6} (1) P#Q (2) -P#Q (6) Q <==FACTOR== (5) Q#Q. (3) -P#-Q (7) -P (I) P#Q (8) Q (3) -P#-Q (9) -P (4) P#-Q (10) -Q (II) Q <==FACTOR== (5) Q#Q NULL No. of u n i f i c a t i o n s i n v o l v e d i n : R e s o l u t i o n Subsumption Checks Tautology Checks 72 0 0 Command: SHORT. Sh o r t e s t l i n e a r proof ? Y/N Y. Command: PROVE. Proo f : {length of proof = 4} (1) P#Q (2) -P#Q (6) Q <==FACTOR== (5) Q#Q (3) -P#-Q (7) -P (4) P#-Q (8) -Q (9) Q <==FACTOR== (5) Q#Q NULL No. of u n i f i c a t i o n s i n v o l v e d i n : R e s o l u t i o n Subsumption Checks Tautology Checks 197 0 4 Command: STOP. EXIT PROLOG/MTS 0.2 #Execution terminated 65 Appendix B - Program L i s t i n g Of The LRTP /******************* THE TRANSLATOR ********************/ OP('=>',RL,33). OP(=,RL,33). OP(#,RL,37). OP($,RL,38). OP(-,PREFIX,39). /* Convert a formula to c l a u s a l form */ t r a n s l a t e ( * x , * x 6 ) <- implout(*x,*x1) & negin(*x1,*x2) & skolem(*x2,*x3,NIL) & univout(*x3,*x4) & conjn(*x4,*x5) & form 1 i s t ( * x 5 , * x 6 ) . /* Removing i m p l i c a t i o n s */ implout((*p = *q) <- / & implout implout((*p => *q <- / & implout i m p l o u t ( a l l ( * x , * p <- / & implout i m p l o u t ( e x i s t s ( * x <- / & implout i m p l o u t ( ( * p $ *q) <- / & implout i m p l o u t ( ( * p # *q) <- / & implout ((*p1 $ *q1) # ("*p1 $ -*q1))) *P,*p1 ,(~*P1 *p,*p1 , a l l ( * *p,*p1 *p),ex *p,*p1 (*P1 $ *p,*p1 (*p1 # *p,*p1 i m p l o u t ( ( - * p ) , ( - * p l ) ) <- / & implout(*p,*p1 implout(*p,*p). & implout(*q,*q1) # * q l ) ) & implout(*q,*q1). ,*P1)) • s t s ( * x , * p 1 ) ) • * q O ) & implout(*q,*q1). *q1 ) ) & implout(*q,*q1). /* Moving negation inwards */ negin((-*p),*p1) <-' / & neg(*p,*p1). n e g i n ( a l l ( * x , * p ) , a l l ( * x , * p 1 ) ) <- / & negin(*p,*p1). n e g i n ( e x i s t s ( * x , * p ) , e x i s t s ( * x , * p 1 ) ) <- / & negin(*p,*p1). n e g i n ( ( * p $ * q ) , ( * p l $ * q l ) ) <- / & negin(*p,*p1) & negin(*q,*q1). n e g i n ( ( * p # * q ) , (*p1 # *q1)) <- / & negin(*p,*p1) & negin(*q,*q1). n e g i n ( * p , * p ) . n e g ( ( - * p ) , * p l ) <- / £< negin (*p, *p1 ) . n e g ( a l l ( * x , * p ) , e x i s t s ( * x , * p 1 ) ) <- / & neg(*p,*p1). n e g ( e x i s t s ( * x , * p ) , a l l ( * x , * p 1 ) ) <- / & neg(*p,*p1). neg((*p $ *q),(*p1 # *q1)) <- / & neg(*p,*pl) & n e g ( * q , * q l ) . neg((*p # *q),(*p1 $ *q1)) <- / & neg(*p,*p1) & n e g ( * q , * q l ) . n e g ( * p , ( n o t ( * p ) ) ) . /* Skolemising */ s k o l e m ( a l l ( * x , * p ) , a l l ( * x , * p 1 ) , * v a r s ) <- / & skolem(*p,*p1,*x.*vars). s k o l e m ( e x i s t s ( * x , * p ) , * p 2 , * v a r s ) <- / & gensym(f,*f) & CONS(*f.*vars,*sk) & s u b s t i t u t e ( * x r * s k , * p , * p 1 ) & skolem(*p1,*p2,*vars). skolem((*p # *q),(*p1 # *q1),*vars) <- / & skolem( *p, *p1 , *vars) £< skolem(*q,*q1,*vars). skolem((*p $ *q),(*p1 $ * q l ) , * v a r s ) <- / & skolem(*p,*p1,*vars) & skolem(*q,*q1,*vars). skolem(*p,*p,*). /* Moving u n i v e r s a l q u a n t i f i e r s outwards 67 u n i v o u t ( a l l ( * x , * p ) , * p 1 ) <- / & u n i v o u t ( * p r * p 1 ) . u n i v o u t ( ( * p $ *q),(*p1 $ * q l ) ) <- / & univout(*p,*p1) & un i v o u t ( * q , * q 1 ) . u n i v o u t ( ( * p # *q),(*p1 # * q l ) ) <- / & univout(*p,*p1) & un i v o u t ( * q , * q 1 ) . u n i v o u t ( * p , * p ) . /* D i s t r i b u t i n g '$' over "#' */ c o n j n ( ( * p # * q ) , * r ) <- / & c o n j n ( * p , * p l ) & conjn(*q,*q1) & c o n j n l ( ( * p 1 # * q 1 ) , * r ) . c o n j n ( ( * p $ *q),(*p1 $ * q l ) ) <- / & conjn(*p,*p1) & conjn(*q,*q1). c o n j n ( * p , * p ) . c o n j n l ( ( ( * p $ *q) # * r ) , ( * p 1 $ *qD) <- / & c o n j n ( ( * p # *r),*p1) & c o n j n ( ( * q # * r ) , * q 1 ) . c o n j n l ( ( * p # (*q $ * r ) ) , ( * p 1 $ *qD) <- / & c o n j n ( ( * p # * q ) , * p l ) & c o n j n ( ( * p # * r ) , * q 1 ) . c o n j n l ( * p , * p ) . /* Convert to l i s t form f o r r e s o l u t i o n */ f o r m _ l i s t ( ( * p $ * q ) , * r ) <- / & f o r m _ l i s t ( * p , * p 1 ) & f o r m _ l i s t ( * q , * q 1 ) & combine(*pl,*q1,*r). f o r m _ l i s t ( ( * p # * q ) , ( * r ) . N I L ) <- / & f o r m _ l i s t ( * p , ( * p 1 ) . N I L ) & f o r m _ l i s t ( * q , ( * q 1 ) . N I L ) & combine(*p1,*q1,*r). f o r m _ l i s t ( * p , ( * p . N I L ) . N I L ) . /* Generate a unique symbol, *symbol, by c o n c a t e n a t i n g * l e t t e r with an i n t e g e r , * i n t e g e r */ gensym(*letter,*symbol) <- newsnum(*integer) & S T R I N G ( * i n t e g e r , * i n t l i s t ) & S T R I N G ( * s y m b o l , * l e t t e r . * i n t l i s t ) . symcount(1). newsnum(*integer) <- symcount(*integer) & a d d l ( * i n t e g e r , * n e x t ) & set(symcount(*next) , 1 ). /* S u b s t i t u t e each occurrence of *x i n the 3rd arg by *sk and r e t u r n r e s u l t i n 4th arg */ s u b s t i t u t e ( * x , * s k , ( * p # *q),(*p1 # *q1)) <- / & s u b s t i t u t e ( * x , * s k , * p , * p 1 ) & s u b s t i t u t e ( * x , * s k , * q , * q 1 ) . s u b s t i t u t e ( * x , * s k , ( * p $ *q),(*p1 $ *q1)) <- / & s u b s t i t u t e ( * x , * s k , * p , * p 1 ) & s u b s t i t u t e ( * x , * s k , * q , * q 1 ) . s u b s t i t u t e ( * x , * s k , * p , * p 1 ) <- sub_skel(*x,*sk,*p,*p1) & /. s u b s t i t u t e ( * , * , * p , * p ) . /* S u b s t i t u t e *sk f o r each occurrence of *x i n s t r u c t u r e *p and r e t u r n r e s u l t i n *p2 */ sub_skel(*x,*sk,*p,*p2) <- SKEL(*p) & CONS(*pred.*arglist,*p) & s u b s t ( * x , * s k , * a r g l i s t , * p 1 ) & CONS(*pred.*p1,*p2). /* C o n s t r u c t a new l i s t , *m, made up from elements of l i s t , * 1 , except that any occurrences of *x w i l l be r e p l a c e d by *a */ subst(*,*,NIL,NIL). subst(*x,*a,*var.*l,*a.*m) <- VAR(*var) & samevar(*x,*var) & / & s u b s t ( * x , * a , * l , * m ) . s u b s t ( * x , * a , * s . * r , * s 1 . *r1) <- sub_skel(*x,*a,*s,*s1) & / & s u b s t ( * x , * a , * r , * r 1 ) . subst(*x,*a,*y.*l,*y.*m) <- subst(*x,*a,* 1,*m). /*. Check i f *x and *y r e f e r to the same v a r i a b l e */ SAME(FALSE), samevar(*x,*y) <- b i n d t e s t ( * x , * y ) & SAME(TRUE) & set(SAME(FALSE),1). /* Check i f *x and *y are the same by b i n d i n g an atom to *x, i f they are the same, SAME i s add to the db b i n d t e s t ( * x , * y ) <- bind(*x) & ATOM(*y) & set(SAME(TRUE),1) & FAIL. b i n d t e s t ( * , * ) . bind(atom). 70 y'* *************** * THE COMMAND INTERPRETER *************/ /* I n i t i a l v alues */ CONTROL(ATTN,ON). ERROR(N). STATUS(CMD). METHOD(NIL). TAUT(NIL). SUBSUME(NIL). WFF(NIL). TOP(0,NIL). SHORT(NIL). SHORT STEPS(0). STEPSlNIL). FROM(OTHERS). CURRNUM(0). PROOF(NIL,0). CLAUSE(NIL). UNIFY_COUNT(R,0). UNIFY_COUNT(S,0). UNIFY COUNT(T,0). /* Command i n t e r p r e t e r */ LRTP <- setup & READ(*input) & exe c u t e ( * i n p u t ) & ready_for_next & co n t i n u e . /* E r r o r recovery */ ERROR <- set(ERROR(Y),1) & LRTP. /* Set up the LRTP */ setup <- ERROR(N) & / & p r i n t s ( ' P l e a s e enter a command: {Type "HELP" f o r a s s i s t a n c e } ' ) & setcase(CMD). setup <- set(ERROR(N),1) & p r i n t s ( ' E r r o r has been recovered, p l e a s e continue') & read y _ f o r _ n e x t . /* Convert a l l input to upper case when STATUS <> WFF */ setcase(WFF) <- update(CONTROL(LOWER,OFF),CONTROL(LOWER,ON)) & /. s e t c a s e ( * s t a t ) <- ->equ(*stat ,WFF) & update(CONTROL(LOWER,ON),CONTROL(LOWER,OFF)) & /. s e t c a s e ( * ) . /* Replace *oldax by *newax */ update(*oldax,*newax) <- DELAX(*oldax,*index) & ADDAX(*newax,*index). /* Process input a c c o r d i n g to c u r r e n t STATUS */ execute(* input) <- STATUS(*stat) & c o n c a t e n a t e ( p r o c e s s , * s t a t , * p r e d ) & CONS(*pred.* input.NIL,*process) & *process & /. /* Concatenate f i r s t two s t r i n g s and r e t u r n a 3rd s t r i n g c o n c a t e n a t e ( * i d 1 , * i d 2 , * i d 3 ) . <- STRING(*id1,* i d 1 l i s t ) & STRING(*id2,*id21ist) & c o m b i n e ( * i d 1 l i s t , * i d 2 l i s t , * i d 3 l i s t ) & S T R I N G ( * i d 3 , * i d 3 1 i s t ) . /* Get ready to accept next input */ ready_for_next <- STATUS(*stat) & prompt(*stat) & s e t c a s e ( * s t a t ) . /* Process command */ processCMD(HELP) <- describe_cmd. pr oc e s sCMD(PROVE) <- set(FROM(PROVE),1) & i n i t i a l i z e . processCMD(*cmd) <- member(*cmd,WFF.METHOD.TAUT.SUBSUME.TOP.SHORT .STEPS.DELETE.PROLOG.NIL) & set(STATUS(*cmd),1). processCMD(ENV) <- printENV. processCMD(LIST) <- l i s t C L A U S E . pr oc e s SCMD(CLEAR) <- flushCLAUSE(*) & set(TOP(0,NIL),2) & set(WFF(NIL),1). processCMD(MTS) <- MTS. processCMD(STOP) <- STOP. processCMD(*) <- p r i n t ( ' I l l e g a l command, type "HELP" f o r a s s i s t a n c e ' ) . /* T r a n s l a t e input wffs to c l a u s a l form and s t o r e them i n database */ processWFF(NIL) <- p r i n t s ( ' C l a u s e ( s ) i n c u r r e n t database :-') & listCLAUSE & i n i t i a l i z e . processWFF(*wff) <- t r a n s l a t e ( * w f f , * c l ) & p r i n t ( ' T h e wff has been converted to:') & a s s e r t ( * c l ) . processWFF(*) <- p r i n t ( ' I l l e g a l wff, t r y a g a i n ' ) . /* S e l e c t a method */ processMETHOD(*method) <- member(*method,FOLR.OLR.LIR.NIL) & set(METHOD(*method),1) & checkMETHOD(*method) & i n i t i a l i z e . p r oc e S sMETHOD(*) <- p r i n t ( ' T h i s method i s not a v a i l a b l e i n the LRTP'). /* Set the switch f o r t a u t o l o g y checks a c c o r d i n g to user response */ processTAUT(*yes) <- member(*yes,Y.YES.ON.NIL) & set(TAUT(Y),1) & i n i t i a l i z e . processTAUT(*) <- "-METHOD (FOLR) & set(TAUT(N),1) & i n i t i a l i z e . processTAUT(*) <- p r i n t ( ' T a u t o l o g y i s not allowed i n FOLR') & i n i t i a l i z e . /* Set the switch f o r subsumption checks a c c o r d i n g to user response */ processSUBSUME(*yes) <- member(*yes,Y.YES.ON.NIL) & set (SUBSUME(Y) , 1 ) 6. i n i t i a l i z e . processSUBSUME(*) <- set(SUBSUME(N),1) & i n i t i a l i z e . /* S e l e c t top cl a u s e */ processTOP(*top) <- INT(*top) & AXN(CLAUSE,2,CLAUSE(A,*topelause),*top) & p r i n t e l ( * t o p ) & p r i n t ( ' has been chosen as top c l a u s e ' ) & set( T O P ( * t o p , * t o p c l a u s e ) , 2 ) & i n i t i a l i z e . processTOP(*) <- p r i n t ( ' C l a u s e not i n database, t r y a g a i n ' ) . /* Set the switch f o r s h o r t e s t l i n e a r r e f u t a t i o n processSHORT(*yes) <- member(*yes,Y.YES.ON.NIL) & set(SHORT(Y),1) & i n i t i a l i z e . processSHORT(*) <- set(SHORT(N),1) & i n i t i a l i z e . /* Enter max. no. of steps i n t o database */ 74 processSTEPS(*maxsteps) <- INT(*maxsteps) & set (STEPS(*maxsteps) , 1 ) S. i n i t i a l i z e . processSTEPS(*) <- p r i n t ( ' M a x . no. of steps must be an i n t e g e r , t r y a g a i n ' ) . /* De l e t e c l a u s e a c c o r d i n g to input c l a u s e no. */ processDELETE(*clnum) <- INT(*clnum) & p r i n t c l ( * c l n u m ) & p r i n t ( ' has been d e l e t e d ' ) & DELAX(CLAUSE(*,*),*clnum) & resetTOP(*clnum) & set(STATUS(CMD),1). processDELETE(*) <- p r i n t ( ' C l a u s e not i n database') & set(STATUS(CMD),1). /* Prompt user f o r i n i t i a l v alues i f there i s one */ INIT(WFF). INIT (METHOD). INIT(TAUT). INIT(SUBSUME). INIT(SHORT). INIT(STEPS). i n i t i a l i z e <- FROM(OTHERS) & set(STATUS(CMD),1). i n i t i a l i z e <- I N I T ( * s t a t ) & CONS(*stat.NIL.NIL,*null) & • n u l l & set (STATUS (*stat) , 1 )'. i n i t i a l i z e <- TOP(0,NIL) & set(STATUS(TOP),1). i n i t i a l i z e <- set(FROM(OTHERS),1) & set(STATUS(CMD),1) & g e t p r o o f . 75 /* Prompt user a c c o r d i n g to c u r r e n t STATUS */ prompt(CMD) <- prints('Command:'). prompt(WFF) <- p r i n t s ( ' E n t e r a wff : {terminate input of wffs by NIL}'). prompt(METHOD) <- p r i n t s ( ' S e l e c t one of the f o l l o w i n g methods:-') & p r i n t ( ' FOLR - Ordered L i n e a r R e s o l u t i o n with Frame') & p r i n t ( ' OLR - Ordered L i n e a r R e s o l u t i o n ' ) & . p r i n t ( ' LIR - L i n e a r Input R e s o l u t i o n ' ) . prompt(TAUT) <- p r i n t s ( ' T a u t o l o g y Check ? Y/N'). prompt(SUBSUME) <- prints('Subsumption Check ? Y/N'). prompt(TOP) <- p r i n t s ( ' T o p c l a u s e no. : ' ) . prompt(SHORT) <- p r i n t s ( ' S h o r t e s t l i n e a r proof ? Y/N'). prompt(STEPS) <- pr i n t s ( ' M a x . no. of steps : ' ) . prompt(DELETE) <- p r i n t s ( ' C l a u s e no. : ' ) . prompt(PROLOG). /* Return to Prolog i n t e r p r e t e r when STATUS=PROLOG */ continue <- STATUS(PROLOG) & set(STATUS(CMD),1). /* P r i n t out the command menu */ describe_cmd <- prints('Commands a v a i l a b l e : ' ) & p r i n t ( ' PROVE - prove a theorem') & p r i n t C WFF - enter wffs i n t o database') & p r i n t C METHOD - s e l e c t a r e s o l u t i o n method') & p r i n t ( ' TAUT - change switch value of t a u t o l o g y check') & p r i n t ( ' SUBSUME - change switch value of subsumption check') & p r i n t ( ' TOP - s e l e c t a top c l a u s e ' ) & p r i n t ( ' SHORT - change switch value f o r s h o r t e s t l i n e a r proof & p r i n t ( ' STEPS - enter max. no. of steps (depth bound)') & p r i n t ( ' ENV - p r i n t parameter values of environment') & - l i s t a l l c l a u s e s i n database') & - d e l e t e c l a u s e ( s ) i n database') & - c l e a r a l l c l a u s e s i n database') & - r e t u r n to Prol o g i n t e r p r e t e r ' ) & - r e t u r n to MTS') & - stop the theorem prover') & - p r i n t command menu') & p r i n t s ( ' P l e a s e enter one of the above commands'). p r i n t ( ' LIST p r i n t ( ' DELETE p r i n t ( ' CLEAR pr i n t ( ' PROLOG pr i n t ( ' MTS p r i n t ( ' STOP p r i n t ( ' HELP /* P r i n t out the values of parameters i n the environment * printENV <- METHOD(*method) & TAUT(*yesno1) & SUBSUME(*yesno2) & TOP(*top,*topclause) & f o r m _ c l a u s e ( * t o p c l a u s e , * c l ) & SHORT(*yesno3) & STEPS(*maxsteps) & p r i n t l n ( ' M e t h o d = '.*method.NIL) & p r i n t l n ( ' T a u t o l o g y Check = '.*yesno1.NIL) & pr i n t l n ( ' S u b s u m p t i o n Check = '.*yesno2.NIL) & p r i n t l n ( ' T o p c l a u s e no. = ',*top.' ; Top c l a u s e = '.*cl.NIL) p r i n t l n ( ' S h o r t e s t l i n e a r proof = '.*yesno3.NIL) & pr i n t In (' Max. no. of steps = ' . *maxsteps .NIL) . /* L i s t out a l l c l a u s e s i n database */ listCLAUSE <- AXN(CLAUSE,2,CLAUSE(*,*cl),*n) & d i s p l a y ( * n , * c l ) & FAIL. l i s t C L A U S E . /* F l u s h c l a u s e ( s ) which are of *type */ flushCLAUSE(*type) <- AXN(CLAUSE,2,CLAUSE(*type,*),*clnum) & DELAX(CLAUSE(*type,*),*clnum) & FAIL. flushCLAUSE(*). /* Add c l a u s e s to database */ a s s e r t ( N I L ) . assert('*cl1 , * c l 2 ) <- s c r e e n ( * c l 1 , 0 , * c l i s t ) & set(WFF(NON_NIL), 1 ) & ADDAX(CLAUSE(A,*cl1),*n) & 77 d i s p l a y ( * n , * c l 1 ) & s u b m s g ( * c l i s t ) & a s s e r t ( * c l 2 ) . a s s e r t ( * . * c l ) <- a s s e r t ( * c l ) . /* D i s p l a y a cl a u s e and i t s no. */ d i s p l a y ( * n , * c l ) <- f o r m _ c l a u s e ( * c l , * c l a u s e ) & p r i n t l n ( * n . ' : ' . * c l a u s e . N I L ) . /* P r i n t subsumption message i f there i s any */ submsg(NIL) <- /. s u b m s g ( * c l i s t ) <- p r i n t ( ' w h i c h subsumes the f o l l o w i n g c l a u s e ( s ) i n database:') & p r i n t _ d e l e t e ( * c l i s t ) . /* P r i n t out a l i s t of subsumed c l a u s e ( s ) and d e l e t e them */ p r i n t _ d e l e t e ( N I L ) . p r i n t _ d e l e t e ( * c l n u m . * c l i s t ) <- p r i n t c l ( * c l n u m ) & p r i n t ( ' {being deleted}') & DELAX(CLAUSE(*,*),*clnum) & p r i n t _ d e l e t e ( * c l i s t ) . /* Update *oldax when given *newax and i t s * a r i t y */ set(* n e w a x , * a r i t y ) <- CONS(*pred.*,*newax) & AXN(*pred,*arity,*oldax) & update(*oldax,*newax) & /. /* I f METHOD=FOLR, t a u t o l o g y checks i s compulsory */ checkMETHOD(FOLR) <- set(TAUT(Y),1) & p r i n t ( ' T a u t o l o g y checks = Y'). chec kMETHOD(*). /* Reset top cl a u s e to n u l l value when i t i s d e l e t e d */ resetTOP(*deleted) <- TOP(*deleted,*) & set(TOP(0,NIL),2) . resetTOP{*). /* Set up COUNTS r f i n d a proof, p r i n t the proof » and f l u s h a l l c l a u s e s except those input by user */ getproof <- r e s e t & f i n d p r o o f & p r i n t p r o o f & flushCLAUSE(R) & flushCLAUSE(F). /* Reset UNIFY_COUNTs to zero and copy STEPS to SHORT_STEPS before r e s o l v i n g */ res e t <- UNIFY_COUNT(*type,*) & update(UNIFY_COUNT(*type,*), UNIFY_COUNT(*type,0)) & FAIL. re s e t <- STEPS(*maxsteps) & set(SHORT_STEPS(*maxsteps), 1 ) . /*• R e t r i e v e top c l a u s e and s t a r t p r o v i n g */ fi n d p r o o f <- TOP(*topclnum,*topcl) & set(PROOF(NIL,0),2) & factoring(*topelnum,*tope 1,*cclause,*cclnums) & prove(*cclnums,*cclause,NIL,0). f i n d p r o o f . /* P r i n t out the proof */ p r i n t p r o o f <- PROOF(NIL,*) & NEWLINE & p r i n t s ( ' C a n n o t be proved i n given s e t t i n g ' ) . p r i n t p r o o f <- PROOF(*proof,*length) & NEWLINE & p r i n t l n ( ' P r o o f : {length of proof = ' .*length.'}'.NIL) p r i n t p r o o f 1 ( * p r o o f ) & print('NULL') & NEWLINE & pr i n t s t a t i s t i c s . p r i n t p r o o f 1 ( N I L ) . p r i n t p r o o f 1 ( * p f 1 . * p f 2 ) <- p r i n t p r o o f 1 ( * p f 2 ) & p r i n t c l p a i r ( * p f 1 ) . /* P r i n t out u n i f i c a t i o n s t a t i s t i c s */ p r i n t s t a t i s t i c s . <- UNIFY_COUNT(R,*rcount) & UNIFY_COUNT(S,*scount) & UNIFY COUNT(T,*tcount) & p r i n t T ' N o . of u n i f i c a t i o n s i n v o l v e d i n :') & p r i n t ( ' R e s o l u t i o n Subsumption Checks Tautology Checks') p r i n t l n ( ' '.*rcount.' '.*scount ',*tcount.NIL). /* P r i n t out the two r e s o l v e d c l a u s e s */ p r i n t c l p a i r ( * c c l n u m s . * c l n u m s ) <- p r i n t f a c t o r ( * c c l n u m s ) & p r i n t b a r ( 2 ) & WRITECH(' | ') & p r i n t f a c t o r ( * c l n u m s ) & pr i n t b a r ( 2 ) . /* P r i n t a c l a u s e together with i t s f a c t o r i f there i s one pr intfactor(*facnum.*clnum) <- p r i n t p c l ( * f a c n u m ) & WRITECHC <==FACTOR== ') & p r i n t p c l ( * c l n u m ) & NEWLINE. p r i n t f a c t o r ( * c l n u m ) <- p r i n t p c l ( * c l n u m ) & NEWLINE. /* P r i n t a c l a u s e as p a r t of proof */ p r i n t p c l ( 0 ) <- WRITECHC r e d u c t i o n ' ) . p r i n t p c l ( * c l n u m ) <- AXN(CLAUSE,1,CLAUSE(*cl),*clnum) & f o r m _ c l a u s e ( * c l , * c l a u s e ) & p r i n t o n ( ' ( ' . * c l n u m . ' ) ' . * c l a u s e . N I L ) . /* P r i n t a c l a u s e */ p r i n t c l ( * c l n u m ) <- AXN(CLAUSE,2,CLAUSE(*,*cl),*clnum) & f orm_clau.se(*cl, * c l a u s e ) & p r i n t o n ( ' ( ' . * c l n u m . ' ) ' . * c l a u s e . N I L ) . /* Form a c l a u s e from a l i s t f o r output f o r m _ c l a u s e ( * l i t . N I L , * l i t 1 ) <- / & c h e c k n o t ( * l i t , * l i t 1 ) . f o r m _ c l a u s e ( * l i t . * c l , * l i t 1 # * c l l ) <- c h e c k n o t ( * l i t , * l i t 1 ) & f o r m _ c l a u s e ( * c l , * c l 1 ) . form_clause(NIL,NIL). /* Replace 'not' by ' -' */ c h e c k n o t ( n o t ( * l i t ) , - * l i t ) <- /. c h e c k n o t ( * l i t , * l i t ) . /* P r i n t out '|' */ p r i n t b a r ( O ) <- /. pr i n t b a r ( * n ) <- p r i n t ( ' |') & subl(*n,*n1) & p r i n t b a r ( * n 1 ) . /* P r i n t t e x t u t i l i t i e s */ p r i n t s ( * x ) <- NEWLINE & p r i n t ( * x ) . p r i n t ( * x ) <- WRITECH(*x) & NEWLINE. p r i n t l n ( N I L ) <- NEWLINE. p r i n t l n ( * h d . * t l ) <- WRITECH(*hd) & p r i n t l n ( * t l ) . p r i n t o n ( N I L ) . p r i n t o n ( * h d . * t l ) <- WRITECH(*hd) p r i n t o n ( * t l ) . 82 / * * * * * * * * * * * * * * * * * TJ-JFJ R E F U T A T I O N MODULE * * * * * * * * * * * * * * * * * * * / /* Prove a c l a u s e (2nd a r g ) , i t s no. (1st a r g ) , and r e t u r n the proof (3rd arg) and len g t h (4th arg) of proof */ p r o v e ( * , N I L , * p r o o f , * l e n g t h ) <- SHORT_STEPS(*maxsteps) & LE(*length,*maxsteps) & s e t ( P R O O F ( * p r o o f , * l e n g t h ) , 2 ) & sto r e _ p r o o f & s h o r t e s t _ o r _ 1 s t ( * l e n g t h ) . p r o v e ( * c c l n u m s , * c c l a u s e , * p f s o f a r , * l e n s o f a r ) <- l i m i t c h e c k ( * c c l a u s e , * l e n s o f a r ) & r e s o l v e ( * c l n u m s , * c c l a u s e , * r e s o l v e n t , * l e n s o f a r ) & sto r e ( R , * r e s n u m , * r e s o l v e n t ) & f a c t o r i n g ( * r e s n u m , * r e s o l v e n t , * f a c c l , * f a c n u m s ) & screen(*faccl,*facnums,0) & a d d l ( * l e n s o f a r , * l e n p l u s 1 ) & red u c e _ r e s o l v e n t ( * f a c n u m s , * f a c c l , * r e d n u m , * r e d c l , (*cclnums.*clnums),*pfsofar,*proof,*lenplus1,*newlen) & prove(*rednum,*redcl,*proof,*newlen). /* Store up a l l c l a u s e s i n v o l v e d i n the proof */ sto r e _ p r o o f <- CLAUSE(*cl) & DELAX(CLAUSE(*cl)) & FAIL. s t o r e _ p r o o f <- CLAUSE(*,*cl) & ADDAX(CLAUSE(*cl)) & FAIL. s t o r e _ p r o o f . /* Check i f s h o r t e s t or f i r s t proof i s r e q u i r e d */ s h o r t e s t _ o r l s t ( * ) <- SHORTTN). s h o r t e s t _ o r 1 s t ( * l e n g t h ) <- SHORTTY) & s u b l ( * l e n g t h , * l e n l e s s 1 ) & s e t ( S H 0 R T _ S T E P S ( * l e n l e s s 1 ) , 1 ) & ANCESTOR(*prove,2) & R E T R Y ( * p r o v e ) . /* Suceeds i f f l i m i t not exceeded */ 1 i m i t e h e e k ( * c c l a u s e , * l e n s o f a r ) 83 <- _ , e q u ( * c c l a u s e ,NIL) & SHORT_STEPS(*maxsteps) & L T ( * l e n s o f a r , * m a x s t e p s ) & l e n g t h ( * c c l a u s e , * c c l e n ) & D I F F ( * m a x s t e p s , * l e n s o f a r , * s t e p s l e f t ) & G E ( * s t e p s l e f t , * c c l e n ) . /* R e s o l v e a c l a u s e ( 2 n d arg) w i t h a n o t h e r c l a u s e whose no. i s s p e c i f i e d i n 1st a r g , and r e t u r n r e s o l v e n t i n 3rd a r g */ r e s o l v e ( * c l n u m s , * 1 i t . * c l , * r e s o l v e n t , * l e n s o f a r ) <- n e g a t e ( * l i t , * n o t l i t ) & s e l e c t ( * c l n u m , * c l a u s e ) & f a c t o r i n g ( * c l n u m , * c l a u s e , * f a c t o r , * c l n u m s ) & r e s o l v a b l e ( R , * n o t l i t , * f a c t o r , * n e w c l a u s e ) & form r e s o l v e n t ( * n e w c l a u s e , * 1 i t . * c l , * r e s o l v e n t ) . /* S t o r e c l a u s e i n database and remove i t on f a i l u r e */ s t o r e ( * , * , N I L ) <- /. s t o r e ( * t y p e , * c l n u m , * c l a u s e ) <- ADDAX(CLAUSE(*type,*clause),*clnum) & set(CURRNUM(*clnum),1). s t o r e ( * t y p e , * , * c l a u s e ) <- CURRNUM(*clnum) & subl(*clnum,*currnum) & set(CURRNUM(*currnum),1) & DELAX(CLAUSE(*type,*clause),*clnum) & FAIL. /* F a c t o r i s e the c l a u s e ( 2 n d arg) i f p o s s i b l e and s t o r e the f a c t o r ( 3 r d arg) i n database i f i t e x i s t s */ f a c t o r i n g ( * c l n u m , * c l a u s e , * f a c t o r , ( * f a c n u m . * c l n u m ) ) <- f a c t o r ( R , * c l a u s e , * f f a c t o r ) & - • e q u ( * c l a u s e , * f f a c t o r ) & l a s t _ f r a m e ( * f f a c t o r , * f a c t o r ) & s t o r e ( F , * f a c n u m , * f a c t o r ) . f a c t o r i n g ( * c l n u m , * c l a u s e , * c l a u s e , * c l n u m ) <- f a c t o r ( X , * c l a u s e , * c l a u s e ) . /* Reduce the r e s o l v e n t i f the method i s FOLR */ r e d u c e _ r e s o l v e n t ( * f n u m , * f , * f n u m , * f , * p r , * p f , * p r . * p f , * l e n , * l e n ) <- "-METHOD(FOLR) 6 /. r e d u c e _ r e s o l v e n t ( * f n u m , * f , * r n u m , * r , * p r , * p f , ( * f n u m . O ) . * p r . * p f , * len,*newlen) 84 <- 1 i m i t c h e c k ( * f , * l e n ) & reduce(R,*f,*r) & - ,equ(*f,*r) & store(R,*rnum,*r) & ad d l ( * l e n , * n e w l e n ) . r e d u c e _ r e s o l v e n t ( * f n u m , * f , * f n u m , * f , * p r , * p f , * p r . * p f , * l e n , * l e n ) <- r e d u c e ( X , * f , * f ) . /* Negate 1st arg and re t u r n i n 2nd arg f o r r e s o l u t i o n */ n e g a t e ( n o t ( * 1 i t ) , * l i t ) <- /. n e g a t e ( * l i t , n o t ( * l i t ) ) . /* S e l e c t a c l a u s e f o r r e s o l v i n g */ s e l e c t ( * c l n u m , * c l a u s e ) <- AXN(CLAUSE,2,CLAUSE(A,*clause),*clnum). select(*c1num,*clause) <- METHOD(OLR) & AXN(CLAUSE,2,CLAUSE(R,*clause),*clnum). /* Resolvable i f f 2nd arg i s a member of 3rd arg and r e t u r n the r e s o l v e d c l a u s e i n 4th arg */ r e s o l v a b l e ( * t y p e , * 1 i t,FRAMED(*).*cl,*newcl) <- / & r e s o l v a b l e ( * t y p e , * 1 i t , * c l , * n e w c l ) . r e s o l v a b l e ( * t y p e , * l i t 1 , * l i t 2 . * c l , * c l ) <- u n i f y ( * t y p e , * l i t 1 , * l i t 2 ) . r e s o l v a b l e ( * t y p e , * l i t , * l . * c l , * l . * n e w e l ) <- r e s o l v a b l e ( * t y p e , * l i t , * c l , * n e w e l ) . /* Form r e s o l v e n t a c c o r d i n g to method used */ f o r m _ r e s o l v e n t ( * c l a u s e , * l i t . * c l , * r e s o l v e n t ) <- METHOD(FOLR) & / & c o m b i n e ( * c l a u s e , F R A M E D ( * l i t ) . * c l , * r e s c l ) & l a s t _ f r a m e ( * r e s c l , * r e s o l v e n t ) . f o r m _ r e s o l v e n t ( * c l a u s e , * l i t . * c l , * r e s o l v e n t ) <- METHOD(LIR) & / & c o m b i n e ( * c l a u s e , * c l , * r e s o l v e n t ) . f o r m _ r e s o l v e n t ( * c l a u s e , * l i t . * c l , * r e s o l v e n t ) <- c o m b i n e ( * c l a u s e , * c l , * r e s o l v e n t ) . /* Merge common f a c t o r to the l e f t */ f a c t o r ( * , N I L , N I L ) . factor(*type,FRAMED(*1i t).*cl,FRAMED(*1it).*newcl) <- / & f a c t o r ( * t y p e , * c l , * n e w c l ) . f a c t o r ( * t y p e , * l i t . * c l , * f a c t o r ) <- member(*type,*1it,*cl) & f a c t o r ( * t y p e , * c l , * f a c t o r ) . f a c t o r ( * t y p e , * l i t . * c l , * l i t . * n e w c l ) <- f a c t o r ( * t y p e , * c l , * n e w c l ) . /* Reduce goal c l a u s e i f the l a s t l i t e r a l can be r e s o l v e d with a framed l i t e r a l */ reduce(*,NIL,NIL) <-•/. r e d u c e ( * t y p e , * 1 i t . * c l , * r e d u c e d ) <- n e g a t e ( * l i t , * n o t l i t ) & m e m b e r f ( * t y p e , * n o t l i t , * c l ) & l a s t _ f r a m e ( * c l , * r e d u c e d ) . r e d u c e ( * , * l i t . * c l , * l i t . * c l ) <- n e g a t e ( * l i t , * n o t l i t ) & -•memberf ( X , * n o t l i t , * c l ) . /* Remove the l a s t l i t e r a l i f i t i s framed */ last_frame(FRAMED(*).*cl,*newcl) <- / & l a s t _ f r a m e ( * c l , * n e w c l ) . l a s t _ f r a m e ( * c l a u s e , * c l a u s e ) . /* Length r e t u r n s the length(2nd arg) of a c l a u s e ( l s t a r g ) . Framed l i t e r a l s are not counted */ len g t h ( N I L , 0 ) . length(FRAMED(*).*cl,*len) <- / & l e n g t h ( * c l , * l e n ) . l e n g t h ( * . * c l , * l e n p l u s 1 ) <- l e n g t h ( * c l , * l e n ) & a d d l ( * l e n , * l e n p l u s 1 ) . /* Member succeeds i f f 2nd arg i s a member of 3rd arg and the UNIFY_COUNT i s incremented a c c o r d i n g to *type; n o t i c e that framed l i t e r a l does not a f f e c t the count */ membe r ( * t ype,*1i t,FRAMED(*).*c1) <- / & m e m b e r ( * t y p e , * l i t , * c l ) . member(*type,*1it 1 , * l i t 2 . * ) <- u n i f y ( * t y p e , * l i t 1 , * l i t 2 ) . m e m b e r ( * t y p e , * l i t , * . * c l ) <- m e m b e r ( * t y p e , * l i t , * c l ) . /* Memberf succeeds i f f the c l a u s e i s r e d u c i b l e ; n o t i c e non-framed l i t e r a l does not a f f e c t the count */ memberf(*type,*lit1,FRAMED(* 1 i t 2 ) . * ) <- u n i f y ( * t y p e , * l i t 1 , * l i t 2 ) . m e m b e r f ( * t y p e , * l i t , * . * c l ) <- m e m b e r f ( * t y p e , * l i t , * c l ) . /* Increment UNIFY_COUNT by 1 ac c o r d i n g to *type. No count i s incremented i f *type=X */ incrUNIFY_COUNT(X) <- /. i ncrUNIFY_COUNT(*type) <- UNIFY_COUNT(*type,*count) & addl(*count,*countplus1) & update(UNIFY_COUNT(*type,*), UNIFY_COUNT(*type,*countplus1)). /* Combine 1st l i s t with 2nd l i s t to form a 3rd l i s t */ combine(NIL,*x,*x) <- /. combine(*head.*tai1,*x,*head.*newtai1) <- combine(*tai1,*x,*newtai1). /* *x - 1 = *y */ sub l ( * x , * y ) <- DIFF(*x,1,*y). /* * x + 1 = *y */ add1(*x,*y) <- DIFF(*x,'-1',*y). /* Succeed i f f 1st arg equals to 2nd arg */ equ(*x,*x). /* Succeed i f f f i r s t arg i s a member of second arg */ m e m b e r ( * l i t , * l i t . * c l ) <- /. 87 m e m b e r ( * l i t , * . * c l ) <- m e m b e r ( * l i t , * c l ) . 88 y****************** THE DELETION MODULE *******************/ /* Check i f d e l e t i o n s t r a t e g i e s have to be a p p l i e d */ screen(NIL,*,*) <- /. s c r e e n ( * c l , * f a c n u m s , * c l i s t ) <- t a u t _ t e s t ( * c l ) & subsume_test1(*cl,*facnums) & subsume t e s t 2 ( * c l , * c l i s t ) . /* Test i f the c l a u s e i s a t a u t o l o g y */ t a u t _ t e s t ( * ) <- TAUT(N) & -METHOD(FOLR) & -STATUS(WFF) & /. IS_TAUT(N). t a u t _ t e s t ( * c l ) <- set(IS_TAUT(N),1) & t a u t o l o g y ( * c l ) & set(IS_TAUT(Y),1) & FAIL. t a u t _ t e s t ( * ) <- IS_TAUT(N) & /. t a u t _ t e s t ( * t a u t ) <- IS_TAUT(Y) & tautmsg(*taut) & / & FAIL. /* Test i f the input c l a u s e i s subsumed by another c l a u s e i n db */ SUBSUME_CLAUSE(NIL). SUBSUMED_CLAUSE(NIL). subsume_test1(*,*) <- SUBSUME(N) & -STATUS(WFF) & /. subsume_test1(*fcl,*facnums) <- set(SUBSUME_CLAUSE(NIL),1) & remove f r a m e s ( * f c l , * s u b c l ) & groundT*subcl) & set (SUBSUMED_CLAUSE(*subcl) , 1 ) S< subsumed(*subcl,*facnums,*clnum) & set(SUBSUME_CLAUSE(*clnum),1) & FAIL. subsume_test1(*,*) <- SUBSUME_CLAUSE(NIL) & /. subsume_test1(*subcl,*) <- SUBSUME_CLAUSE(*clnum) & submsg(*subcl,*clnum) & / & FAIL. /* Test i f input c l a u s e subsumes any c l a u s e ( s ) in db & d e l e t e them */ subsume_test2(*,*) <- -STATUS(WFF) & /. subsume_test2(*cl,*) <- set(SUBSUME_CLAUSE(NIL),1) & AXN(CLAUSE,2,CLAUSE(*,*clause),*clnum) & ground(*clause) & set(SUBSUMED_CLAUSE(*clause),1) & subsumed_by(*clause,*cl) & SUBSUME_CLAUSE(*clist) & set(SUBSUME_CLAUSE(*clnum.*clist),1) & . FAIL. s u b s u m e _ t e s t 2 ( * , * c l i s t ) <- SUBSUME C L A U S E ( * c l i S t ) . /* Succeeds i f f the a r g . i s a t a u t o l g y */ tautology(FRAMED(*),*cl) <- / & t a u t o l o g y ( * c l ) . t a u t o l o g y ( * l i t . * c l ) <- n e g a t e ( * l i t , * n o t l i t ) & member ( T , * n o t l i t , * c l ) & /. t a u t o l o g y ( * . * c l ) <- t a u t o l o g y ( * c l ) . /* Replace a l l v a r i a b l e s i n the c l a u s e by d i s t i n c t i v e c o n s t a n t s (atoms s t a r t i n g with a l e t t e r 'c') */ ground(NIL). ground(*x.*y) <- VAR(*x) & gensym(c,*x) & / & ground(*y). ground(FRAMED(*).*cl) <- / & g r o u n d ( * c l ) . ground(*x.*y) <- C O N S ( * . * a r g l i s t , * x ) & g r o u n d ( * a r g l i s t ) & ground(*y) & /. /* Removes a l l frames i n 1st arg and r e t u r n s r e s u l t i n 2nd arg */ remove_frames(NIL,NIL). remove frames(FRAMED(*).*cl,*newcl) <- 7 & remove_frames(*cl,*newcl). r e m o v e _ f r a m e s ( * l i t . * c l , * l i t . * n e w c l ) <- remove_frames(*cl,*newcl). /* Succeeds i f f * s u b c l i s subsumed by a c l a u s e (whose no. i s *clnum) in the c u r r e n t database */ subsumed(*subcl,*facnums,*clnum) <- AXN(CLAUSE,2,CLAUSE(*,*clause),*clnum) & - - i t s e l f (*clnum,*facnums) & subsumed_by(*subcl,*clause) & /. /* Succeeds i f f 1st arg i s subsumed by 2nd arg */ subsumed_by(*,NIL) <- /. subsumed_by(*1it.*,*clause) <- r e s o l v a b l e ( S , * l i t , * c l a u s e , * r e s o l v e n t ) & SUBSUMED_CLAUSE(*subcl) & subsumed_by(*subcl,*resolvent). subsumed_by(*.*cl,*clause) <- subsumed_by(*cl,*clause). /* Prevent checking subsumption with the c l a u s e i t s e l f i t s e l f ( * c l n u m , * c l n u m . * ) <- /. i t s e l f ( * c l n u m , * . * c l n u m ) <- /. i t s e l f ( * c l n u m , * c l n u m ) . /* P r i n t message i f c l a u s e i s not accepted d u r i n g input of wffs */ tautmsg(*taut) <- STATUS(WFF) & f o r m _ c l a u s e ( * t a u t , * t a u t c l ) & p r i n t l n ( * t a u t c l . ' which i s a t a u t o l o g y '.NIL) & p r i n t ( ' -> not added i n t o database'). tautmsg(*). submsg(*subcl,*clnum) <- STATUS(WFF) & form_clause(*subcl,*subsumed) & printon(*subsumed.' which i s subsumed by p r i n t c l ( * c l n u m ) & p r i n t s ( ' -> not added i n t o database'), submsg(*,*). 92 /****************** THE UNIFICATION MODULE ***************/ /* U n i f i c a t i o n with occurs check */ un i f y ( * c a t e g o r y , * x , * y ) <- incrUNIFY COUNT(*category) & unif i a b l e T*x,*y) & equ(*x,*y) & /. un i f i a b l e ( * x , * y ) <- VAR(*x) & VAR(*y) & /. u n i f i a b l e ( * x , * y ) <- VAR(*x) & / & o c c u r s c h e c k ( * x , * y ) . u n i f i a b l e ( * x , * y ) <- VAR(*y) & / & occurscheck(*y, *x) . uni f i a b l e ( * x , * y ) <- SKEL(*x) & SKEL(*y) & / & CONS(*xlist,*x) & CON S ( * y l i s t , * y ) & e q l i s t ( * x l i s t , * y l i s t ) . uni f i a b l e ( * , * ) . occurscheck(*x,*y) <- SKEL(*y) & / & CO N S ( * . * a r g l i s t , * y ) & -•occursin (*x, * a r g l i s t ) . o c c u r s c h e c k ( * , * ) . e q l i s t ( N I L , N I L ) . e q l i s t ( * h d 1 . * t l 1 , * h d 2 . * t l 2 ) <- u n i f i a b l e ( * h d 1 , * h d 2 ) & e q l i s t ( * t l 1 , * t l 2 ) . o c c u r s i n ( * x , * h d . * ) <- VAR(*hd) & samevar(*x,*hd). o c c u r s i n ( * x , * h d . * ) <- SKEL(*hd) & CONS(*.*arglist,*hd) & o c c u r s i n ( * x , * a r g l i o c c u r s i n ( * x , * . * t l ) <- o c c u r s i n ( * x , * t l ) . 

Cite

Citation Scheme:

        

Citations by CSL (citeproc-js)

Usage Statistics

Share

Embed

Customize your widget with the following options, then copy and paste the code below into the HTML of your page to embed this item in your website.
                        
                            <div id="ubcOpenCollectionsWidgetDisplay">
                            <script id="ubcOpenCollectionsWidget"
                            src="{[{embed.src}]}"
                            data-item="{[{embed.item}]}"
                            data-collection="{[{embed.collection}]}"
                            data-metadata="{[{embed.showMetadata}]}"
                            data-width="{[{embed.width}]}"
                            async >
                            </script>
                            </div>
                        
                    
IIIF logo Our image viewer uses the IIIF 2.0 standard. To load this item in other compatible viewers, use this url:
https://iiif.library.ubc.ca/presentation/dsp.831.1-0051861/manifest

Comment

Related Items