- Library Home /
- Search Collections /
- Open Collections /
- Browse Collections /
- UBC Theses and Dissertations /
- On the completeness of linear strategies in automatic...
Open Collections
UBC Theses and Dissertations
Featured Collection
UBC Theses and Dissertations
On the completeness of linear strategies in automatic consequence finding 1972
pdf
Page Metadata
Item Metadata
Title | On the completeness of linear strategies in automatic consequence finding |
Creator |
Minicozzi, Eliana |
Publisher | University of British Columbia |
Date Created | 2011-04-12T18:45:40Z |
Date Issued | 2011-04-12T18:45:40Z |
Date | 1972 |
Description | The problem of the automatic generation of logical consequences of a set of axioms is examined. The merging subsumption linear strategy has been shown complete with respect to that problem. A generalization of a set of support strategy is given, and the completeness of merging subsumption linear strategy with set of support is proved. The merging-linear-A-ordered strategy and the merging linear-C-ordered strategy have been shown to be incomplete. Relations between unit strategy and input strategy have been examined. A little review of the ‘interesting theorem’ is given. |
Subject |
Automatic Theorem Proving. |
Genre |
Thesis/Dissertation |
Type |
Text |
Language | Eng |
Collection |
Retrospective Theses and Dissertations, 1919-2007 |
Series | UBC Retrospective Theses Digitization Project [http://www.library.ubc.ca/archives/retro_theses/] |
Date Available | 2011-04-12T18:45:40Z |
DOI | 10.14288/1.0051192 |
Degree |
Master of Science - MSc |
Program |
Computer Science |
Affiliation |
Science, Faculty of |
Degree Grantor | University of British Columbia |
Campus |
UBCV |
Scholarly Level | Graduate |
URI | http://hdl.handle.net/2429/33572 |
Aggregated Source Repository | DSpace |
Digital Resource Original Record | https://open.library.ubc.ca/collections/831/items/1.0051192/source |
Download
- Media
- UBC_1972_A6_7 M55.pdf [ 2.92MB ]
- Metadata
- JSON: 1.0051192.json
- JSON-LD: 1.0051192+ld.json
- RDF/XML (Pretty): 1.0051192.xml
- RDF/JSON: 1.0051192+rdf.json
- Turtle: 1.0051192+rdf-turtle.txt
- N-Triples: 1.0051192+rdf-ntriples.txt
- Citation
- 1.0051192.ris
Full Text
ON THE IN COMPLETENESS OF LINEAR STRATEGIES AUTOMATIC CONSEQUENCE FINDING by E L I ANA MINICOZZI A THESIS SUBMITTED I N PARTIAL FULFILMENT OF THE REQUIREMENTS FOR THE DEGREE OF MASTER OF SCIENCE i n the Department o f Computer S c i e n c e We a c c e p t t h i s t h e s i s as conforming t o t h e r e q u i r e d s t a n d a r d THE UNIVERSITY OF BRITISH COLUMBIA A p r i l , 1972 In presenting this thesis in partial fulfilment of the requirements for an advanced degree at the University of British Columbia, I agree that the Library shall make i t freely available for reference and study. I further agree that permission for extensive copying of this thesis for scholarly purposes may be granted by the Head of my Department or by his representatives. It is understood that copying or publication of this thesis for financial gain shall not be allowed without my written permission. Department of Computer Science The University of British Columbia Vancouver 8, Canada Date April 14. 1972 ABSTRACT The problem of the automatic generation of l o g i c a l consequences of a set of axioms i s examined. The merging sub- sumption l i n e a r strategy has been shown complete with respect to that problem. A generalization of a set of support strategy- i s given, and the completeness of merging subsumption l i n e a r strategy with set of support i s proved. The merging-linear-A- ordered strategy and the merging linear-C-ordered strategy have been shown to be incomplete. Relations between unit strategy and input strategy have been examined. A l i t t l e review of the 'interesting theorem 1 i s given. TABLE OF CONTENTS Page INTRODUCTION 1 CHAPTER 1: FORMAL AXIOMATIC THEOREIS AND THE RESOLUTION PRINCIPLE 4 Section 1: Formal axiomatic theory 4 Section22: Set of well formed formulas as set of clauses 9 Section ~5'. Herbrand ' s theorems . .. 13 Section 4: Completeness d e f i n i t i o n . . . . . . 14 Section 5: The Resolution P r i n c i p l e 15 CHAPTER 2: MERGING-SUBSUMPTION-LINEAR RESOLUTION AND SET OF SUPPORT STRATEGY 19 Section 1; Preliminary d e f i n i t i o n s 19 Section 2: The completeness theorems for consequence finding of merging-linear-subsumption strategy 20 Section 3* The extension of the set of support strategy to the consequence finding case 24 CHAPTER 3: SOME DIFFERENCES BETWEEN THEOREM PROVING AND CONSEQUENCE FINDING- 27 Section 1: Unit and Input strategies.... 27 Section 2: Merge-linear-A-ordered Resolution 29 Section 3: Merge-linear-C-ordered Resolution 35 CHAPTER 4: INTERESTING THEOREMS 40 Section 1: Short review on the inte r e s t - ing theorem problem 40 Section 2: Observations and suggestions.. 42 CONCLUSIONS 45 BIBLIOGRAPHY 48 o 0 AC K NOWLEDG-EME NTS I wish to warmly thank a l l the members of the Computer Science Department at the University of B r i t i s h Columbia for t h e i r f r i e n d l y and h e l p f u l attitude towards me. In p a r t i c u l a r , I have enjoyed discussions on a l l possible subjects with Professors Abbe Mowshowitz, Frieder Nake, Raymond Reiter, Richard Rosenberg, Mrs. Vanni Criscuolo and Mrs. Peter Rowat. I have been lead to work i n the area of t h i s thesis by an i n s p i r i n g course given by Professor Raymond Reiter and t h i s thesis derives from a close collaboration with him. To him my hearty acknowledgement for continuous guidance and help, and for h i s patience during endless hours of discussion. My thanks to Miss Cathy Smith, not only for the typing of this thesis, but also for helping me to survive and go through the language ba r r i e r during my f i r s t period i n Vancouver. 1. INTRODUCTION The problem s t u d i e d i n t h i s t h e s i s I s t h e a u t o m a t i c ( i . e . by computer) g e n e r a t i o n o f theorems from a g i v e n s e t o f axioms S. T h i s problem, c a l l e d 'consequence f i n d i n g ' , has been i n t r o d u c e d by R.C.T. Lee i n [ 5]-. : ' • 1 r> L o o s e l y s p e a k i n g , we can say t h a t Lee shows t h a t u s i n g a p a r t i c u l a r r u l e o f 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 £9], i t i s p o s s i b l e to deduce a l l the theorems of S. L a t e r on S l a g l e , Chang and Lee t l 2 " ] have shown t h a t w i t h r e s p e c t t o the consequence f i n d i n g problem, the Semantic R e s o l u t i o n , a n o t h e r r u l e o f i n f e r e n c e , has t h e same p r o p e r t y o f the R e s o l u t i o n P r i n c i p l e . I n b o t h of the works t h a t we have mentioned ( p a r t i c u l a r l y i n the f i r s t ) t h e a u t h o r s a l s o t r y t o f o r m a l i z e what i s meant by an ' i n t e r e s t i n g theorem'. Moreover, they t r y , l e s s s u c c e s s f u l l y , t o f i n d m e c h a n i c a l p r o c e d u r e s f o r s e l e c t i n g the ' i n t e r e s t i n g ' theorems from t h e ' u n i n t e r e s t i n g ' o n e s . Our i n t e r e s t i n t h i s problem i s based m a i n l y on two r e a s o n s . One i s t h a t i t c a n l e a d , as was the case f o r theorem p r o v i n g , t o a deeper u n d e r s t a n d i n g o f the laws o f the d e d u c t i o n i n m a t h e m a t i c a l l o g i c ; f o r example one can f i n d r u l e s o f i n f e r e n c e s i m p l e r but e q u i v a l e n t t o the ones t r a d i t i o n a l l y u sed. The second r e a s o n i s t h a t t o study a u t o m a t i c consequences f i n d i n g c a n h e l p the development o f A r t i f i c i a l I n t e l l i g e n c e t o p i c s , not n e c e s s a r i l y r e l a t e d t o mathematics. I n any c a s e , we b e l i e v e t h a t t h i s p roblem must be seen as a t o p i c b e l o n g i n g t o the f i e l d o f A r t i f i c i a l I n t e l l i g e n c e . 2. Of c o u r s e , g i v e n the t i g h t r e l a t i o n s h i p between our t o p i c and theorem p r o v i n g , a much more deve l o p e d s u b j e c t , the q u e s t i o n a r i s e s as t o how w o r t h w h i l e i t i s to d e v e l o p i t as an independent s u b j e c t o f r e s e a r c h . I n o r d e r t o answer t h i s q u e s t i o n we w i s h here t o s t r e s s the f o l l o w i n g two p o i n t s : 1) Theorem p r o v i n g i s a c t u a l l y d e v e l o p i n g as a study o f a p a r t i c u l a r type o f p r o o f , the p r o o f o f a c o n t r a d i c t i o n . Of c o u r s e , one can prove t h a t a p r o p o s i t i o n T i s a theorem o f a g i v e n s e t of axioms not o n l y by c o n t r a d i c t i o n , ( i , e . showing t h a t from S and the n e g a t i o n o f T one c a n deduce a c o n t r a d i c t i o n ) , but a l s o by the d e d u c t i o n o f T i t s e l f from S. - Then the r e s e a r c h on consequences f i n d i n g can be seen as the study on a k i n d o f p r o o f d i f f e r e n t from the one by c o n t r a d i c t i o n . I n t h i s r e g a r d we can t h i n k the r e l a t i o n s h i p between theorem p r o v i n g and consequence f i n d i n g as the one between problem o f g e n e r a t i o n and problem o f r e c o g n i t i o n : 2) Consequence f i n d i n g d i f f e r s from theorem p r o v i n g i n the f a c t t h a t i t does not need p r e v i o u s knowledge o f the theorems. So a consequence f i n d i n g program c a n l e a d the computer to f i n d new theorems, an a c t i v i t y t h a t s h o u l d be c o n s i d e r e d as i n t e l l i g e n t as the one o f p r o v i n g theorems. The a pproach we f o l l o w i s e s s e n t i a l l y the same as the one o f Lee, Chang and S l a g l e who have s t u d i e d the a p p l i c a b i l i t y t o consequence f i n d i n g o f some s t r a t e g i e s f i r s t i n t r o d u c e d i n theorem p r o v i n g . We have t a k e n i n t o c o n s i d e r a t i o n s t r a t e g i e s d i f f e r e n t from t h o s e and our t e c h n i q u e f o r p r o v i n g theorems i s a l s o d i f f e r e n t from the one used by them. The main r e s u l t s we have found i n t h i s t h e s i s are the f o l l o w i n g : The merging l i n e a r subsumption s t r a t e g y i s complete f o r consequence f i n d i n g ; i t i s p o s s i b l e t o g e n e r a l i z e the s e t o f s u p p o r t s t r a t e g y t o consequence f i n d i n g and the merging l i n e a r subsumption s t r a t e g y w i t h s e t o f support i s complete f o r i t ; the merging A - o r d e r e d l i n e a r s t r a t e g y and the merging G-ordered l i n e a r s t r a t e g y a r e not complete f o r consequence f i n d i n g . We have a l s o found under w h i c h h y p o t h e s i s on the s e t o f axioms S i t i s p o s s i b l e t o use the i i i e r g i n g A - o r d e r e d l i n e a r and the merging C-ordered l i n e a r s t r a t e g i e s f o r d e d u c i n g theorems from S, and we have shown t h a t f o r consequence f i n d i n g the u n i t s t r a t e g y i s not e q u i v a l e n t t o the i n p u t s t r a t e g y . We do not t h i n k t h a t the approach we have ;chosen i s the o n l y p o s s i b l e one, but we b e l i e v e t h a t i t can h e l p i n b e t t e r u n d e r s t a n d i n g b o t h the p e c u l i a r i t y o f theorem p r o v i n g i t s e l f and the d i f f e r e n c e between theorem p r o v i n g and consequence f i n d i n g , as t h e y have been h i s t o r i c a l l y d e v e l o p i n g . 4. CHAPTER 1: FORMAL AXIOMATIC THEORIES AND THE- RESOLUTION PRINCIPLE. In t h i s chapter a rather rigorous description of what a formal axiomatic theory i s w i l l be given; i t w i l l be, also, c l a r i f i e d under which l i m i t s we w i l l speak about axioms' and theorems; a p a r t i c u l a r rule of inference, that i s the resolution p r i n c i p l e , w i l l be introduced. " / Section 1: Formal Axiomatic Theories. D e f i n i t i o n [7"}. A formal axiomatic theory K i s defined when the following conditions are s a t i s f i e d : 1) A countable set of symbols i s given as symbols of K. A f i n i t e sequence of symbols of K i s called an expression of K. 2) There i s a subset of the expressions of K call e d the set of well formed formulas (wffs) of K (we w i l l assume that there exists an eff e c t i v e procedure to determine whether a given expression i s a wff). 3) A set of wffs i s set aside and cal l e d the set of axioms of K. There exists an eff e c t i v e procedure to determine i f a wff i s an axiom or not. 4) There i s a f i n i t e set I-^.,.ln of rel a t i o n s among wffs, called rules of inference. For each 'Ij_ there i s auunique positive integer J such that, for every set of J wffs and each wff A, one can e f f e c t i v e l y decide whether the given J wffs are i n the r e l a t i o n 1^ to A, and i f so, A i s called a di r e c t consequence of the given wffs by virtue of I j _ . 5. (LI) D e f i n i t i o n £7]: A wff A i s said to "be a consequence i n K of a set S of w f f s , i f and only i f there i s a sequence A]_A2...An of wffs such that A^A and for e§,ch i , either Aj_ i s an axiom or Â_ i s i n S, or Aj_ i s a direct consequence by some rule of inference of some of the preceding wffs i n the sequence. Such a sequence i s called a proof (or deduction) of A from S. The members of S are ca l l e d the hypothesis or premises of the proof. I f S i s just the set of the axioms of K, then the consequences i n K of S are c a l l e d theorems. Before giving an equivalent d e f i n i t i o n of 'wff i s a consequence i n K of a set S of wffs' l e t us give some other s p e c i f i c a t i o n of our theory 'K: 1) The set of symbols of K w i l l be a subset of the following set of symbols: a) Punctuation symbols: .,; ( ; ) ; ,. b) Logical symbols: V; & ; - ; V ; 3 ; c) Individual variables: x; y; z; X]_; y u z i ; etc. d) Individual constants: a; b; c; a-p b-j_; c^; etc. e) Predicate l e t t e r s : PT Q; R; S; T; P x ; Q x; Rx; Tx; etc. Where any symbol represents an n-ary predicate l e t t e r with n X. 0. 6. f ) F u n c t i o n l e t t e r s : f; g; h; f x ; g x ; h-p e t c . Where any symbol r e p r e s e n t s an n-ary f u n c t i o n l e t t e r w i t h n 2 0. 2 ) Set of terms: a) V a r i a b l e s and i n d i v i d u a l c o n s t a n t s a r e terms. c) An e x p r e s s i o n i s a term o n l y i f i t can be shown t o be a term on the b a s i s o f a) and b ) . 3) Set of atomic f o r m u l a s : I f n^,...n , a r e terms and L i s an n-ary p r e d i c a t e t h e n L(n]_,...n n) i s an atomic f o r m u l a . 4) Set o f w f f s : a) Every atomic f o r m u l a i s a w f f . b) I f A and B are w f f s , and. w i s a v a r i a b l e t h e n : A; A & B; A v B; \/w(A); 3w(A) are w f f s . c) An e x p r e s s i o n i s a w f f o n l y i f i t can be shown to be a w f f on the b a s i s o f a) and b) . D e f i n i t i o n s C73: I ) An e x p r e s s i o n i s s a i d t o be q u a n t i f i e r b) I f Z i s an n-ary f u n c t i o n l e t t e r and n]_...n- are terms, t h e n £ ( n ^ .. .n n) i s a term. n f r e e i f the symbolsV , 3 do not appear i n i t . 2) I n V w ( o r 3 w)(A) A i s c a l l e d the scope of the u n i v e r s a l ( o r e x i s t e n t i a l ) q u a n t i f i e r . 3) An o c c u r r e n c e o f a v a r i a b l e w i s bound I n a w f f , i f e i t h e r i t i s the v a r i a b l e of a u n i v e r s a l q u a n t i f i e r o r i t i s 7. the v a r i a b l e o f an e x i s t e n t i a l q u a n t i f i e r i n the w f f , o r i t i s w i t h i n the scope o f e i t h e r 'Vw' o r Sw' i n the f o r m u l a . Otherwise the o c c u r r e n c e i s s a i d t o be f r e e i n t h e w f f . 4) A v a r i a b l e i s s a i d t o be f r e e (bound) i n a w f f i f i t has a f r e e (bound) o c c u r r e n c e i n the w f f . D e f i n i t i o n \,7~}i An i n t e r p r e t a t i o n c o n s i s t s o f a not-empty s e t D, c a l l e d the domain o f the i n t e r - p r e t a t i o n , and an assignment t o each n-ary f u n c t i o n l e t t e r % o f an n-place o p e r a t i o n i n D ( i . e . a f u n c t i o n from D n i n t o D), t o each n-ary p r e d i c a t e l e t t e r L of an n-place r e l a t i o n i n D, whose v a l u e s a r e 'True' or ' F a l s e ' ( t h a t i s a f u n c t i o n D n-^ (True, F a l s e ) ) . G i v e n such an i n t e r p r e t a t i o n v a r i a b l e s a r e thought of as r a n g i n g over the set D, each c o n s t a n t i s thought o f as a s i n g l e p o i n t i n D, 'V', ' &' 'V ' 3 ' are g i v e n t h e i r u s u a l meaning. For a g i v e n i n t e r p r e t a t i o n , a w f f w i t h o u t f r e e v a r i a b l e s •(sclosed w f f ) r e p r e s e n t s a p r o p o s i t i o n which i s t r u e o r f a l s e , whereas a w f f w i t h f r e e v a r i a b l e s s t a n d s f o r a r e l a t i o n on the domain of the i n t e r p r e t a t i o n which may be s a t i s f i e d ( t r u e ) f o r some v a l u e s i n the domain o f t h e f r e e v a r i a b l e and f o r t h e v a l u e s o f the c o n s t a n t s , and not s a t i s f i e d ( f a l s e ) f o r o t h e r r v a l u e s of the f r e e v a r i a b l e s and f o r the v a l u e s o f the c o n s t a n t s v ' ^we w i l l not go i n t o any d e f i n i t i o n o f t r u t h and s a t i s f i a b i l i t y more f o r m a l t h a n t h e one we have g i v e n b e f o r e . 8. D e f i n i t i o n s : 1) A w f f i s c a l l e d ' s a t i s f i a b l e ' i f t h e r e i s some i n t e r p r e t a t i o n i n wh i c h i t i s s a t i s f i e d . 2) A s e t of w f f s i s s a t i s f l a b l e i f t h e r e i s an i n t e r p r e t a t i o n i n which a l l the w f f s i n the s e t a r e s a t i s f i e d . 3) A w f f i s c a l l e d ' u n s a t i s f i a b l e ' i f i t i s not s a t i s f i a b l e . 4) A set of w f f s i s ' u n s a t i s f i a b l e ' I f every w f f i n the s e t i s not s a t i s f i a b l e . (L2) D e f i n i t i o n 7 : A w f f A i s s a i d t o be l o g i c a l consequence i n K o f a s e t S of w f f s i f the s e t S' = SUA i s u n s a t i s f i a b l e . We w i l l say S i m p l i e s A f o r 'A i s a l o g i c a l consequence o f S'. D e f i n i t i o n % : A w f f A i s s a i d t o be l o g i c a l l y v a l i d i f and o n l y i f A i s t r u e f o r eve r y i n t e r p r e t a t i o n . D e f i n i t i o n 7 : A t h e o r y K i s s a i d t o be a f i r s t o r d e r l o g i c t h e o r y i f : 1) The axioms o f K are d i v i d e d i n t o two c l a s s e s : the l o g i c a l axioms and the p r o p e r axioms. 2) The r u l e s of i n f e r e n c e a r e : (2) •'Modus ponens and g e n e r a l i z a t i o n * - . t o r the d e f i n i t i o n o f t h e s e i n f e r e n c e r u l e s , see the r e f e r e n c e g i v e n i n Chapter 2. 9. The l o g i c a l axioms a r e the same f o r every f i r s t o r d e r l o g i c t h e o r y and t h e y a r e l o g i c a l l y v a l i d w f f s . The prop e r axioms v a r y from t h e o r y t o t h e o r y . A f i r s t o r d e r l o g i c t h e o r y i n which t h e r e a r e not p r o p e r axioms i s c a l l e d , a 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 . The l o g i c a l axioms are so d e s i g n e d t h a t the l o g i c a l consequences of the c l o s u r e o f the axioms o f K a r e p r e c i s e l y the theorems o f K. The t h e o r i e s we w i l l c o n s i d e r w i l l be f i r s t o r d e r l o g i c t h e o r i e s . S e c t i o n 2: Set o f w f f s as s e t o f c l a u s e s . D e f i n i t i o n : A l i t e r a l i s an atomic f o r m u l a o r i t s n e g a t i o n . D e f i n i t i o n : A c l a u s e i s a s e t o f l i t e r a l s . We w i l l i n d i c a t e them w i t h the f o l l o w i n g symbols: C; T; C T C t i T e t c . C 0; T 0; G1; T x; e t c . R Q; R]_; e t c . R 0; R].; e t c . D e f i n i t i o n [ 7 ^ : A w f f B such t h a t B % w i • • • ( A) Where: i s e i t h e r the u n i v e r s a l q u a n t i f i e r or the e x i s t e n t i a l q u a n t i f i e r , w^ i s a v a r i a b l e and Wj_ wj f o r i ̂ J , A i s a q u a n t i f i e r f r e e w f f i s s a i d t o be i n prenex normal form; A i s c a l l e d the m a t r i x and the sequence Q-̂ ŵ • • • i s c a l l e d the p r e f i x . can be a l s o a q u a n t i f i e r f r e e w f f . 10. D e f i n i t i o n : A w f f i s s a i d t o be i n prenex c o n j u n c t i v e form i f I t i s i n prenex normal form and i t s m a t r i x i s a c o n j u n c t i o n o f w f f s . D e f i n i t i o n : A w f f A i s s a i d t o be e q u i v a l e n t t o a w f f B i f B i s a consequence o f A and A i s a consequence o f B. Th. [7] : There i s an e f f e c t i v e p r o c e d u r e f o r t r a n s f o r m i n g any w f f A i n t o a w f f B i n prenex normal form such t h a t H A=B^ ̂ . G i v e n a c l o s e d w f f A i n prenex normal form: A=^W]_...QgW^CCC) we w i l l say t h a t : D e f i n i t i o n : B i s the f u n c t i o n a l normal form o f A i f B i s o b t a i n e d from A u s i n g the f o l l o w i n g p r o c e d u r e : 0) I f A i s a q u a n t i f i e r f r e e w f f , B i s j u s t A. 1) S t a r t i n g from the l e f t o f A l e t be the f i r s t e x i s t e n t i a l q u a n t i f i e r we meet, and l e t Wr be the v a r i a b l e w h i c h i s q u a n t i f i e d by Qj,, c o n s t r u c t B r % W x . . . Qr_ 1 % + 1W r + 1. . . Q KW K( 0 • ) where C i s C except t h a t any o c c u r r e n c e of Wr i n G i s s u b s t i t u t e d e i t h e r w i t h • »Wr_i)» where J& i s a f u n c t i o n a l symbol w h i c h does not oc c u r i n our t h e o r y K, i f r > 1, or w i t h a c o n s t a n t symbol, which does not oc c u r i n our t h e o r y K, i f r = l ; )-A=B means t h a t 'A e q u i v a l e n t t o B 1 i s a theorem o f the 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 . 11. 2) I f e i t h e r t h e r e i s not such Qp, o r n K , t h e n s t o p : B i s a f u n c t i o n a l normal form o f the s t a r t i n g w f f A, o t h e r w i s e c a l l B, A and C 1, G and go t o s t e p 1. Because t h i s p r o c e d u r e s u b s t i t u t e s f o r a v a r i a b l e bound by an e x i s t e n t i a l q u a n t i f i e r a p a r t i c u l a r term, i n t u i t i v e l y i t i s c l e a r t h a t the prensec normal form o f a w f f i s a consequence o f i t s f u n c t i o n a l normal form, but t h e o p p o s i t e i s not t r u e ; l e t us g i v e an example: A = VxVy3zC(x,y,z) B - VxVyC(x,y,£(x,y), C l e a r l y , whenever B i s s a t i s f i e d a l s o A i s s a t i s f i e d . Now we are ready to p e r f o r m the f o l l o w i n g t r a n s f o r m a t i o n o f our t h e o r y K: 1) We c o n s i d e r the c l o s u r e o f the w f f s o f our t h e o r y K, 2) Eve r y w f f so o b t a i n e d i s t r a n s f o r m e d i n t o i t s prenex c o n j u n c t i v e i l o r m a l form. 3) E v e r y w f f so o b t a i n e d I s t r a n s f o r m e d i n i t s f u n c t i o n a l normal form. 4) E v e r y w f f so o b t a i n e d i s t r a n s f o r m e d i n t o a c o r r e s p o n d i n g s e t o f c l a u s e s . L e t us g i v e an example o f the a l g o r i t h m j u s t g i v e n : Example: C o n s i d e r a w f f A _ V x 3 y ( ( p ( x , y ) V q ( x , c ) ) & ( p ( X , b ) V q ( x , y ) ) By s t e p s 1 and 2 A i s t r a n s f o r m e d I n t o A, by s t e p 3 A i s t r a n s f o r m e d i n t o B such t h a t B - ( p ( x , f ( x ) ) V q ( x , c ) ) < 5 c ( p ( x , b ) V q ( x , f ( x ) ) where f i s a new f u n c t i o n a l symbol. By st e p 4 B i s t r a n s f o r m e d i n t o a s e t o f c l a u s e s S = ( p ( x , f ( x ) ) q ( x , c ) , p ( x , b ) q ( x , f ( x ) ) ) (Note t h a t from the f a c t t h a t our w f f s a r e c l o s e d f o r m u l a s ( 5) and from the l o g i c a l soundness o f the r u l e s o f i n f e r e n c e we w i l l use, i t f o l l o w s e a s i l y t h a t t h e d e f i n i t i o n s ( L I ) and (L2) are e q u i v a l e n t , t h a t i s a w f f A i s a l o g i c a l consequence o f a s e t o f w f f s i f and o n l y i f A i s a consequence i n K o f S. I t seems n a t u r a l t o us t o l o o k a t d e f i n i t i o n s ( L I ) and (L2) as c h a r a c t e r i s t i c r e s p e c t i v e l y o f t h e consequence f i n d i n g approach and the theorem p r o v i n g a p p r o a c h ) . From now on we w i l l r e g a r d t h e axioms of our t h e o r y as a set o f c l a u s e s ^ ^ and our theorem as a c l a u s e * ^ . L o g i c a l soundness i s an elementary p r o p e r t y t h a t every s e t o f r u l e s o f i n f e r e n c e must s a t i s f y . A s e t o f r u l e s o f i n f e r e n c e i s l o g i c a l l y sound i f , when i t i s a p p l i e d t o some s a t i s f i a b l e s e t o f w f f s , the r e s u l t i n g s e t o f w f f s i s s t i l l s a t i s f i a b l e . (6) For an i n t u i t i v e u n d e r s t a n d i n g o f some n o t i o n we w i l l i n t r o d u c e l a t e r 9 i;t i s enough t o remember t h a t each c l a u s e r e p r e s e n t s the d i s j u n c t i o n o f i t s l i t e r a l s , and a s e t o f c l a u s e s r e p r e s e n t s the c o n j u n c t i o n o f i t s c l a u s e . (7) A c t u a l l y , s i n c e the r u l e s o f i n f e r e n c e we are g o i n g t o use are such t h a t t h e y t r a n s f o r m a c o u p l e o f c l a u s e s i n t o a s i n g l e c l a u s e , a c l a u s e w i l l be t r e a t e d as an axiom. 13. S e c t i o n 3: Herbrand 1 s theorems. D e f i n i t i o n s [9J J l ) A l i t e r a l which does not c o n t a i n v a r i a b l e s i s c a l l e d a ground l i t e r a l . 2) A c l a u s e each member o f w h i c h i s ground i s c a l l e d a ground c l a u s e . A p a r t i c u l a r ground c l a u s e i s the empty c l a u s e . By g e n e r a l c l a u s e o r s i m p l y c l a u s e we w i l l mean any c l a u s e (not n e c e s s a r i l y g r o u n d ) . (8) D e f i n i t i o n : : W i t h any s e t S o f c l a u s e s c a n be a s s o c i a t e d a s e t o f ground terms c a l l e d t h e Herbrand U n i v e r s e o f S: b n=0 n » 3 Where: H„ „z the s e t o f a l l c o n s t a n t symbols b e l o n g i n g t o S i f t h e r e a r e any, o t h e r w i s e a g e n e r i c c o n s t a n t symbol, H n > s - H n_]_ } S U / s e t o f a l l terms o b t a i n e d from a l l the f u n c t i o n a l symbols o f S i n whic h the v a r i a b l e s a r e s u b s t i t u t e d by terms o f H ^. D e f i n i t i o n s l9j : 1) I f S i s any s e t o f c l a u s e s and P i s any set o f terms t h e n by P(Sdi we denote the s a t u r a t i o n o f S over P, t h a t i s the s e t o f a l l ground c l a u s e s o b t a i n a b l e from members o f S by r e p l a c i n g v a r i a b l e w i t h member o f P, o c c u r r e n c e s o f t h e same v a r i a b l e i n any one o f c l a u s e b e i n g D e f i n i t i o n o f the Herbrand U n i v e r s e e q u i v a l e n t t o t h i s one can be found, f o r example, 1 n ' f 9 D . 14. replaced by occurrences of the same term. 2) A set of ground l i t e r a l s which does not contain a l i t e r a l and Its negation i s cal l e d a model. 3) A clause C belonging to a set S of clauses i s s a t i s f i e d by a model M i f for every member C of H S(G), C' f\ M i s not empty. A set S of clauses i s s a t i s f i e d by a model M i f every clause i n S i s s a t i s f i e d by M. Such M i s said to be a model for S. F i r s t Herbrand's t h e o r e m i f S i s any f i n i t e set of clauses, then S Is unsatisfiable i f and only i f there i s . a f i n i t e subset of Hg(S) which i s uns a t i s f i a b l e . G-eneralized Herbrand 1 s theorem C-12"] : I f S i s any f i n i t e set of clauses and C i s a ground clause then S Implieŝ '*®*1 C i f and only i f there i s a f i n i t e subset S' of % U C ( S ) such that S' implies C. Section 4: Completeness. Let S be any f i n i t e set of clauses, l e t T be a set of rules of inference, l e t C be a clause. Def i n i t i o n s : 1) :<£ i s r e f u t a t i o n complete i f : (11) S i s u n s a t i s f i a b l e v ' ' i f and'only i f there i s a deduction of the empty clause from S by 3 1 -^Formulation 0 f ̂ he Herbrand theorem equivalent to t h i s one can be found i n C4l, £90, C101. ^ S implies C i s equivalent to 'G i s a l o g i c a l sequence of S'. ^ ̂ O b v i o u s l y S i s unsatisf iable i f there i s no model for i t . 1 5 . 2) i i s complete f o r consequence f i n d i n g i f : S i m p l i e s C i f and o n l y i f t h e r e i s a d e d u c t i o n o f a c l a u s e C' from S by l a n d C i m p l i e s C. S e c t i o n 5 1 R e s o l u t i o n p r i n c i p l e . D e f i n i t i o n s [ 9 3 : 1) Any e x p r e s s i o n o f the form n/w where w i s any v a r i a b l e and n i s any term d i f f e r e n t from w i s c a l l e d s u b s t i t u t i o n component. 2) Any f i n i t e s et o f s u b s t i t u t i o n components ( p o s s i b l y empty), none o f the v a r i a b l e s o f w h i c h are the same, i s c a l l e d a s u b s t i t u t i o n . We w r i t e the s u b s t i t u t i o n whose components are n]_/w^, ..-n^/w^ as (n-^/w-^,... n^/w^")with the u n d e r s t a n d i n g t h a t the o r d e r o f components i s i m m a t e r i a l . We use lower case Greek l e t t e r s t o denote s u b s t i t u t i o n . I n p a r t i c u l a r € i s the empty s u b s t i t u t i o n . 3;).; I f 0 -z (n^/w-L,... n k/w k) and A. are two s u b s t i t u t i o n s , t h e n 0o V \ % where X,' i s the s e t o f a l l components of X whose v a r i a b l e s a r e among w-̂ ...ŵ and-©' i s the s e t of a l l components n^ X/w^ such t h a t A. i s d i f f e r e n t from w^ i s c a l l e d the c o m p o s i t i o n o f 9 by A. and i s denoted by 0/t . 4) I f E i s any string of symbols and 0 i (n 1/w 1 > .. .nk/wk) i s any substitution, then the i n s t a n t i a t i o n of E by 0 i s the operation of replacing each occurrence of ŵ i n E by an occurrence of the term n^, E0 Is c a l l e d the instance of E by ©. (As a r e s u l t i n [ 7 l we want to remember that E(erA.)s, (B«r) A, . 5) I f C i s any set of strings and © i s a substitution then the instance of G by 0 i s the set of a l l strings E© where E i s i n G. We denote this set by G0 and we say that i t i s an instance of C. D e f i n i t i o n : Given a st r i n g of symbols E (or a set of strings C), the substitution g* i s a most general substitution for E (or for C) i f for any substitution © there i s a substitution A, such that E0srE(frJt) (or G0 * C ( r J l ) ) , that i s for any 0, E0(or G0) i s an instance of E<5~ (or O f f ) , Definitions 9 *• 1) Given two clauses G and 0' such that there are two l i t e r a l s m and. m1, m belonging to C, m' belonging to C' — • (12) and mQ= m'cT where 0 andtf" are the most general substitutions with For avoiding confusion, given a set S of clauses, we rename variables so that a l l variables i n one clause are d i s t i n c t from a l l the variables i n the other clause. (Standardization process C93 )• 17. r e s p e c t t o making m and m' the complement o f each o t h e r , t h e c l a u s e R± = (C-m)etXC'-m1 )<r i s c a l l e d a r e s o l v e n t of G and Co. C l e a r l y two c l a u s e s can have o n l y a f i n i t e number o f r e s o l v e n t s . 2) I f S i s any set o f c l a u s e s the s e t o f a l l c l a u s e s which a re members of S or r e s o l v e n t s o f members o f S i s denoted by R ( S ) ; R ( R n _ 1 ( S ) ) w i t h R°(S)=S and n>l i s c a l l e d t h e n-t h r e s o l u t i o n o f S. Le t us g i v e an example o f the l a s t d e f i n i t i o n s : Ex: L e t S be ( p r q , pq, q r ) R^(S) r R(S) w i l l be r q , p r r , pqq, pr)\@f> D e f i n i t i o n [93 : The R e s o l u t i o n P r i n c i p l e i s the f o l l o w i n g r u l e o f i n f e r e n c e : From any p a i r o f c l a u s e s G and C', one may i n f e r a r e s o l v e n t o f C and C . C and. C 1 are c a l l e d p a r e n t c l a u s e s o f t h e i r r e s o l v e n t . I t i s c l e a r from the d e f i n i t i o n t h a t any model f o r the pa r e n t c l a u s e s o f a r e s o l u t i o n s a t i s f i e s the r e s o l v e n t , t h a t i s the r e s o l v e n t i s a l o g i c a l consequence o f i t s p a r e n t s . I n t u i t i v e l y we can say t h a t the r e s o l u t i o n p r i n c i p l e i n v o l v e s , as i d e a s , the s y l l o g i s m p r i n c i p l e o f the p r o p o s i t i o n a l c a l c u l u s , t h a t i s from p v q and p v r we o b t a i n q v r , and the 18 i n s t a n t i a t i o n o f p r e d i c a t e c a l c u l u s , t h a t i s from Vw-^...Vwn A(w^,...w ) we o b t a i n A( n-|_, .. .n n) where w-p...wn are v a r i a b l e s , A i s a w f f , ' n , . . . n a r e terms. 1 n R e s u l t s : : F o r the r e s o l u t i o n p r i n c i p l e b o t h r e f u t a t i o n c ompleteness and completeness f o r consequence f i n d i n g have been proved [ 9 , 5 7 . 1 9 . CHAPTER 2:. MERGING SUBSUMPTION LINEAR RESOLUTION AND SET OF SUPPORT STRATEGY. In t h i s chapter we w i l l prove the completeness for consequences finding of the merging li n e a r subsumption strategy. A generalization to consequence finding of the set of support strategy w i l l be given and i t s completeness w i l l be proved. Section 1: Preliminary d e f i n i t i o n s . Deduction as a tree: We w i l l represent a deduction of a clause from a set of clauses as a tree performing the following elementary correspondence: i f a clause R̂ i s inferred from Cj and C k by I m then the tree shown i n Figure 1 w i l l represent t h i s deduction. When there i s no p o s s i b i l i t y of confusion about the rule of inference used the tree of Figure 1 w i l l be substituted by the tree Figure l a . Let", us ".give ah example of a not elementary deduction: Let S be (prq, pqJt, & ). The clause pr can be deduced from S by resolution, one of these deductions can be:- From prq and pq£ by r e s o l u t i o n pr£, From p r % and % by r e s o l u t i o n pr, the deduction tree corresponding to t h i s deduction of pr w i l l be the tree of. T&lgure Ibv.;. D e f i n i t i o n : I f G and C' are two clauses we say that C subsumes C ' l f there i s a s u b s t i t u t i o n ^ such that C f f i s a subset of C'^1^] ___ Note that i f G subsumes C' then C implies C', the converse i s not true. 20. D e f i n i t i o n 2 : A ground cl a u s e C'' i s c a l l e d a merge r e s o l v e n t of two ground c l a u s e s C and C i f C " i s a r e s o l v e n t of C and C and there i s some l i t e r a l K such t h a t K i s an element o f C, C and C' 1. K i s c a l l e d a merge l i t e r a l . D e f i n i t i o n : A clause T i s a prime i m p l i c a t e of a set of c l a u s e s S , i f S i m p l i e s T and every T' such t h a t T^T' and S i m p l i e s T f , does not subsume T. D e f i n i t i o n : A set of c l a u s e s S i s a minimum deduction set f a r a clause T i f S i m p l i e s T and S-CT, where C i s any element .of S, does not imply T. I f S i s a minimum d e d u c t i o n set f o r T we w i l l say a l s o that S minimally i m p l i e s T. c t l o n 2: Completeness theorems f o r consequence f i n d i n g f o r the merging-linear-subsumption s t r a t e g y . D e f i n i t i o n : A merging-subsumptlon-llnear d e d u c t i o n (m-s-1) C2,6,l"3 of a c l a u s e i s a d eduction r e p r e s e n t e d by the t r e e i n Figure 2 where: 1) C ^ i s o i n S;' - ~. ..^ 2) R^ . f o r ^ - l ^ i i r i i i s t a ] r e s o l v e n t t o f the two c l a u s e s immediately above i t . 3) C£ f o r 04i£n-l i s e i t h e r i n S or i s one Rj f o r some j < i . 4) I f C 1 i s not i n S then: a) subsumes some i n s t a n c e of R ± b) i s a merge r e s o l v e n t c) The l i t e r a l r e s o l v e d upon i n C^ i s a merge l i t e r a l of C i 21. 5) No clause i n the deduction i s a tautology. Result: The ref u t a t i o n completeness of the m.s.l. strategy with top clause^ ^any clause i n a minimally unsatisfiable set of clauses has been proved [!"}. Lemma 1: Let S be a f i n i t e set of ground clauses, l e t K be a set of l i t e r a l s , l e t S' be the set (C'/C C S & C-C-K) ( 1 7 ) l e t T be a clause then: i f S Implies T, S' implies T. Proof: Every model for S' i s a model for S. Then because S implies T, S' implies T. Corollary 1: Let S be a f i n i t e set of ground clauses l e t K be a set of l i t e r a l s , l e t S' be the set (C/C S & C'rC-K) then i f S i s un s a t i s f i a b l e , S* i s uns a t i s f i a b l e . Proof: Di r e c t l y from Lemma 1 when T i s the empty clause. Th. 1: Let S be a f i n i t e set of ground clauses, l e t T be a clause, l e t C be a clause i n S then: i f S minimally implies T ^ t h e n there i s a m.s.l. deduction with top clause C of a clause T' such that T' subsumes T. Proof: Since S implies T, the set S-^SUT i s unsati sf i a b l e . Consider S| z(C'/CeS 4 & C'=C-T) from corollary 1 S^ i s u n s a t i s f i a b l e . An m.s.l. deduction with top clause C i s a m.s.l. deduction i n which the l e f t top clause i s C. Note that i f some C i n S i s just K the empty clause w i l l be i n S' The hypothesis that S minimally Implies T can be substituted by the hypothesis S implies T If"the deduction of T i n which we are interested i s just a m^s.l. deduction of T from b. (17) (18) C o n s i d e r Sg a subset o f Sj[ such t h a t S g i s m i n i m a l l y u n s a t i s f i a b l e . From the r e f u t a t i o n completeness o f the m.s . l . s t r a t e g y w i t h top c l a u s e any c l a u s e i n a m i n i m a l l y u n s a t i s f i a b l e se t o f c l a u s e s , f o r any c l a u s e C i n 3^ t h e r e i s a m . s . l . d e d u c t i o n o f the empty c l a u s e from w i t h top c l a u s e C . I n p a r t i c u l a r , because S. m i n i m a l l y i m p l i e s T, t h e r e s w i l l be a m . s . l . d e d u c t i o n o f the empty c l a u s e , from 5^ w i t h top c l a u s e C'~C-T where C i s the g i v e n c l a u s e o f S. L e t D ( F i g . 3 ) be such a d e d u c t i o n . S t a r t i n g from thJe^ t o p of D, a p p l y the f o l l o w i n g a l g o r i t h m : . ' A l g o r i t h m ' R e c o n s t r u c t i o n ' . (19) 1) S u b s t i t u t e f o r C the c o r r e s p o n d i n g c l a u s e i n S^ 2) For 0<i<n-l i f C| i s i n S^ s u b s t i t u t e f o r i t the c o r r e s p o n d i n g c l a u s e i n S^. 3) S u b s t i t u t e f o r each r e s o l v e n t a p p e a r i n g i n D as R^ or C^ , t h e r e s o l v e n t o b t a i n e d under the p r e v i o u s s u b s t i t u t i o n . L e t the d e d u c t i o n D' i n F i g . 4 be such d e d u c t i o n . Observe now t h a t no £ such t h a t t i s i n T, appears i n D' because o t h e r w i s e t would be i n some c l a u s e s of D and t h e n i n the empty c l a u s e ; t h i s means t h a t : the n o - t a u t o l o g i e s c o n d i t i o n h o l d s f o r D' because i t h o l d s f o r D and D' i s a d e d u c t i o n from S more t h a n from S-̂ . (250)" T r i v i a l l y the l a s t r e s o l v e n t o f D'T1 subsumes T " . T r i v i a l l y the merging and. subsumption c o n d i t i o n s h o l d f o r D* . . Th„.2: L e t S be a s e t o f g e n e r a l c l a u s e s , l e t T be a g e n e r a l c l a u s e t h e n : i f S m i n i m a l l y i m p l i e s T(x-]_, ...x n) t h e n f o r every T h i s means to add T'' t o C'-C-T i f T'' i s a subset o f T and o f C. (20) Remember t h a t the empty c l a u s e subsumes ev e r y c l a u s e . 23. clause i n S, there i s a m-y-s.l. deduction from S with top clause C of a clause T' such that T' subsumes T. Proof: Let us write T as T(X]_, .. ,.xn) to emphasise the variables of T. 1) Let us introduce the individual symbols b^,...b such that for 1< L i n b^ does not appear i n S or i n T . 2) Consider T(bi,...b n), since S implies T(xi,...x n) represents a closed w f f , T(x-L,...xn) implies "<• T(b 1,...b n) and S implies T(b 1,...b n). 3) Let us construct the Herbrand universe of S and T(b 1,...b n), that i s HS0T. 4) From the generalised Herbrand theorem there i s a f i n i t e subset S' of H S U T(S) such that S1 implies T(b 1,...b n). 5) Consider the subset S " o f S 1 such that S " minimally implies T(b-j_, .. .bn) . 6) From Th.l, for every clause C1 i n S'* there i s a m.s.l. deduction with top clause C from S'1 of a clause T"1 such that T'1 subsumes T(b l fb 2,...b n). Let D, (Fig.5) be the m.s.l. deduction of T1', with top clause C, which i s an instance of the given clause C of S. Starting from the top of D do the following operations:. a) Substitute for C the clause C of which C i s an instance, b) i f Ĉ belongs to S1', substitute for i t the clause i n S of which C[ i s an instance, c) substitute for each resolvent appearing i n D as Rl (21 ) or C£ the clause obtained under the previous substitution. ; I n [jl we can find the following r e s u l t : 'If clauses T and C have as instances respectively T' and C with resolvent Ri then there exists a resolvent R^of T and C with instance R̂ . 24. Let D' i n Fig.5a be the deduction so obtained and l e t T' be the r e s u l t of the deduction D'. Note that: a) T' does not contain b^,...bn, because b^, .. ,b n are not i n d i v i d u a l symbols i n S, b) because T' subsumes T 1 1 there i s a substi t u t i o n (b^/x-L, .. ,b n/x n) such that T" subsumes T1 ' . From the fact that Tf' subsumes T(b 1,...b ) i t follows that T1 subsumes T(x|,...x n). I t i s easy to see that the top clause condition holds for D 1 as well as the merging subsumption and no tautologies conditions. Corollary 2 :: Let S be a set of clauses, l e t C be a clause i n S, l e t T be a clause then i f S minimally implies T and T i s prime Implicate of S then there i s a m.s.l. deduction with top clause C, from S, of T. Proof: From Th.2 and from the d e f i n i t i o n of prime implicate. Section 3: The extension of set of support strategy to the consequence finding case. The set of support strategy was introduced by Woe, Robinson, Carson C l 3 l i n order to speed up the search for the deduction of the empty clause from an unsatisfiable set of clauses, when the used rules of inference are r e s o l u t i o n [133 and the paramodulation L14"]. The I n t u i t i v e idea on which the set of support strategy i s based i s e s s e n t i a l l y t h i s one: Given an unsati s f i a b l e set of clauses S, i f our goal i s the deduction of 25. t h e empty c l a u s e from S, i t i s not n e c e s s a r y t o r e s o l v e ( o r t o paramod.u]acbe) two c l a u s e s i n a s a t i s f i a b l e subset o f S. However, s i n c e the d e f i n i t i o n s a re more g e n e r a l t h a n t h i s i n t u i t i v e i d e a (22) we w i l l g i v e them ; D e f i n i t i o n Cl3jJ G i v e n a s e t S o f c l a u s e s and a subset S' of S, a c l a u s e C has Sd--support ( w i t h r e s p e c t t o S) i f e i t h e r C i s i n o r C i s a r e s o l v e n t and a t l e a s t " one o f i t s p a r e n t c l a u s e s has S ' - s u p p o r t . D e f i n i t i o n C133: G i v e n a s e t S o f c l a u s e s and a subset S 1 o f S, a S'-supported d e d u c t i o n i s a sequence o f c l a u s e s such t h a t every c l a u s e i n the sequence e i t h e r i s i n S-S' or has S' s u p p o r t . R e s u l t s : G i v e n an u n s a t i s f i a b l e s e t o f c l a u s e s S, f o r every S* subset of S, such t h a t S-S* i s s a t i s f i a b l e the r e f u t a t i o n completeness o f b o t h r e s o l u t i o n w i t h s e t o f support S' £13,141 and m . s . l . r e s o l u t i o n w i t h s e t o f su p p o r t S* [ 1~} has been p r o v e d . The way of g e n e r a l i z i n g the s e t o f support s t r a t e g y t o consequence f i n d i n g comes t o us n a t u r a l l y from o b s e r v i n g t h a t the set S' mentioned i n the r e s u l t s J u s t g i v e n i s such t h a t S-S' does not i m p l y the empty c l a u s e . T h . 3 i L e t S be a s e t of c l a u s e s , l e t T be a c l a u s e t h e n i f S i m p l i e s T, t h e n f o r ev e r y S' subset o f S such t h a t S-S* does not i m p l y T, t h e r e i s a m . s . l . S ' - s u p p o r t e d d e d u c t i o n o f a c l a u s e T' such t h a t T' i m p l i e s T. 22)pjecause we a r e i n t e r e s t e d i n s t r a t e g i e s based on r e s o l u t i o n we w i l l not mention f u r t h e r p a r a m o d u l a t i o n . 26. Proof: I f T i s the empty clause, Th.3 i s just the ref u t a t i o n completeness of m.s.l. resolution with S'-support. Otherwise, since S-S' does iaot implie T, the minimum deduction set f<5r T i s such that i t s i n t e r s e c t i o n S" with S 1 i s not empty. Let C be a clause i n S". From theorem 2 we have that there i s a m.s.l. deduction with top clause G of a clause T' such that T' implies T. This one i s just a m.s.l. deduction with set support S*. 20. CHAPTER 3: SOME DIFFERENCES BETWEEN THEOREM PROVING AND CONSEQUENCE FINDING-. In t h i s chapter we w i l l examine unit resolution, input resolution, A-ordered resolution, C-ordered resol u t i o n with respect to the consequence finding problem. Section 1:: Unit and input strategies. D e f i n i t i o n s : G-iven a set S of clauses we w i l l say that: / ' • 1) C i s an input clause i f C i s an element of S. 2) C i s a unit clause i f C i s a feast, consisting of a single l i t e r a l . 3) A deduction D i s a unit proof of a clause C i f D i s a deduction of C by resolution, and every reso l u t i o n i n D i s such that at least one of the two parent clauses i s unit. 4) A deduction D i s an input proof of a clause C, i f D i s a deduction of Cliand every resolution i n D i s such that at • least one of the two parent clauses i s an input clause. Result: Chang C33 : : I f S i s an unsatisfiable set of clauses then there i s an input proof of the empty clause from S i f and only i f there i s a unit proof of the empty clause from S. The above result was important i n theorem proving because of the ef f i c i e n c y (time and storage used) of the unit strategy ( i . e . the only allowed resolutions are unit resolutions). 28. Unfortunately, i n consequence finding (Th.4) we loose t h i s equivalence, t r i v i a l l y because for having a unit proof we must have at least some unit clause i n S. The following example shows t h i s loss of equivalence between unit and input proof: Ex: Let the following clauses "be our axioms: 1) p q 2) p q Resolving 1 and 2 we have an input proof of p, and obviously there i s not unit proof of p from 1 and 2. Th.4 ? Let S be a set of ground clauses, '.'•-1 I l e t T be a clause, l e t S imply T then i f there i s a unit proof from S of some clause T' such Ehat T* implies T, then there i s an input proof from S of some T" such that T" implies T. Proof: Since there i s a deduction by resolution from S of T' then S implies T-* and S \J ~T' i s unsatisf i a b l e . Since T' i s a set of unit clauses and there i s a unit proof of T' from S then there i s a unit proof D from S' of the empty clause (Fi g . 6 ) . By Chang's theorem there i s an input proof from S of the empty clause. In this proof remove every T̂ element of T1 on the r i g h t as shown i n Fig.7 and i n Fig.7a; the deduction so obtained i s an input proof from S of T" such that T" implies T. 29. Th.55 Let S be a set of general clauses, l e t T be a clause then i f there i s a unit proof from S of some clause T1 such that T* implies T, then there i s an input proof from S of some clause T" such that T" implies T. Proof: It follows from Trrv4 using the same method has been used for proving Th.2. We must observe that the loss of equivalence between input and unit resolution for consequence finding causes some loss of the relevance of Th.4. Section 2: Merge l i n e a r A-order resolution: D e f i n i t i o n s : Let S be a set of clauses, we w i l l say that: 1) S i s an A-ordered set of clauses i f a sequence 0 - A^-A2...An of a l l atoms i n S without repetitions i s given, 2) i s greater than A 1 i f j i s greater than i . D e f i n i t i o n : An atom and i t s negation are equal under any A-ordering. D e f i n i t i o n : Given an A-ordered set of atoms R, then i f R' i s any subset of R, the A-ordering of R' induced by an A-ordering 0 o:f R, i s the sequence 0' obtained from 0 by deleting the atoms of R-R' from 0. De f i n i t i o n : A merge A-ordered l i n e a r r esolution (m.a.l.) with top clause C from an A-ordered set of clauses S i s a deduction D (Fig.8) where: 30. a) G i s i n S, b) each resolvent i s formed by resolving upon the largest l i t e r a l under the A-ordering of S i n the clause on the l e f t i n D, c) for 0$o<n — 1 either "belongs to S or Cj_ i s some Rj for j < i , i n which case Cj_ i s a merge A-ordered resolvent and. the l i t e r a l resolved upon i n Cj_ i s a merge l i t e r a l (as well as being the largest l i t e r a l i n 4.) No clause i n the deduction D i s a tautology. Result: The r e f u t a t i o n completeness of m.a.l. resolution has been proved [83. Unfortunately, as the following example w i l l show, the completeness for consequence': finding of the m-;a.l. resolution does not hold: Ex: Consider the set of axioms S (pq, qrp., pqs).. We can easi l y see that, pr and qs are l o g i c a l consequences of S, and moreover, that they are prime implicates of S. By observing 'that r and. s do not appear negated i n S, we see that pr i s a prime implicate of pq and qrp and qs i s prime implicate of pq and pqs; then the only possible deductions of pr and qs are those ones shown i n Figs: 9, 10, 11 and 12. Just looking into deductions we convince ourselves that no A-ordering of S i s possible, i f we wish to deduce both pr and q:s. ' In fact, for deducing qs we need p q, for deducing pr. we need, q p. 31. Th.6: The m.a.l. strategy i s not complete for consequences finding. Moreover there are axiom sets for which there i s not A-ordering such that we can find a l l prime implicates of S using A-ordered resolution. Proof: The previous example proves t h i s theorem. Th.7* Let S be a set of ground clauses, l e t T be a clause, l e t C be a clause i n S, then i f S minimally implies T there i s an A-ordering of S, such that there i s a m.a.l. deduction with top clause C from S of some clause T-1 such that-T 1 subsumes T. Proof: Since S implies T, SUT i s unsati sf i a b l e . Let Sn be ?JJ$. •: ' 1 Consider S{ zi^'/G^^ & c ' r C-T) , from ' corollary 1 S£ i s un s a t i s f i a b l e . Consider Sg subset of S-£ such that S^ i s minimally unsati s f i a b l e . From the re f u t a t i o n completeness of the msa.l. strategy with top clause any clause i n a minimally unsatisfiable set of clauses considered bny clause C i n Sg and for any A-ordering 0 of Ŝ ,' there i s a m.a.l. deduction with top clause C from S^ of the empty clause. In p a r t i c u l a r , because S minimally implies T there w i l l be a m.a.l. deduction of the empty clause from S^ with top clause C' r C-T where C i s the given clause of S. Let D be such deduction (Fig.13). Clearly 0' i s an A-ordering of S since no clause i n T i s some clause of S' because S p minimally 3 2 . implies the empty clause and a l l clauses of 3 are clauses of S^ because S minimally implies T. Apply now to the deduction D the reconstruction algorithm. Let D' be the deduction so obtained (Fig. 1 3 a ) . Clearly D' i s a m.a.l. ordered deduction with top clause C from S of T', such that T' subsumes T, with 0' the A-ordering of S. Note that the A-ordering 0' for which Theorem 6 holds i s arb i t r a r y except for the fact tbs&t the l i t e r a l s belonging to T must be less than every l i t e r a l i n S under 0'. The extension of Theorem 6 to a case i n which S i s a set of general clauses ffellows from Theorem 1. (23) Th.8: Given a set of ground v r, . ('. clauses S, l e t T̂ , . ..T be prime Implicates of S, l e t S^, ...S be the minimum deduction sets respectively for T̂ ,...T such that S-̂ £ Sg...̂ S n then there i s an A-'erdering such that there i s a m.a.l. deduction of T̂ from S for every 1 < i £ n. Proof: We give the algorithm for constructing t h i s A-ordering: Let 0 be the ordered sequence of atoms i n S already constructed: Stage i : 1) Read a new l i t e r a l K 6 3. Vm : For s i m p l i c i t y we speak about a set of ground clauses, the extension of Th.8 to the general case follows as Th.2 follows from ' f i i a l i . 33. 2) I f K belongs to T± and either K or K belongs to 0 as A^i\ then drop from 0 and change every A ^ i n 0 to A^* 1* 1) for 0< h< j,go to 6. 3) I f K belongs to but K and K do not belong to 0 then change every A^*1) i n 0 i n A ( h + 1 ) go to 6. 4) I f K does not belong to and either K or K belongs to 0 then to to 7. 5) I f K does not belong to the prime implicate 1̂ but K and K do not belong to 0, i f A U ) i s the greatest atom i n 0, then put go to 7. 6) Put A ( 0 ) = K 7) C a l l 0 the new sequence of atoms obtained. I f there is^'some l i t e r a l K i n S^ not already read, get i t and %p to 1, otherwise i r i f l i i f i < n f 1 to to 1, otherwise stop. With theorem 6 i n mind, we can understand, from the following observations, that the A-ordering constructed s a t i s f i e s the condition of Th.8. Observations: 1) Substeps 2, 3 and 6 of the given algorithm are based on the fact that i f K belongs to T\ then, because Ŝ, minimally implies and because S^ £ for 1<Z , K does not appear negated i n every S^ with i *Z ( i . e . K i s never resolved i n any deduction of from S 1 ) . 2) Step 4 and 5 of the given algorithm are based on the fact that the only condition we have on the l i t e r a l s i n 34. Sj_, but not i n T̂ , i s that they must be greater than every l i t e r a l i n 1 \ . Lemma 2: I f a set of clauses S minimally implies a clause T and T i s a prime implicate of S, then there i s not a clause Q ̂ T such that S minimally implies Q and Q i s prime implicate of S. Proof: Suppose the lemma i s false then we have: a) S minimally implies T and b) S minimally implies Q and. c) both T and Q are prime implicate of 3 and d) T j Q From c o r o l l a r y ' 2 ' there w i l l he a m.s.l. deduction from S as of T as of Q. Let D and D' be such deductions. From a) there i s no t such that t i s i n T and t i s i n some clauses of S, from b) a l l clauses C i n S such that some t is i n C and t i s i n T appear somewhere in.D', then T subsumes .Q; but i f T subsumes Q because for .hypothesis Q i s prime implicate of S, T must be equal to Q contradicting the hypothesis that T £ Q, therefore the lemma holds. From theorem 8, lemma 2, and from the fact that an unsatis- f i a b l e set of clauses has as unique prime implicate, the empty clause, i t i s i n t u i t i v e l y enough clear why the m.a.l. strategy i s complete for re f u t a t i o n . (We could say just for the same reasons for which i t i s not complete for consequence finding). 35. Section 3'- Merge lin e a r C-ordered resolution. D e f i n i t i o n : An ordered clause (O-clause) i s a sequence of l i t e r a l s with no two l i t e r a l s the same. If G i s a clause we denote by (G) an O-clause obtained from C by some arbitrary but fixed ordering of i t s l i t e r a l s . I f S i s a set of clauses we denote by (S) the set S i n which a l l clauses are ordered. D e f i n i t i o n : Given two G-ordered ground clauses (G) and ( C ) , the clause w i l l be the G-ordered resolvent between (G) and ( C ) i f a) Rj_ i s a resolvent between C and G'. b) She l i t e r a , ! resolved upon i s the rightmost l i t e r a l i n (C) i f (G) i s the l e f t clause i n the deduction tree of R̂ from (C) and (C'), otherwise i t i s the rightmost l i t e r a l i n (G 1). c) I f (C) i s the l e f t clause i n the deduction tree of R̂ from (C) and (C*), and C;?-^... n and C'r c-]_... c k so that G n - c s ^ o r s o m e s ~ lc' t n e n Rj_ ^ s ^ e sequence C i » « « c n _ i followed by the sequence obtained from ci'«» c^ by deleting. c'Q-- together with any l i t e r a l c| which also occurs i n G. I f such c£ ex i s t s , i t i s a merge l i t e r a l and Ri i s an ordered merge resolvent. We w i l l write Ri as (R i). (Fig.14 i s an example of the previous d e f i n i t i o n ) . 36. D e f i n i t i o n : Let (S1.) be a set of ground O-clauses, a merge lin e a r 0-ordered (m.c.l) deduction from S i s a deduction l i k e the deduction i n Fig.1 5 where: 1) (C) i s i n S 2) For each i , 0 < i £ n-1 Either (G 1) i s i n (S) or (G i) i s some Rj ) for some j < i i n which case a) (C^) i s an ordered merge resolvent, b) the l i t e r a l resolved upon i n (C^) i s a merge literal, o S o(that the rightmost l i t e r a l of (R^) i s i t s complement. 3) No clause i n the deduction i s a tautology. With m.c.l. deduction with top clause C, we mean a m.c.l. deduction with top l e f t clause just C. Result: The re f u t a t i o n completeness for m.c.l. resolution with top clause any clause i n a minimally unsaxi sf iable set of clauses has been proved tQ~}. Th.9: The m.c.l. reso l u t i o n i s not complete for consequence finding. Moreover, there are some set of clauses S and some prime implicate T of i t such that there i s no G-ordering for which i t i s possible to have a m.c.l. deduction' of T from S. Proof: Consider the set of ground clauses S r (t-jP, t 2 r , t^q, pqr) , cl e a r l y t ^ t g t ^ i s a prime implicate of S, but i t i s easy to see that there does not exist a C-ordering of S, which allows us to hsr^e a m.c.l. deduction of t-j_t2t-jfrom S. 3 7 . As an example of the possible deductions of t - j ^ t - ^ from S see Fig. 1 6 . There the resolvent t^qtg does not allow us to define a C-ordering for that deduction. Th . 10: Let S be a set of ground clauses, l e t T be a clause, l e t C be a clause i n S such that T i s a. subset of C, then: i f S minimally implies T and T i s prime implicate of S, then there i s a C-ordering of clauses i n S for which exist a m.c.l. deduction of T from S. Proof: Because S implies T, SUT i s u n s a t i s f i a b l e . Consider the sets' such that S 1 = (c'/C <£• SUT C 1 = C-T) From corollary 1 5' i s u n s a t i s f i a b l e . Let S'1 be a subset of S' minimally u n s a t i s f i a b l e . Since S minimally implies T, there w i l l be i n S'1 some clause C, such that C = C-T and T i s a subset of C. From the refutation completeness of a m.c.l. resolution with top clause any clause i n a minimally unsatisfiable set of clauses, for any C-ordering of S'1, there i s a m.c.l. deduction of the empty clause from S 1' with top clause (C')r(C-T) where C has as i t s subset T. Let D i n Fig.17 be such deduction. Consider now the C-ordering of S such that under i t : 1) I f C i n S corresponds to the top clause (C 1) i n D then the l i t e r a l s i n T are the leftmost l i t e r a l s i n C and the l i t e r a l s i n C-f^are ordered, as the l i t e r a l s i n the top clause C' of D. 2 ) A l l the other clauses C i n S are ordered as the corresponding (C 1) i n D, and l i t e r a l s contained i n both C and T are inserted anywhere. Starting from the top of D, apply the following algorithm: 38. 1) Substitute to (C 1) the corresponding clause (C) i n (S) 2) For 0 £ i £ n-1 i f (C'± ) i s i n S' 1 substitute for i t the corresponding clause i n (S). 3) Substitute for each resolvent appearing i n D as either (R^) or (C^) the ordered resolvent obtained under the previous substitution. Let D' be such deduction, then from the following facts; a) T i s a subset of the top clause i n D', b) We merge l e f t , c) S minimally implies T (that i s no "t^ such that tj_ i s i n T, i s i n some clause of S), i t follows that D' i s a m.c.l. ordered deduction of T from S. Before going to theorem 11, l e t us make some observations about theorem 10 to indicate the difference between the consequene finding case and the theorem proving case: 1) the top clause i n the deduction s a t i s f y i n g theorem 10 i s not a r b i t r a r y , 2) the C-ordering s a t i s f y i n g theorem 10 i s arbitrary for a l l clauses i n S except for the top clause of D'. T h . l l : Let S be a set of ground clauses, l e t T]_.»«Tn be prime implicates of S, l e t C]_...Cn be clauses i n S having the following properties: a ) T± £ C± Gi £ C j for i £ j b) Gj_ €-Sj_ where Sj_ minimally implies Tj_, then there i s a C-ordering of the clauses i n S, such that there i s a m.c.l. deduction from S of every T1 for 1 < i < n. 39. Proof: Choose a C-ordering of S arbitrary except that under i t for any i , 1 ^ i ̂ n T i i s the leftmost subset of the corresponding Ĉ . From theorem 10 and the second observation above, i t i s clear that the theorem holds. Obviously, theorems 10 and 11 hold also i n the case i n which S i s a set of general clauses, t h e i r extension to a general case follows from them, as theorem 2 follows from theorem 1. 40. CHAPTER 4: INTERESTING THEOREMS As-we are interested^ i n consequence finding as a sub-field of A r t i f i c i a l Intelligence, we have to deal with the problem of how to single interesting theorems out of a l l the theorems of a given set of axioms. The aim of t h i s chapter i s to give a short review of the r e s u l t obtained up to now on t h i s problem, and make some suggestions on possible developments. Section 1: Short review on the interesting theorems problem. We w i l l report some of the work done by R.C.T. Lee [5D to give an idea on what i s known up to now on how to single interesting theorems out of a l l the theorems following from a given set of axioms. Indeed, most of the basic ideas developed up to now on t h i s subject are contained i n t h i s work. The following d e f i n i t i o n of non t r i v i a l theorem ( i . e . interesting theorem) i s given: De f i n i t i o n s : 1) A theorem T i s t r i v i a l i f i t i s implied by another theorem T' such that T' i s not equivalent to T. Given t h i s d e f i n i t i o n i t i s easy to see that: 1) The only uniform way to decide that a theorem T i s not t r i v i a l i s to prove that there i s not any theorem T1 such that T' implies T ( t h i s statement i s undecidable for meaningfull f i r s t order theories). 2) In order to single out interesting theorems, one needs a theorem proving program or a consequence finding program (in both cases one i s faced with new problems, for example i n the l a s t case, s t i l l with the problem A l . of the generation of t r i v i a l theorems). Faced with these d i f f i c u l t i e s , Lee t r i e s to give algorithms able to select prime implicates of a given set of axioms rather than interesting theorems. We notice that, although an inte r e s t i n g theorem i s prime implicate, the converse i s not necessarily true^• • .̂ As an example of the algorithms we can find i n his work we w i l l mention the following two: 1) Unit resolution p r i n c i p l e and Bound of Clause, that i s : a) clauses containing more than k l i t e r a l s are not generated, for some fixed k. b) the t r i v i a l i t y i s checked only for unit clauses. c) the unit resolution strategy i s used. 2) Axiom resolution strategy, that i s : a) axioms are resolved with axioms or with theorems, b) resolutions between theorems are forbidden. Obviously, both of these h e u r i s t i c s , as well as the other ones introduced, by Lee, do not make us sure to obtain a l l the prime implicates as well as only the prime implicates of a given set of axioms. Since Lee's work i s the only one i n which t h i s topic i s presented extensively, i t i s worthwhile to mention his opinion as a f a i r description of the stage of the research on how to single out inte r e s t i n g theorems: Remember that: i f a clause C subsumes a clause D then C implies D, but the converse i s not necessarily true. 42. The greatest f a i l u r e of t h i s research i s that the author did not sueeed i n obtaining a general theory on how an important theorem i s derived. Section 2: Observations and suggestions. To begin t h i s discussion, i t seems useful to us to stress the existence of an ambiguity i n the way the problem of how to single out inte r e s t i n g theorems i s treated. This ambiguity arises from the fact that, although one would l i k e to single out theorems which are interesting with respect to t h e i r l o g i c a l properties, necessarily one has to take into account the computational power of the actual computers. For example, i t seems clear to us that the proposal of the strategies reported i n the l a s t section i s suggested much more by considerations on the computational power of computers rather than by the o r i g i n a l purpose. In fact, i t i s possible to understand from the discussion i n Chapter 3 of t h i s thesis , on the unit and imput strategies ( i . e . the Lee's axiom resolution), that both of them do not give us any assurance even on the problem of finding prime implicates. Of course t h i s does not mean that these two strategies are completely useless for finding interesting theorems. In p a r t i c u l a r the unit strategy can be an e f f i c i e n t procedure because of our d e f i n i t i o n of theorems as disjunction of l i t e r a l s . With regard to the r e l a t i o n between results found i n our thesis and the problem i n discussion here, we f i r s t remember that an obvious consequence of the completeness of the m.s.l. strategy i s that by i t we can generate a l l prime implicates of a given set of axioms (Corollary '2). 45. However, at the beginning of our work we thought that the m.s.l. strategy would r e s t r i c t the number of uninteresting theorems more than we have actually found. To give an idea of i t s lack of effi c i e n c y with respect to t h i s problem we give the following example: Let us consider the set of axioms S (qp*, pq, pr, qr) . Clearly the clause r i s a prime implicate of S and the subset S-i_ of S such that S], - (qp, pq, p?), i s the minimum deduction set for r. Let us consider the following deductions of r from S-̂ by m.s.l. resolution: Deduction Dl ( F i g . 1 8 ) : from qp and pq, p; from p and pr, r; Deduction D 2 ( F i g . 1 9 ) : from pr" and qp", qr; from qr* and Pq, pr; from pr and pr, r; Deduction D3 (Fig.20): from pr and qp, rq"; from rq and. qp, rp; from rp and. pr, r; We see that D2 and D3 generate a r e l a t i v e l y large number of t r i v i a l theorems, namely: qr, pr, ?q, and Dl generates only prime implicates, namely: p, r. The previous example shows that the freedom with respect to the top clause that we have i n mss.l. strategy i s paid with a loss of e f f i c i e n c y . 44. However, there i s an obvious difference between Dl and the deductions D2 and D3, namely that i n Dl we introduce our theorem l i t e r a l s as la t e as i s possible; i t i s easy to see from the ch a r a c t e r i s t i c s of the minimum deduction set that this fact cut-off the generation of clauses subsumed by our theorem. We have mentioned t h i s difference between Dl and D2 and D3 because we hope that i t could suggest some possible implementation of the m.s.l. strategy with respect to finding interesting theorems. Furthermore, we suggest using the mss.l. strategy supplemented by the rule of deleting every l e f t theorem that i n a m.s.l. deduction we resolve with theorem, instead of the Lee's axiom resolution. As far as the other strategies discussed i n our thesis are concerned, we stress that t h e i r a p p l i c a b i l i t y to the interesting theorems problem presents d i f f e r e n t but not minor d i f f i c u l t i e s to those of the mss.l. The m.a.l. and the m.c.l. strategies are almost useless for finding, i n t e r e s t i n g theorems, since they are applicable to consequence finding only i n very peculiar cases. The m.s.l. strategy with set of support presents the obvious d i f f i c u l t y that i s i s undecidable whether a given set of axioms i s a minimum deduction set for a theorem T. However, i n t h i s case, as a possible suggestion for developing e f f i c i e n t strategies for finding prime implicates we give the following procedure: Let S be a set of ground clauses, 45. 1) Consider one l i t e r a l K contained, i n some clause of S. 2) Consider the subset S 1 of S such that K does not appear i n any clause of S' and. K appears i n a l l the clauses of S-S1. 3) I f K i s prime implicate of S, we w i l l find i t from S'' by m.s.l. In t h i s case we choose another l i t e r a l i n S and we repeat the procedure applied to K. If K i s not prime implicate of S we ce r t a i n l y w i l l deduce a l l prime implicate i n K of S". Let T be one of them, we consider the set of clauses S'OT and for a l l of the l i t e r a l s contained i n i t we apply the same procedure we applied to K. We notice that t h i s procedure as i t stands i s not applicable to the case of a set of general clauses. Conclusions We think that the completeness for consequence finding of the m.s.l. strategy, proved, i n t h i s thesis, i t s completeness, for r e f u t a t i o n already well known, and i t s s i m p l i c i t y can help i n better understanding the laws of the l o g i c a l deduction. It i s already well known that the m.s.l. re s o l u t i o n has a higher e f f i c i e n c y than simple resolution, because of the r e s t r i c t i o n s i t puts on the deduction. The completeness theorem that we have proved allows us to use i t i n consequence finding instead of ordinary resolution. Furthermore, i t seems that the m.s.l. strategy, when supplemented with a certain h e u r i s t i c procedure can usefully supplement Lee's axiom resolution v/ith respect to the interesting theorems problem. 46. We have also seen i n t h i s thesis that the m.a.l. and. the m.c.l., although complete for theorem proving, are not complete for consequence finding and that the m.s.l. strategy with set of support although complete i s d i f f i c u l t to use. This seems to support our i n i t i a l f e e l i n g on the difference between theorem proving and consequence finding, and, at the same time, provide some insight i n both f i e l d s . In p a r t i c u l a r , i t seems to us that our results suggest the following conclusions: 1) The completeness for consequence finding and the degree of a p p l i c a b i l i t y to consequence finding of a given strategy can be taken as c r i t e r i o n of i t s e f f i c i e n c y for theorem proving. We guess that the less a strategy i s applicable to consequence finding the more e f f i c i e n t i t i s for theoEm proving. 2) The generality of a strategy, for example i t s completeness for both consequence finding and theorem proving, i s paid i n i t s e f f i c i e n c y . We believe i n fact that theemore e f f i c i e n t a strategy i s the more i t i s applicable to the deduction of peculiar classes of theorems. Support for t h i s idea comes to us, not only from the r e s u l t s mentioned above, but also from the following r e f l e c t i o n on the nature of theorem proving. We can i n fact regard theorem proving as the problem of finding prime implicates of an unsatisfiable set of clauses; then the compatibility between the completeness of a strategy and i t s e f f i c i e n c y seems to us related to the lucky s i t u a t i o n that for an unsat i s f i a b l e set of clauses the set of prime implicates reduces to a single element, the empty clause. 47. On the basis of these considerations i t seems to us that a possible l i n e of development of the f i e l d of consequence finding i s to search strategies related to the l o g i c a l properties of theorems and axioms, rather than complete strategies. An amusing, example of theorems the computer can derive, when the strategy used completely disregards the semantics, i s the following given by R.G.T. Lee 5 : Consider the case i n which we have the following statements as axioms: 1) I f M has y z's and z has v'w's, then x has y ; ;v w's 2) Man has 2 hands; 3) Hand, has 5 fingers. These three axioms can be put into three clauses as follows: 1) p(x,y,z) p(z,v,w) p(x,f(y,v)w) 2) p (man, 2,hand) 3) p(hand,5,finger). By m.s.l. we can deduce from 1 and 2 p(x,y,man)p(x,y#2,hand). We can e a s i l y see that the above clause, although i t i s a theorem, does not have an acceptable meaning,;' then i t s deduction i s completely useless. We think that a point of view very similar to the one we have just discussed for consequence finding should also be taken when dealing with the problem of how to single out interesting theorems. Moreover, i n t h i s case we want also to notice that, although important semantic and syntactic properties d i f f e r e n t i a t e .the class of prime implicate from-the other theorems, further subdivisions of t h i s cla'ss could be useful for finding more e f f i c i e n t . s t r a t e g i c s and getting more insight into what i s meant by 'interesting theorems'. l«T- P Q-Cu J): cs— FOQ : 1} fa:** 48. BIBLIOGRAPHY 1. Anderson, R., Bledsoe, W.W. A Next Technique for Establishing Completeness. J. ACM, Vol . 1 7 , 3'(July 1970) pp.525-534. 2. Andrews, P.B. Resolution With Merging. J. ACM, Vol . 1 5 , 3(July 1968)pp.367-381. 3 . Chang, C.L. The Unit Proof and the Input Proof i n Theorem Proving. J.ACM, 17,4 (October 1970) ppr.698-707. 4. Davis, M. Eliminating the Irrelevant from Mechanical Proofs. Proc. of Symposia i n Applied Mathematics. American Mathematical Society (1963) pp.15-30. 5. Lee, R.C.T. A Completeness Theorem and a Computer Program for Finding Theorems Derivable from Given Axioms. Doctoral Dissertation, Department of E l e c t r i c a l Engineering and Computer Science, University of C a l i f o r n i a , Berkeley, 1967. 6. Loveland, D.W. A Linear Format for Resolution. Carnegie Mellon University:;- Pittsburg, Pa., December 1968. 7. Mendelson, E. Introduction to Mathematical Logic. Princeton N.J., Van Nostrand 1964. o. Reiter, R. Two Results on Ordering for Resolution with Merging and Linear Format. J. ACM, 18, 4(0ctober 1 9 7 D , pp.630-646. 9 . Robinson, J.A. A Machine Oriented Logic Based on the Resolution P r i n c i p l e . J. ACM, Vol . 7 (January 1965) pp.23-41. 10. Robinson, J.A. A Review of Automatic Theorem Proving. Annual Symposia i n Applied Mathematics, Vol.XIX (1965). 11. Slagle, J.R. Automatic Theorem Proving with Renamable and Semantic Resolution. J. ACM, Vol . 1 2 , 4(0ctober 1967), pp .687- 697. 12. Slagle, J.R., Chang, C.L., Lee, R.C.T. Completeness Theorems for Semantic Resolution for Consequence Finding. Div. of Computer Res. and Technol. National Institute os Health, Bethesda, Md., 1969. 13. Wos, L., Robinson, G.A., Carson, D.F. E f f i c i e n c e and Completeness of the Set of Support Strategy i n Theorem Proving. J. ACM, Vol.12, 4 (October 1965), pp.536-541. 14.. Wos, L., Robinson, G.A. Paramodulation and Set of Support. Symposium on Automatic Demonstration. V e r s a i l l e s (France) December 1968.
Cite
Citation Scheme:
Usage Statistics
Country | Views | Downloads |
---|---|---|
United States | 2 | 0 |
Russia | 1 | 0 |
China | 1 | 23 |
City | Views | Downloads |
---|---|---|
Unknown | 2 | 0 |
Redmond | 1 | 0 |
Beijing | 1 | 0 |
{[{ mDataHeader[type] }]} | {[{ month[type] }]} | {[{ tData[type] }]} |
Share
Share to: