UBC Theses and Dissertations

UBC Theses Logo

UBC Theses and Dissertations

A unit resolution theorem proving system LeQuesne, Peter Neave 1972-12-31

You don't seem to have a PDF reader installed, try download the pdf

Item Metadata

Download

Media
[if-you-see-this-DO-NOT-CLICK]
UBC_1972_A6_7 L46.pdf [ 1.93MB ]
Metadata
JSON: 1.0051190.json
JSON-LD: 1.0051190+ld.json
RDF/XML (Pretty): 1.0051190.xml
RDF/JSON: 1.0051190+rdf.json
Turtle: 1.0051190+rdf-turtle.txt
N-Triples: 1.0051190+rdf-ntriples.txt
Original Record: 1.0051190 +original-record.json
Full Text
1.0051190.txt
Citation
1.0051190.ris

Full Text

A UNIT RESOLUTION THEOREM PROVING SYSTEM  by PETER NEAVE LEQUESNE B.Sc,  University of B r i t i s h Columbia, 1963  A THESIS SUBMITTED IN PARTIAL FULFILMENT OF THE REQUIREMENTS FOR THE DEGREE OF Master of Science i n the Department of Computer Science  We accept this thesis as conforming to the required standard  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 B r i t i s h 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 by his representatives.  be granted by the Head of my  Department or  It is understood that copying or publication  of this thesis for financial gain shall not be allowed without my written  permission.  Department of The University of B r i t i s h Columbia Vancouver 8, Canada  Abstract  A unit resolution theorem proving system i s developed compared with the previous work of C.L.  Chang.  This thesis  and includes  a description of a p a r t i c u l a r approach to unit resolution and description of the r e s u l t i n g program and i t s effectiveness.  a  ii Table of Contents I  Concepts and Terminology  1  1.  Introduction  1  2.  Preliminary Formulation  of the Axioms and  1  Proposed Theorems 3.  The Unit Proof  3  4.  U n i f i c a t i o n and Substitution for a Unit  4  Proof  II  III  IV  5.  Subsumption  5  6.  The "hyper" Unit Resolution Strategy  5  7.  Embedded Equality Axioms  7  A Description of the Program and i t s Use  9  1.  Input to the Program  9  2.  Program Operation  10  3.  Program Output  13  Evaluation of Experimental Results  16  1.  Comparison with the work of Chang  16  2.  Comments on the Differences i n the Results  17  Possible Directions f o r Further Work  19  1.  The Nature of I n f e r e n t i a l Unit Resolution  19  2.  Heuristic Tree Search  19  3.  Concluding  20  Remarks  Bibliography  22  Appendix 1  23  Appendix 2  25  Appendix 3  27  Appendix 4  28  iii Appendix 5  29  Appendix 6  37  L i s t of Tables  Table 1  A Comparative Table of Chang's Exampl  v  Acknowledgement  Most of the ideas developed i n this thesis are the suggestions of Professor Raymond Reiter.  I am deeply grateful  for the patient assistance he has given me i n completing this work. Thanks are also extended to the Department of Computer Science f o r a most s a t i s f y i n g two years of study and to Mrs. Olwen Sutton for an excellent typing job.  1. I  Concepts and Terminology  1.  Introduction Application of the f u l l resolution proof procedure normally  results i n a very large amount of matching and clause generation. Unit resolution i s a means of reducing the size of such problems. This work i s an implementation  of a p a r t i c u l a r form of unit resolu-  t i o n , p a r a l l e l i n g closely that of C L .  Chang [2].  This Chapter  outlines the t h e o r e t i c a l basis of the program produced and describes the notation and terminology used.  A f u l l description of  resolution i s not attempted however unit resolution w i l l be described as a s p e c i a l case of the more general 2.  technique.  Preliminary Formulation of the Axioms and Proposed Theorem. For any resolution procedure, the axioms and proposed theorem  of a given system must be expressed i n a p a r t i c u l a r format for expressions of f i r s t order mathematical l o g i c called conjunctive normal form.  Procedures for converting to conjunctive normal form  are given i n [3] and [8].  A conjunctive normal form (cnf) has  the  following structure. Let  C^,...,C^ be l o g i c a l phrases called clauses.  Then a c.n.f.  has the following form: C. A C„ A ... A C. 1 2  k  That i s , a c.n.f. i s a conjunction of clauses. disjunction of l i t e r a l s .  A clause i s a  Say L^,...,L^ are l i t e r a l s then a clause  has the following structure for M > 0: L^ v ... v L^.  A  literal  i s a l o g i c a l phrase of the following general form, where + or indicates a sign, P a predicate symbol, and t ^ , . . . , t ^ are expressions  2. called terms:  ± P t^,...,t^  for some k > 0.  A term may be a free  v a r i a b l e , a constant or a functional value where a functional value i s a functional symbol followed by a number of terms i n brackets, e.g., f(t^,...,t£) for some H > 0.  Consider the following examples of  a)  a free v a r i a b l e , x  b)  a constant, 3  c)  a functional value, g(x,3)  d)  a l i t e r a l , + T x g(x,3) x  e)  a clause, + P x g(x,3) x V + Q x, g(x,5), 5  f)  a c.n.f.  }  + P x g(x,3) x V + Q x g(x,5) 5 A + T x g(x,3) x For purposes of programming i n the LISP 1.5  language the following  notation i s used for the date types described above 1)  A free variable i s designated by the l e t t e r x followed by  any  number, e.g. x20, xl5. 2)  A constant i s any other l e t t e r or an integer, e.g. A,B,C,1,15,10.  3)  A functional'value has the following l i s t form (F t ^  t^-•-tyj  for example (F 1 x3 10) or (G x l x2). 4)  A l i t e r a l i s again a l i s t but always begins with a + or - sign followed by a predicate symbol.  For example: (+ P x l x2  x3)  or (- Q (F xl) 2) 5)  A clause i s simply a l i s t of its, l i t e r a l s .  Further information  on input of the c.n.f. to the program i s given i n Chapter 2. Fundamental to this thesis i s the concept of a unit clause. unit clause i s a clause of one l i t e r a l .  A  For instance (( - P x l x2))  where one set of brackets denotes a clause and the other a single l i t e r a l , i s a unit clause.  In p r a c t i s e , for example, i n the context  3. of the program written, the outer set of brackets i s dropped. For a unit resolution theorem prover to proceed on a proposed theorem and associated set of axioms at least one unit clause must be present i n the associated conjunctive normal form. 3.  The Unit Proof A resolution proof i s normally sketched as an inverted binary  tree whose bottom-most node i s the • symbol.  A unit proof i s defined  as a resolution proof such that for each node generated downwards i n the proof tree, at least one parent node i s a unit clause.  For  example i f we denote unit clauses as U^, regular non-unit clauses as C_. and have the following c.n.f. ;  A  A  A  A C^; then if_ a  proof for this c.n.f. i s found as follows,  • we then have a proof by unit resolution. Normal resolution i s a process combining clauses u n t i l two clauses combine to n i l or •.  clauses to form  In the above hypo-  t h e t i c a l diagram, three new unit clauses (U^, U^, U,.) and two non-unit clauses (C^, Cj.) are generated.  new  new  In each case the new  clause has at least one parent which i s a unit clause.  Since we  are describing what i s r e a l l y a combining process an.-advantage of unit resolution i s apparent.  For any given resolution the length of  4. the newly generated clause ( i . e . , the number of l i t e r a l s which i t contains) w i l l be one less than that of the non-unit parent.  An  approach which attempts to make such unit resolutions f i r s t i n search of a proof i s termed the unit preference strategy [1],  The theorem  proving system developed i n this work does not attempt non-unit resolution and hence w i l l not succeed on problems which do not have a unit proof.  That i s , i t w i l l not prove proposed theorems whose  c.n.f. has no unit clauses or whose proof i s dependent on the resolution of two non-unit 4.  clauses.  U n i f i c a t i o n and Substitution for a Unit Proof. E s s e n t i a l l y , u n i f i c a t i o n i s the process of finding a common  instance of two sets of terms.  For the purposes of resolution  these two sets of terms appear i n separate clauses and are associated with the same predicate symbols of d i f f e r i n g signs.  This common  instance of two sets of terms i s demonstrated by the generation of a s u b s t i t u t i o n to be made to the two clauses i n question, the result of which i s the presence of contradictory l i t e r a l s within the clauses i n question, which are then combined to form a resolvent (minus the contradictory l i t e r a l s ) .  Further to the concept of a unifying  s u b s t i t u t i o n , i s the idea of a most general u n i f i e r .  This notion  which i s developed i n (10) b a s i c a l l y means that there exists a substitution for two u n i f i a b l e l i t e r a l s such that the most general common instance of the two i s the r e s u l t . In normal resolution systems i t i s necessary  to apply a unifying  substitution to both clauses being resolved as the two w i l l be combined (minus the l i t e r a l s "resolved away") to form a new clause.  5. Here u n i t r e s o l u t i o n has the p a r e n t  Because one  clauses i n u n i t r e s o l u t i o n i s a u n i t clause, a  s u b s t i t u t i o n need o n l y be literal).  Since  considerable 5.  a s p e c i a l advantage.  a p p l i e d to one  clause  (minus the  of  given resolved  these s u b s t i t u t i o n s are q u i t e expensive t h i s i s a  advantage.  Subsumption C l o s e l y r e l a t e d to the concept of u n i f i c a t i o n i s the subsumed  clause.  A c l a u s e M i s s a i d to be subsumed by  e x i s t s a s u b s t i t u t i o n 0 such t h a t N 6 £ M.  a clause N i f there  B a s i c a l l y , t h i s means  whenever M i s t r u e , N i s t r u e and hence t h e r e i s l i t t l e terms o f the r e s o l u t i o n process  value i n  i n k e e p i n g the subsumed c l a u s e .  A check f o r subsumed c l a u s e s i n i n c l u d e d i n t h i s  theorem p r o v i n g  system. 6.  The  "hyper" U n i t R e s o l u t i o n  Consider  Strategy  a sequence of r e s o l u t i o n s o f the f o l l o w i n g type where  a, a are u n i t c l a u s e s and 5, v 5L I n 1 2 c l a u s e (axiom):  cL v a 1  0  2  v . . . v a  v  n  a  3  a.2 v  a3 v a4 v  v  a  n  v g is a  v ... v a  v 3  a  n  n  non-unit  6. In short where a l l the consequent l i t e r a l s may unit clauses i t i s possible that a new by i n this case n resolutions.  be matched with known  unit clause can be generated  A necessary condition for this to  occur i s that the l i t e r a l s must have d i f f e r i n g signs and matching predicate symbols with their corresponding units i n {a^}. additional each l i t e r a l / u n i t p a i r must unify at the stage of the o v e r a l l resolution sequence. strategy i s simply fashion.  In  appropriate  The "hyper" unit resolution  to generate only unit resolvents i n the above  The n resolutions outlined above are treated as occurring  simultaneously  for purposes of retaining new  resolvents.  A resolvent  is generated only i f i t i s a unit clause, that i s , a l l l i t e r a l s appearing i n a given axiom except the "target" l i t e r a l  already  e x i s t as axioms or previously generated unit resolvents.  This target  l i t e r a l , i.e. , that l i t e r a l of the axiom which becomes the unit resolvent, may  be any of the l i t e r a l s appearing i n the axiom.  The use of this apparent r e s t r i c t i o n on clauses generated by unit resolution greatly reduces the number of clauses generated for further use i n search of a contradiction.  For instance  (not  including multiple instances of the same target l i t e r a l : which d i f f e r i n t h e i r terms) for three axioms of length four there are twelve possible unit resolvents while there are forty-eight possible resolvents including non-unit clauses.  Appendix 1 contains a f u l l  example demonstrating this advantage. The following theorem demonstrates that the use of "hyper" resolution i s i n fact not a further r e s t r i c t i o n on the effectiveness of unit resolution.  "A set of clauses can be proved i n s a t i s f i a b l e  7. by unit resolution i f and only i f i t can be proved u n s a t i s f i a b l e by "hyper" unit resolution".  C l e a r l y , from the d e f i n i t i o n of unit  resolution, any proof by regular unit resolution can be converted to a proof by "hyper" unit resolution and hence the proof i s t r i v i a l . There i s s i g n i f i c a n t combinatorial aspect of "hyper" resolution to be described.  Consider the generation of unit resolvents  clause C = L., v ... v L  1  r  of r l i t e r a l s .  which may become unit resolvents.  from a  There are r possible K  These possible'"target"  literals  literals  each may become a unit clause after r - l other l i t e r a l s are resolved away using the, say k, unit clauses available. that a l l possible resolvents  In order to insure  are generated at a p a r t i c u l a r l e v e l , i t  i s necessary to match each sequence of r - l l i t e r a l s corresponding to a p a r t i c u l a r target l i t e r a l with a l l possible l i s t s of length r - l of e x i s t i n g units.  Since a given unit may be used more than once  kfr—2 there are ( _^ ) such combinations of units. r  Each of these combinations  may be ordered i n ( r - l ) ! ways hence f o r a clause c of r possible k+r-2 target l i t e r a l s there are (  ) ( r - l ) ! * r combinations of clause  l i t e r a l s and unit clauses to be checked for possible r e s u l t s .  Thus  i t i s clear that while the number of retained units i s s i g n i f i c a n t l y reduced with a "hyper" resolution approach there i s no reduction  apparent  i n the amount of matching which must take place i n order to generate a p a r t i c u l a r unit 7.  clause.  Embedded Equality Axioms. The  treatment of problems of proof generation with axiom sets  expressing equality has had considerable attention i n a number of papers on mechanical theorem proving [ 7 , 9 ] .  The problem i s a  f a m i l i a r one - only more so. Consider the following axiom ( r e f l e x i v e ) :  8.  E ( x l x2) => E (x2 x l ) or i n clausal form  E ( x l x2) v E (x2 x l ) .  Now any unit clause with E as i t s predicate symbol w i l l unify with one or the other of the l i t e r a l s i n this clause. abnormally  In consequence an  large number of new unit clauses w i l l be generated, most  of which are quite useless to the production of a proof.  Since the  nature of axioms expressing equality are r e l a t i v e l y mechanical i n their e f f e c t , treating them as any other axiom unnecessarily marrs the e f f i c i e n c y of a theorem proving program.  Such axioms may be  embedded within the code of the program and thus produce much more e f f i c i e n t l y as required.  In! l i g h t of this the axioms of r e f l e x i t i v i t y  and t r a n s i t i v i t y of equality, i . e . , E ( x l x2) ^ E (x2-xl) and E ( x l x2) A E (x2 x3) => E ( x l x3) have been coded d i r e c t l y into this program and may be used by setting a switch variable on input.  9. II  A Description of the Program and i t s UseThe "hyper" unit resolution strategy described i n Chapter I  has been implemented as a theorem proving program written i n LISP 1.5 [ 5 , ' l l ] .  Appendix 4 outlines how this program may be accessed  on the U.B.C./MTS system.  This chapter comprises  a description of  the input format required, an outline of the flow of processing performed by the program and f i n a l l y a description of program output and i t s interpretation. 1.  Input to the Program A representation of the conjunctive normal form of a given  proposed theorem and a few c o n t r o l l i n g parameters are passed to the predicate UPR00F i n order to i n i t i a t e the generation of a proof. This c a l l has the following general form: UPR00F (CLAUSES UNITSET DEPTH FD ES) CLAUSES i s a structured l i s t of the non-unit clauses of the c.n.f. and UNITSET i s a l i s t of the unit clauses.  DEPTH i s an integer  i n d i c a t i n g the allowable number of times the CLAUSES may be used before q u i t t i n g the search f o r a proof.  FD, also an integer,  indicates the maximum function depth i n retained unit clauses. ES i s a switch variable; i t s value i s T i f embedded equality relations are to be used and NIL otherwise. The l a t t e r three parameters have a s e l f explanatory format as indicated i n the example which follows.  CLAUSES and UNITSET, however,  require further description. CLAUSES has a certain amount of structure i n i t s format i n order to aid the search process of the program.  As indicated  e a r l i e r i n Chapter I, a clause i s represented as a l i s t of i t s  10. l i t e r a l s which i n turn are l i s t s of signs, predicate symbols and variables etc.  An example i s ((+ P x l x2)(+ Q x l x2)(+ R x2 x3)).  Given this format for a clause, CLAUSES i s imply a set of clauses grouped by length.  In other words, CLAUSES i s a l i s t of l i s t s of  clauses, each s u b l i s t containing clauses of the same length.  The  following i s a set of four clauses so arranged: ((((+  P x l x2)(+ Q x2 x3()- R x l x2)))  (((+ P x2 x3)(- Q x3 x2)(- P x3  x2))  ( ( - R x l x4)(+ Q x l x2)(+ P x l x2))) (((+ P x l x2)(- Rx2  xl))))  UNITSET i s simply a l i s t of unit clauses.  As e a r l i e r mentioned  i n Chapter I, the additional set of brackets which would normally denote a clause as opposed to a l i t e r a l have been dropped hence UNITSET appears as shown i n the following example: ((+ P x l x2)(+  Q  x l x3)(- R x2  x3))  A l l variables which appear i n CLAUSES and UNITSET are according to the following condition.  The same variable name may  appear i n two or more non-unit clauses but may unit clause.  x-standardized  not appear i n any  In addition those variable names occurring i n a unit  clause must be d i s t i n c t from a l l other variable names appearing i n unit clauses (as w e l l as those appearing  i n CLAUSES).  to avoid ambiguity i n u n i f i c a t i o n and substitution.  This i s done In addition a l l  variable names must include an integer larger than 20 to avoid c o n f l i c t with i n t e r n a l variables i n the equality processing. complete example of a c a l l to UPR00F follows:  A  11. UPR00F ((((+ P xlOO)(+ D (G xlOO) xlOO)) ((+ P xlOO)(+ L 1 (G xlOO))) ((+ P xlOO)(+ L (G xlOO) xlOO)) ( ( - P xlOO)(- D xlOO A))) ( ( ( - L 1 xlOO)(- L xlOO A)(+ P (F xlOO))) ( ( - L 1 xlOO)(- L xlOO A)(+ D (F xlOO) xlOO)) (- D xlOO x200)(- D x200 x300)(+ D xlOO x300)))) ((+ D x400 x400)(+ L 1 A)) 5 3 This i s a formulation 2.  NIL)  of example eight from Chang [2].  Program Operation This program generates and tests unit clauses i n a breadth  f i r s t fashion using the general procedure outlined i n the  following  steps. 1.  Select a set of non-unit clauses of the same length (SLCSET)  2.  Generate a l i s t of unit clauses from the unitset (UNITS)  3.  If l e v e l of generation i s greater than one test above units for presence of at least one unit from previous level.  4.  Match UNITS against a l l 10. clauses i n SLCSET and generate any new resolvents possible. 11. Test newly generated resolvents for function depth and subsumption by other units.  5.  6.  7.  Is a new s t r i n g of units possible i f so go to step 2.  8.  Is a new set of clauses of the same length available? If yes, go to step 1.  9.  Test a l l units generated at this l e v e l for contradiction and subsumption among each other i f contradiction return T, i f no units remain return 1.  Test remaining units generated for contradiction with other units already e x i s t i n g , i f found return T.  Has maximum depth of clause use been reached i f so return 0. Update unitset with newly generated units and go to step 1.  12.  In short, this program matches every clause of length t-1 a given l e v e l .  Using clause rotation each l i t e r a l i n a clause i s  treated as a possible unit resolvent. algorithm  at  A simple  combinatorial  [4] i s used to.generate l i s t s of units from the UNITSET  of a given l e v e l .  I n i t i a l checks are made on such l i s t s and a given  clause (or rotation of a clause) to insure appropriate sign and predicate symbols i n each l i t e r a l p a i r from l e f t to r i g h t .  Given  the success of the above test, u n i f i c a t i o n and s u b s t i t u t i o n proceed on the l i t e r a l pairings from the l e f t u n t i l the given l i s t of units i s exhausted or u n i f i c a t i o n f a l l s .  I f a unit resolvent i s generated  i t i s tested for function depth, subsumption by e x i s t i n g units and for possible contradiction by resolution against one of the e x i s t i n g units.  I f i t does not contradict or f a i l the other test i t i s  saved for use during the next l e v e l of resolution. There are three major sections or LISP functions i n this theorem proving system.  They are UPR00F, AL0NZ0I, and SIGMA.  UPR00F i s the o v e r a l l driver of the system.  I t controls passage  through the clauses, updates the set of units between levels of clause use, and communicates with the user.  UPR00F c a l l s on  AL0NZ0I to perform the matching of clauses with l i s t s of units and to do most of the screening of generated unit clauses. AL0NZ0I i s the most active of the functions-of the system.  It  generates l i s t s of units of the appropriate length for the clause or clauses i t has been passed, checks f o r sign and predicate symbol matching, controls and c a l l s the u n i f i c a t i o n and s u b s t i t u t i o n functions as required, rotates clauses as needed, and performs subsumption, function depth and contradictory unit tests as needed.  If a  13. contradiction i s found or a l l possible units have been generated for a given l i s t of clauses of the same length, AL0NZ0I returns to UPR00F. SIGMA, i s the controling LISP function for a c o l l e c t i o n of routines which perform u n i f i c a t i o n ( i f possible) f o r a given p a i r of l i s t s of terms of a l i t e r a l pair.  SIGMA produces a most general  u n i f i e r i f u n i f i c a t i o n i s possible or else returns the LISP atom NIL. In order to obtain a run which u t i l i z e s i m p l i c i t coding of the equality axioms, i . e . , E (x, y) A E (y, z) = E (x, z) E (x, y) a E (y, x) the value of the input variable ES must be T.  In order to have  these axioms be e f f e c t i v e at the appropriate point i n use of the clauses there are a few dynamic switch variables set i n UPR00F and passed to AL0NZ0I. generate new  The function EQGEN i s called by AL0NZ0I to  units r e s u l t i n g from said axioms, when such generation  i s signaled by UPR00F. Appendices 2 and 3 contain r e l a t i v e l y detailed flow charts for UPR00F and AL0NZ0I and Appendix 5, The LISP Code. 3.  Program Output A machine generated proof must be recoverable.  This program  achieves this condition for i t s proofs by printing out the h i s t o r y of a unit just after i t has been generated. i s as follows:  This history's format  14. < parent c l a u s e o r a r o t a t i o n of that clause > < the l i s t of u n i t s used to r e s o l v e a g a i n s t the c l a u s e above > < the u n i t r e s o l v e n t > an example might  be;  CLAUSE 'USED ((- P x l x 2 ) ( - P x2 x3)(+ UNITS USED ((+ P A B ) (+ P B C)) RESULTANT UNIT CLAUSE (+ P A C)  U n i t s generated by simply  listed  with previous  the use  P x l x3))  of i m p l i c i t e q u a l i t y axioms are  as such and n o r m a l l y existing units.  are simply  t r a c e d by  checking  Upon the d i s c o v e r y of two  u n i t c l a u s e s , UPR00F r e t u r n s the v a l u e T.  The  two  contradictory  u n i t s which  c o n t r a d i c t are p r i n t e d under the heading. PR00F F0UND F0R At t h i s p o i n t the u s e r may theorem i n q u e s t i o n by question.  THIS THE0REM r e c o n s t r u c t the p r o o f  t r a c i n g the p r i n t e d h i s t o r i e s o f the u n i t s i n  S i n c e v a r i a b l e s are r e s t a n d a r d i z e d  w i t h i n the p r o o f  generation process,  back f o r a d i f f e r e n t i n s t a n c e the c u r r e n t u n i t b e i n g Each time a new of c l a u s e use,  t r e e f o r the  relatively  often  the user must g e n e r a l l y  look  ( i n r e s p e c t of v a r i a b l e names) than  traced.  s e t of c l a u s e s i s passed to AL0NZ0I, the  c l a u s e s p a s s e d , and new  u n i t s from the p r e v i o u s  level label  are p r i n t e d . If  the program f a i l s to f i n d a p r o o f i t w i l l be  a r e t u r n v a l u e o f 0 or 1 or an obvious time over-run.  i n d i c a t e d by A r e t u r n value  15. of 0 indicates that a proof was not found at the maximum depth s p e c i f i e d by the input parameter DEPTH.  A return value of 1  s i g n i f i e s that at the l a s t indicated l e v e l of clause use no  new  units were generated (or more s p e c i f i c a l l y no new units were generated that passed both the subsumption tests).  and function depth  In the l a t t e r circumstance, i f a greater function depth  does not change matters then no unit proof exists f o r the proposed theorem. The output format described above i s motivated by two considerations; generation of a trace of a proof i s costly and involves a considerable amount of programming and, secondly, to e f f e c t i v e l y study the possible implementation of h e u r i s t i c s i n a theorem prover i t i s h e l p f u l to p r i n t as much as possible concerning the directions taken. A sample run i s given of example 1 from Chang i n Appendix 6.  16. Ill  Evaluation of Experimental Results  1.  Comparison with the work of Chang-- [2] Apart from h i s 'use of the set of support technique, the work of  Chang i s quite similar to that presented here.  The following table  displays the results of the two programmes when applied to the examples given by ChangEXAMPLE #  UNITS GENERATED  CLAUSE DEPTH  UNITS RETAINED  TIME (sec)  1  16 2  1 1  0 0  1.550 .524  2  109 72  3 2  3 4  7.510 28.222  3  44 14  3 2  3 3  3.417 3.821  4  32 14  2 1  2 0  2.650 2.0.51  5  21 1  1 1  0 0  0.667 0.646  6  32 74  2 1  1 0  2.300 15.267  7  58 6  2 1  5 0  3.566 5.602  8  65 17  ?  4  11 4  5.184 4.843  ?  34 15  4  10 9  4.050 6.640  10(a)  136 154  4 2  17 16  24.550 31.457  10(b)  59 169  3 2  6 16  9.367 37.228  10(c)  53 141  3 2  4 16  6.916 28.151  10(d)  48 167  3 2  5 16  7.317 37.055  9  TABLE I :  A Comparative Table of Chang's Examples  17. For each entry i n the table the value obtained by Chang i s followed by that obtained with this system.  The column headings  have the following, more elaborate explanations: UNITS GENERATED - the t o t a l number of unit clauses produced before a proof was found. CLAUSE DEPTH  - the number of times the set of non-unit  clauses  was used i n order to find a proof. UNITS RETAINED  - the number of generated unit clauses which were retained for use i n further levels before a proof was found.  Comparison of the two sets of results reveals the following general differences: (1)  With:••the exception of examples 6 and 10 this system produces  s i g n i f i c a n t l y fewer unit clauses than Chang's. (2)  The clause depth necessary f o r proof f o r this system i s most  often lower than that f o r Chang's. (3)  Relative to the number of clauses generated, the number of  clauses retained by both programmes i s about the same. (4)  The running times required by Chang's programme are (not  withstanding differences i n hardware and software)  significantly  lower than those required by this programme. 2.  Comments on the Differences i n the Results The conclusions stated here are by necessity somewhat  speculative both f o r reasons of inadequate  information about the  i n t e r n a l operation of Chang's system and, perhaps more importantly, lack of an adequate or conclusive technique for measuring the effectiveness of a theorem proving programme [6],  18. Points (1) and (2) are probable evidence of an inherent disadvantage of the set of support strategy.  Simply put, i t quite  often results i n deeper proofs than are necessary.  In many  circumstances an " i n f e r e n t i a l " proof exists at a shallower depth than one provided by set of support.  The set of support programme  must pass through, i n general, more levels of clause use (and generate more clauses as a result) i n order to f i n d a contradiction. This f a u l t i n the set of support approach i s probably not p a r t i c u l a r l y s i g n i f i c a n t for theorems which do not admit to a r e l a t i v e l y simple i n f e r e n t i a l proof. It should be noted at this point that although not e x p l i c i t l y stated, Changes program i s using the same basic strategy as the "hyper" unit resolution developed here.  In addition, h i s routine  includes a mechanism to avoid the generation of duplicate clauses. Point (3) i s approximately as expected since the routines have the same clause rejection mechanisms, i . e . , subsumption and function depth. Point (4), judging by points ( l ) - ( 3 ) , relates to the amount of e f f o r t expended on non-productive matching i n the larger search tree a program without set of support techniques must face.  Here  also the e f f e c t s of not having a means of avoiding duplicate clause generation are shown as well as a probable difference i n programming skill. In summary, our programme has a d e f i n i t e advantage over Chang's i n respect to depth of search and units generated where a proof of a shallow i n f e r e n t i a l nature e x i s t s .  I t also seems l i k e l y that with  or without set of support, either program could not prove s i g n i f i c a n t l y deeper theorems without additional techniques.  19. IV  Possible Directions  for Further Work  1.  The nature of i n f e r e n t i a l unit resolution. While incomplete as an inference  system, unit resolution appears  to admit many proofs which are i n f e r e n t i a l i n nature.  That i s ,  a consequent of the axioms c o n f l i c t s with the negation of the theorem. I t i s perhaps possible that a program could be developed to choose such proof circumstances and, using a form of backtracking from the negation of the proposed theorem, construct development by regular unit resolution. points  possible proof trees f o r  In short this sort of idea  to the development of a "measure of complexity" for resolution  proofs. 2.  H e u r i s t i c Tree Search Insofar as unit resolution i s not complete, i . e . there are  possible theorems i t cannot t h e o r e t i c a l l y prove, i t can therefore be thought of as a h e u r i s t i c approach.  As Chang states " I f a  theorem, i . e . , a set of clauses, does not have an input or unit proof, we may convert i t into a theorem which has an input or [ ]. 2  unit proof by putting into i t appropriate lemmas"  . This would  c e r t a i n l y seem to be the d i r e c t i o n to follow i f i t were clear that unit resolution, as now implemented can f i n d proofs for a l l such lemmas.  Results so f a r seem to indicate this i s not the case and  that continued work on the development of stronger unit resolution procedures i s very much needed.  Most refinements to resolution have  centered on the l o g i c a l power of the technique i n order to reduce the o v e r a l l size of the search tree.  Like unit resolution i n this  system, they have generally been applied to that tree so defined  20. i n a breadth f i r s t manner, normally plowing through masses of units i n quite rote fashion.  Work with this programme has emphasised this  blindness of flow i n two respects.  F i r s t , once a clause i s retained  i t i s not evaluated f o r significance i n further proof development. Secondly, axioms are selected and used rotely without any type of dynamic choice. of  When these types of concepts are entertained, much  the theory and philosophy of tree search becomes relevant to  theorem proving.  I t i s simply a matter of saying l o g i c a l completeness  or algorithmic process i s not worth much i f the program i s not able to reach i n t e r e s t i n g l e v e l s . A couple of facts drawn from runs with this theorem prover are worthy of consideration i n developing a genuinely h e u r i s t i c theorem proving system.  The f i r s t of these i s the significance of ground  instances of l i t e r a l s or unit clauses.  Most proofs include at least  one of these i n their tree structure and hence appear to be of more than average value when generated.  The other fact i s the difference  i n time required f o r proof using varying orders of clause s e l e c t i o n . For this program using breadth f i r s t search, the times may vary as much as the t o t a l processing time f o r the deepest l e v e l required. Obviously even a s l i g h t amount of s e l e c t i v e l y or dynamic clause ordering would reduce the mean time f o r such proofs. 3.  Concluding Remarks The o r i g i n a l intent of this work was twofold.  F i r s t to provide  a form of theorem proving system f o r further work and secondly to try  the "hyper" unit resolution technique described i n Chapter I. It seems clear now that the "further work" which motivated  this project w i l l involve some major changes to the theorem prover  21. i t s e l f as i t s potential f o r " i n t e r e s t i n g " results i s l i m i t e d . The "hyper" unit resolution strategy  seems to b o i l down to a method  of description of i n t e r n a l workings of the program rather than an advancement as a natural approach. with respect  I f the problems i t e n t a i l s  to the i n t e r n a l ordering  and construction  of l i s t s  can be reduced i t seems as good as any other unit resolution approach. F i n a l l y insofar as i t i s r e l a t i v e l y uncluttered  i n concept, unit  resolution should perhaps be given more time and e f f o r t than i t : appears to have received.  I f the problems of resolution theorem  proving are to be solved i t seems wise to work on the simpler case first.  Bibliography  22.  1.  Carson, D., Robinson, G., and Wos, L., The unit preference strategy i n theorem proving, Proceedings, 1964 F a l l Joint Computer Conference, 615-621, Spartan Press, 1964.  2.  Chang, C L . , The unit proof and the input proof i n Theorem Proving. J.ACM 17, 4 (October 1970), 698-707.  3.  Davis, M., Eliminating the i r r e l e v a n t from mechanical proofs, Proc. Symp. App. Math XV, 1963, pp. 15-30.  4.  Lehmer, D.H., The machine tools of Combinatorics, i n Applied Combinatorial Mathematics, E.F. Beckinbach, ed., Wiley, New York, 1964, pp. 17-18.  5.  McCarthy, J . , et. a l . , LISP 1.5 Programmer's Manual, MIT Press, Cambridge, Mass., 1962.  6.  Meltzer, B., Prolegomena to a theory of e f f i c i e n c y of proof procedures, A r t i f i c i a l Intelligence and Heuristic Programming, N.V. Findler, B. Meltzer, eds., American E l s e v i e r , N.Y., 1971.  7.  Morris, J.B., E resolution; extension of resolution to include the equality r e l a t i o n . , Proceedings Int. Joint Conference on A r t i f i c i a l Intelligence, Wash. D.C, May 7-9, 1969.  8.  Nilsson, N.J., Problem Solving Methods i n A r t i f i c i a l Intelligence , McGraw-Hill, 1971.  9.  Robinson, G., and Wos, L., Paramodulation and theorem proving i n f i r s t order theories with equality, i n Machine Intelligence IV, Meltzer and Michie, eds. , Edinburgh University Press, 1969.  10.  Robinson, J.A., A machine oriented l o g i c based on the resolution p r i n c i p l e , J.ACM, 12, 1 (Jan. 1965), 23-41.  11.  Weissman, C , LISP 1.5 Primer, Dickenson Publishing Company, 1967.  23. Appendix 1 An example of "hyper" unit resolution  We wish to prove a=d from the following axioms: a=b, b=c, c=d x=y A y=z  3  x=z  In the notation of this theorem proving system we are thus working with the unit clauses (+ E A B) , (+ E B C)(+ E C D) and the non unit clause ( ( - E x l x2) (- E x2 x3j.(+ E x l x3)) If we apply regular unit resolution the following clauses are generated: ((- E B x3) (+ E A x3)) ((-EC  x3)(+ E B x3))  ( ( - E D x3) (+ E C x3)) 1st l e v e l resolvents ((- E x l A)(+ E x l B)) ( ( - E x l B) (+ E x l C)) ((- E x l C) (+ E x l D)) (+ E A C) 2nd l e v e l resolvents (+ E B D) ((-EC  x3)(+ E A x3))  ((- E B x3)(+ E D x3)) ( ( - E x l A)(+ E x l C))  3rd l e v e l resolvents  ( ( - E x l B) (+ E x l D)) (+ E A D) In short, twelve clauses were generated and retained before the clause desired appeared.  24.. Using "hyper" unit resolution, we  take our three i n i t i a l  p o s i t i v e units i n pairs and try to match them with the two l i t e r a l s of the non-unit clause. ((+ E A B)(+ E B C)) and the p a i r of resolvents  negative  The only two pairs which work are  ((+ E B C)(+ E C D)) which i n turn produce  (+ E A C) and  (+ E B D).  Hence for the next l e v e l of clause use we have f i v e unit From these f i v e units only two pairs ((+ E A B)(+ E B D)) ((+ E A C)(+ E C D)) w i l l produce a unit resolvent clause.  clauses.  and  from our non-unit  (Repeated matchings from e a r l i e r levels are not used.)  both cases the unit r e s u l t i s (+ E A D) which i s the desired  clause  i n this proof. The important difference i n these two methods i s c l e a r l y i l l u s t r a t e d ; the regular unit proof must retain 12 clauses before the desired result i s found whereas the "hyper" unit resolution technique needs to hold only 2 intermediate r e s u l t s .  In  Appendix 2 Flow of AL0NZ0I  ENTRY Generate initial unit l i s t  t Check each unit which has been generated f o r Function Depth Subsumption and contradition with other units. Save remaining units  y  Return T and the contradictory units to UPR00F  Generate a new l i s t of units Return units generated to UPR00F  26.  CLAUSE-<-SLCSET(CP) CP^CP + 1  Enter u n i f i c a t i o n and substitution procedure  Rotate the clause  P r i n t clause, unit l i s t and resultant unit.  Save the resultant unit  CP - position i n set of clauses of the same length. SLCSET - set of clauses of the same length. CLAUSE - a p a r t i c u l a r clause from SLCSET.  Appendix 3  •27.  Flow of UPR00F  ENTRY Set SLCSET to I entry of CLAUSES t n  IH-I  DEPTH set to DEPTH -1  +  1  Print SLCSET LEVEL and new units  X C a l l AL0NZ0I  RETURN 0  Set LEVEL to LEVEL+1 >  '•SI  from two levels above current to UNITSET  Save previous l e v e l ' s generated units  Screen out subsumed units i n those generated at this l e v e l  Save r e maining units  28. Appendix 4 Use of the Programme on the U.B.C. M.T.S.  System  Because of the somewhat awkward method of compilation used by USP 1) 2) 3) 4) 5) 6) 7) 8)  1.5 the following job set up must be used to run the program. $SIG <ID> T= , etc. PW $R LISP:LISP.-SCARDS=*SOURCE* 0PEN(THRM:UTP SYSFILE INPUT) RE S T0RE(THRM:UTP) CL0SE(THRM:UTP) UPR00F (<args as given i n Chapter II>) MTS() $SIG  1)  signon card  allow enough time and pages (program i s somewhat verbose to say the l e a s t ) .  2)  run card  note that the program does not use the regular LISP 1/5 system (for reasons of data c e l l space required).  3)  0PEN  opens the data c e l l f i l e containing the compiled theorem prover.  4)  REST0RE  reads the compiled program into the LISP  5)  CL0SE  closes the source f i l e - must be included.  6)  UPR00F  statement to c a l l the program exactly as outlined i n Chapter I I . , Can be several cards but don't use past column 72.  7)  MTSQ  this c a l l returns control to MTS. i s a n i l argument.  8)  signdff  system.  Note that there  The f i l e THRM:UTP i s marked public and takes approximately 3 seconds to restore. F i n a l l y , check input to UPR00F carefully before attempting a long run.  LISP i s not the cheapest way to f l y .  Appendix 5  1.  29.  S0URCE C0DE The f u n c t i o n s AL0NZ0I and UPR00F and t h e i r s u p p o r t i n g f u n c t i o n s .  >DEFI N E C ( ( N E W U C H K (LAMBDAC CTRL N I S ) > ( C 0 N D ( ( N U L L C T R L ) N I L ) ( ( M E M B E R (CAR C T R L ) N I S ) T ) X T (NEWUCHK (CDR C T R L ) N I S ) ) )))))))))))) > D E F I N E ( ( ( S U B S (LAMBDA (S S T R I N G ) XPROGO >S2 ( C O N D U N U L L S) (RETURN S T R I N G ) ) ) X S E T Q S T R I N G ( A T O M S U B S T ( C A A R S ) (CADAR S " S T R I N G ) ) X S E T Q S (CDR S ) ) XGO S2)))))))))))) >DEFINE(((FETCH (LAMBDA ( J L I S T ) X C O N D U N U L L LI S T ) N I L ) ( ( E Q U A L J 1 ) ( C A R L I S T ) ) X T (FETCH (SUB1 J M C D R L I S T ) ) ) ) ) ) ) ) ) ) ) ) ) >DEFINE(((REPLACE(LAMBDA(J B LIST) XPROG(TEMPl) >Al(COND((EQUAL J l ) ( G O END))) X S E T Q T E M P I (APPEND1 T E M P I (CAR L I S T ) ) ) X S E T Q L I S T (CDR L I S T ) ) X S E T Q J (SUB1 J ) ) (GO A l ) >END ( R E T U R N (NCONC T E M P I ( R P L A C A L I S T B ) ) ) ) ) ) ) ) ) ) >DEFINE ( ( ( C O N T R A (LAMBDA ( U N I T U L I S T ) XPROG (X) >L1 ( C O N D ( ( N U L L U L I S T ) ( R E T U R N N I L ) ) ) X S E T Q X (CAR U L I S T ) ) X C 0 N D ( ( A N D ( N U L L ( E Q ( C A R U N I T ) ( C A R X ) ) ) ( E Q (CADR U N I T ) ( C A D R X ) ) ) >(C0ND((SIGMA(CDDR UNIT)(CDDR X))(RETURN X ) ) ( T NIL)))) X S E T Q U L I S T (CDR U L I S T ) ) (GO L l ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) > D E F I N E ( ( ( A L O N Z O K L A M B D A ( S L C S E T U N I T S E T NEWU FD ES EQS F S ) X P R O G ( F I R S T COUNTER L N L I S T J X R E S U L T S Y COUNT ANS CTEMP UTEMP S >CLAUSE C P C L A U S E 1 U L I S T 1 UT1 E L E NC V I V2 CTRL N I S K) X C O N D U N U L L EQSMGO A B B ) ) ) X S D T Q ANS (NCONC ANS (EQGEN NEWU U N I T S E T ) ) ) X C O N D ( F S ( S E T Q ANS (NCONC ANS (EQGEN U N I T S E T N I L ) ) ) ) ) X P R I N T (QUOTE $ $ ' U N I T S GENERATED BY I M P L I C I T E Q U A L I T Y RELATIONS')) X P R I N T ANS) >ABC ( S E T Q NC ( L E N G T H S L C S E T ) ) X S E T Q L ( S U B 1 ( L E N G T H (CAR S L C S E T ) ) ) ) >LAB1 ( S E T Q F I R S T ( F E T C H 1 U N I T S E T ) ) X S E T Q COUNTER L ) >L1 ( S E T Q N L I S T ( A P P E N D 1 N L I S T (STAND F I R S S ) ) ) X S E T Q C T R L ( A P P E N D 1 C T R L (QUOTE 1 ) ) ) X S E T Q COUNTER ( S U B 1 COUNTER) ) X C O N D C ( G R E A T E R P COUNTER 0 ) ( G O L l ) ) ) X C O N D ( ( N U L L NEWU) (GO Z2 ) ) ) X S E T Q COUNTER (ADD1 ( L E N G T H U N I T S E T ) ) ) X S E T Q U N I T S E T ( A P P E N D U N I T S E T NEWU)) >Z1 ( S E T Q N I S ( A P P E N D 1 N I S C O U N T E R ) ) #  J U X S E T Q COUNTER ( A D D 1 C O U N T E R ) ) * > ( C O N D ( ( G R E A T E R P COUNTER ( L E N G T H U N I T S E T ) ) ( G O Z 2 ) ) (T (GO ZD)) >Z2 ( S E T Q K ( L E N G T H UNITSET)) >L2 ( C O N D ( ( N U L L NEWU) (GO P A S T ) ) ) X C O N D U N U L L (NEWUCHK C T R L N I S ) ) ( G O O N ) ) ) >PAST ( S E T Q CP 1 ) >CF (COND ( ( G R E A T E R P CP N C X G O O U T ) ) ) X S E T Q C L A U S E ( F E T C H CP S L C S E T ) ) X S E T Q CP ( A D D 1 C P ) ) X S E T Q COUNT ( A D D 1 L ) ) >L00(SETQ ULIST1 NLIST) X S E T Q CLAUSE1 CLAUSE) > L 1 0 0 ( C O N D ( ( E Q (CAAR U L I S T 1 M C A A R C L A U S E D X G O LM))) > ( C O N D ( ( N O T ( E Q (CADAR UL I S T 1 ) (CADAR C L A U S E D ) ) (GO Lkk))) X S E T Q U L I S T 1 (CDR U L I S T D ) X S E T Q C L A U S E 1 (CDR C L A U S E D ) XCOND((NULL ULISTD(GO L22))) X G O LlOO) >lkk ( S E T Q COUNT ( S U B 1 C O U N T ) ) X S E T Q C L A U S E ( A P P E N D (CDR C L A U S E X L I S T ( C A R C L A U S E ) ) ) ) > ( C O N D ( ( E Q U A L COUNT 0 ) ( G O C F ) ) ) X G O LOO) >L22 ( S E T Q CTEMP C L A U S E X S E T Q UTEMP N L I S S ) > L 7 7 ( S E T Q S ( S I G M A (CDDAR C T E M P ) ( C D D A R U T E M P ) ) ) X C O N D ( S (GO L 3 3 ) ) ( T (GO Lkh))) >L33 (COND ( ( E Q U A L S T ) ( G O L 5 5 ) ) ) X S E T Q CTEMP ( S U B S S C T E M P ) ) > L 5 5 ( C O N D ( ( E Q U A L (CDR U T E M P ) N I L X G O L 6 6 ) ) ) X S E T Q CTEMP (CDR C T E M P ) ) ( S E T Q UTEMP (CDR U T E M P ) ) XGO L77) > L 6 6 ( P R I N T (QUOTE $ $ ' C L A U S E U S E D ' ) ) ( P R I N T C L A U S E ) X P R I N T (QUOTE $ $ ' U N I T S U S E D ' ) ) ( P R I N T N L I S T ) > ( P R I N T ( Q U O T E $ $ ' R E S U L T A N T U N I T C L A U S E 1 ) ) ( P R I N T (CADR C T E M P ) ) X S E T Q ANS ( A P P E N D 1 ANS ( S T A N D (CADR C T E M P ) ) ) ) ( G O lkk) >OUT(COND((NULL ANS)(GO O N ) ) ) X S E T Q V2 ( A P P E N D U N I T S E T R E S U L T S ) ) X S E T Q V I (CAR A N S ) ) X C O N D U F D C H K (CDDR V I ) F D ) ( G O B Y ) ) ) X C O N D U N U L L ES)(GO L 5 0 0 ) ) ) X C O N D ( ( N O T ( E Q (CADR V l ) ( Q U O T E E ) ) ) ( G O L 5 0 0 ) ) ) > ( C O N D ( ( E Q (CAR V l ) ( Q U O T E - ) ) ( G O ED)) XCOND((SIGMA (LIST(CADDR V1))(CDDDR V l ) ) ( G O B Y ) ) ) X G O L500) >E1 ( C O N D ( ( S I G M A ( L I S T ( C A D D R V I ) ) ( C D D D R V I ) ) X R E T U R N ( A P P E N D 1 ( L I S T T ( L I S T (QUOTE + H Q U O T E E X Q U O T E X ) XQUOTE X)))V1>)>) >L500(COND((NOT(EQ(CADR V1)(CADAR V 2 ) ) ) ( G O L 5 0 D ) >((EQ(CAR V I ) ( C A A R V 2 ) ) ( G O L 5 0 2 ) ) ) > ( C O N D ( ( S I G M A (CDDR V 1 ) ( C D D A R V 2 ) ) X R E T U R N ( A P P E N D 1 ( L I S T T (CAR V 2 ) ) V I ) ) ) ) X G O L501) >L502 ( S E T Q Y ( S I G M A (CDDAR V 2 X C D D R V D ) ) X C O N D ( Y (GO L 6 0 D X T (GO L 5 0 1 ) ) ) > L 6 0 1 ( C O N D ( ( E Q U A L Y T ) (GO B Z ) ) )  #  > L 6 0 1 ( C O N D ( ( E Q U A L Y T ) (GO B Y ) ) ) >L506 (COND((NOT(ATVAROF (CADAR Y)(CDDAR U 2 ) ) ) ( G 0 L 5 0 1 ) ) ) X C O N D U N U L L (CDR Y ) ) (GO B Y ) ) ) X S E T Q Y (CDR Y ) ) ( G O L 5 0 6 ) > L 5 0 1 ( S E T Q V2 (CDR V 2 ) ) X C 0 N D ( V 2 (GO L 5 0 0 ) ) ) >X1(SETQ RESULTS (APPEND1 RESULTS (CAR A N S ) ) ) >BY ( S E T Q ANS (CDR A N S ) ) (GO OUT) >0N ( S E T Q J 1 ) >LU ( S E T Q E L E (ADD1 ( F E T C H J C T R L ) ) ) X C O N D ( (GREATERP ELE K ) ( G O L 3 ) ) ) X S E T Q X (STAND (FETCH ELE U N I T S E T ) ) ) X S D T Q NLIST (REPLACE J X N L I S T ) ) X S E T Q CTRL ( R E P L A C E J ELE C T R L ) ) X C O N D U E Q U A L J 1 ) (GO L 2 ) ) ) X S E T Q COUNTER ( S U B 1 J ) ) >L5 ( S E T Q N L I S T ( R E P L A C E COUNTER ( S T A N D F I R S T ) N L I S T ) ) X S E T Q C T R L ( R E P L A C E COUNTER (QUOTE 1 ) C T R L ) ) X S E T Q COUNTER ( S U B 1 C O U N T E R ) ) X C O N D ( ( G R E A T E R P COUNTER 0 ) ( G O L 5 ) ) ) X G O L2) >L3 ( S E T Q J ( A D D 1 J ) ) X C O N D ( ( L E S S P J L ) ( G O Ik)) X ( E Q U A L J L ) ( G 0 Lk))) XRETURN R E S U L T S ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) > D E F I N E ( ( ( U P R O O F ( L A M B D A ( C L A U S E S U N I T S E T D E P T H FD E S ) X P R O G ( I S L C S E T A NEW NU V A l L E V E L EQS F S " X S E T Q LEVEL 1) X C O N D ( E S ( S E T Q EQS T ) ) ) X S E T Q FS T ) >SETCC ( S E T Q I 1 ) >GETC ( S E T Q S L C S E T ( F E T C H I C L A U S E S ) ) X S E T Q I (ADD1 I ) ) X C O N D C S L C S E T (GO O N ) ) ) X S E T Q DEPTH ( S U B 1 D E P T H ) ) X C O N D ( ( E Q U A L DEPTH 0 ) (RETURN 0 ) ) ) X S E T Q L E V E L (ADD1 L E V E L ) ) XCONDUNULL ESXGO AA))) X S E T Q EQS T ) >AA ( S E T Q U N I T S E T (NCONC U N I T S E T N U ) ) > S L 1 ( S E T Q I (LENGTH NEW)) X C O N D U L E S S P I 2)(GO SL2 ) ) ) > S L U ( C O N D ( ( S U B S U M E D ( C A R N E W H C D R N E W ) ) ( G O S L3 ) ) ) X S E T Q NEW ( A P P E N D (CDR N E W H L I S T (CAR N E W ) ) ) ) X S E T Q I (SUB1 I ) ) X C O N D U E Q U A L I 0)(GO SL2 ) )) X G O SLk) >SL3 ( S E T Q NEW (CDR N E W ) ) ( G O S L 1 ) >SL2 ( S E T Q NU NEW) X C O N D ( ( N U L L NU) ( R E T U R N 1 ) ) ) X S E T Q NEW N I L ) (GO S E T C C ) > O N ( P R I N T (QUOTE $ $ ' L E V E L OF C L A U S E U S E ' ) ) X P R I NT L E V E L ) X P R L T (QUOTE C L A U S E S ) ) X P R I N T SLCSET) > ( P R I N T ( Q U O T E $ $ ' N E W U N I T S FROM P R E V I O U S L E V E L 1 ) ) X P R I N T NU) X S E T Q A ( A L O N Z O l S L C S E T U N I T S E T NU FD ES EQS F S ) ) X S E T Q EQS NI L ) ( S E T Q FS N I L ) > ( C O N D ( A (GO T E S T ) ) ( T ( G O G E T C ) ) )  > ( C O N D ( A (GO T E S T ) ) ( T ( G O GETC))) >TEST(COND((NULL(EQUAL (CAR A) T ) ) ( G O B l ) ) ) X P R I N T (QUOTE $ $ ' P R O O F FOUND FOR T H I S T H E O R M 1 ) ) X P R I N T (CADR A ) ) X P R I N T (QUOTE $$ ' CONTRAD I CTS 1 ) ) X P R I N T (CADDR A ) ) ( R E T U R N T ) >B1 ( S E T Q A l A ) >B2 ( S E T Q V (CONTRA (CAR A ) N E W ) ) X C O N D ( V (GO E N D 1 ) ) ) X S E T Q A (CDR A ) ) X C O N D ( A (GO B 2 ) ) ) X S E T Q NEW (NCONC NEW A D ) X G O GETC) >END1 ( P R I N T T ) ( P R I N T V ) ( P R I N T (CAR A ) ) XRETURN T)))))))))))))))) > D E F I N E ( ( ( T A (LAMBDA (ARG) X C O N D U N U L L ARG) 0 ) ( ( A T O M ARG) 0 ) X T ( M A X ( A D D 1 ( T A ( C A R A R G ) ) ) ( T A (CDR A R G ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) > D E F L E ( ( ( F D C H K ( L A M B D A (ARG F D ) X P R O G (A) > L 1 ( S E T Q A (CAR A R G ) ) X C O N D ( ( G R E A T E R P (TA A ) FD)(RETURN T ) ) ) X S E T Q ARG (CDR A R G ) ) X C O N D U N U L L A R G ) ( R E T U R N N I L ) ) ( T (GO L l ) ) ) ) ) ) ) ) ) ) ) ) ) ) >DEFINE(((SUBSUMED(LAMBDA(U UL) X P R O G ( S I G N SYMB S V A R L I S T 1 V A R L I S T 2 ) X S E T Q S I G N (CAR U ) ) ( S E T Q SYMB (CADR U ) ) X S E T Q V A R L I S T 1 (CDDR U ) ) >CHECK ( C O N D ( ( A N D ( E Q S I G N (CAAR U L ) ) ( E Q SYMB (CADAR U L ) ) ) X S E T Q V A R L I S T 2 (CDDAR U L ) ) ) X T (GO NEXTUN I T ) ) ) X S E T Q S (SIGMA VARLIST2 V A R L I S T D ) >(COND((NULL S X G O NEXTUNIT)) > ( ( E Q U A L S T ) ( R E T U R N (CAR U L ) ) ) ) >TEST ( C O N D U N O T ( A T V A R O F (CADAR S ) V A R L I S S 2 ) ) > (GO N E X T U N I T ) ) ) X S E T Q S (CDR S ) ) >(COND( S (GO T E S T ) ) ( T (RETURN (CAR U L ) ) ) ) >NEXTUNIT ( S E T Q UL (CDR U L ) ) X C O N D ( U L (GO C H E C K ) ) ( T ( R E T U R N NIL)))))))))))))))) #  32  2.  The U n i f i c a t i o n Routines  >DEFINE ( ( ( V A R S E T (LAMBDA ( C ) XCOND >((ATOM C) XCOND X ( E Q (CAR (EXPLODE O ) (QUOTE X ) ) ( L I S T O ) XT NIL))) X T ( A T U N I O N ( V A R S E T (CAR O ) ( V A R S E T (CDR C ) ) ) ) ) ) ) ) ) > D E F I N E ( ( ( A T U N I ON (LAMBDA ( A B ) XCOND X C N U L L A) B) X ( A T M E M B D R ( C A R A ) B ) ( A T U N I O N (CDR A ) B ) ) X T (CONS (CAR A ) ( U N I O N (CDR A ) B ) ) ) ) ) ) ) ) > D E F L E ( ( ( A T M E M B D R ( L A M B D A ( A B) XCOND X ( N U L L B) N I L ) > ( ( E Q A (CAR B ) ) T ) X T (ATMEMBER A (CDR B 1 1 ) ) ) ) ) ) ) >DEFINE(((STAND (LAMBDA ( C ) XPROG (A) X S E T Q A (VARSET O ) >TAG (COND X ( N U L L A) ( R E T U R N C ) ) ) X S E T Q C ( A T O M S U B S T (GENSYM1 (QUOTE X ) ) (CAR A ) O ) X S E T Q A (CDR A ) ) XGO TAG)))))) >DEFIL E ( ( ( S I G M A ( L A M B D A ( C D) X P R O G (L A B) X S E T Q L NIL) >L1 ( S E T Q A ( C A R C>) X S E T Q B (CAR D ) ) XCOND > ( ( A T O M A ) (GO U O ) X ( A T O M B) (GO L 5 ) ) X C N O T ( E Q (CAR A ) (CAR B ) ) ) ( R E T U R N N I L ) ) ) X S E T Q C (NCONC (CDR A ) (CDR C ) ) ) X S E T Q D (NCONC (CDR B ) (CDR D ) ) ) XGO Ll) >lh (COND X ( E Q ( C A R ( E X P L O D E A ) ) (QUOTE X ) ) (GO L 6 ) ) > ( ( N O T (ATOM B ) ) ( R E T U R N N I L ) ) > ( ( E Q (CAR ( E X P L O D E B ) ) (QUOTE X ) ) (GO L 3 ) ) >((NOT (EQ A B ) ) (RETURN N I L ) ) ) >L7 ( S E T Q C (CDR O ) X S E T Q D (CDR D ) ) X G O L2) >L5 (COND > ( ( N O T ( E Q (CAR ( E X P L O D E B ) ) (QUOTE X ) ) ) ( R E T U R N N I L ) ) X ( A T V A R O F B A ) (RETURN N I L ) ) ) X G O L3) >L6 (COND ( ( E Q A B " (GO L 7 ) ) #  34. >((ATVAROF A B " (RETURN N I L ) ) ) X S E T Q L (APPEND1 L ( L I S T B A ) ) ) X S E T Q C ( A T O M S U B S T B A (CDR C ) ) ) X S E T Q D ( A T O M S U B S T B A (CDR D ) ) ) >L2 (COND >((NOT (NULL O ) (GO L l ) ) > ( ( N U L L L) (RETURN T ) ) ) >(RETURN L ) >L3 ( S E T Q L ( A P P E N D 1 L ( L I S T A B ) ) ) X S D T Q C ( A T O M S U B S T A B (CDR C ) ) ) X S E T Q D (ATOMSUBSS A B (CDR D ) ) ) XGO L2)))))) > D E F I N E ( ( ( U N I O N (LAMBDA (X Y ) X C O N D ( ( N U L L X ) Y ) ( ( M E M B E R (CAR X ) Y ) ( U N I O N (CDR X ) Y ) ) X T (CONS ( C A R X ) ( U N I O N (CDR X ) Y ) ) ) ) ) ) ) ) > D E F I N E ( ( ( E F F A C E (LAMBDA (A X ) XCOND X C N U L L X) N I L ) X ( E Q U A L A (CAR X ) ) (CDR X ) ) X T (CONS ( C A R X ) ( E F F A C E A (CDR X ) ) ) ) ) ) ) ) ) > D E F I N E ( ( ( S U B S T ( L A M B D A (X Y Z ) XCOND >((EQUAL Y Z) X) X ( A T O M Z) Z) X T (CONS ( S U B S T X Y ( C A R Z ) ) ( S U B S T X Y (CDR Z ) ) ) ) ) ) ) ) ) > D E F I N E ( ( ( S T R I N G S U B (LAMBDA ( S T V Z ) XCOND X C A T O M Z) Z) X ( E Q V (CAR Z ) ) ( A P P E N D ST ( S T R I N G S U B ST V (CDR Z ) ) ) ) X T (CONS ( S T R I N G S U B S T V ( C A R Z ) ) ( S T R I N G S U B ST V (CDR Z ) ) ) ) ) ) ) ) ) > D E F I N E ( ( ( A T O M S U B S T ( L A M B D A (X A Z ) XCOND X ( E Q A Z) X) X C A T O M Z) Z) X T (CONS ( A T O M S U B S T X A (CAR Z ) ) X A T O M S U B S T X A (CDR Z ) ) ) ) ) ) ) ) ) >DEFINE(((ATVAROF (LAMBDA ( A Y ) XCOND X ( A T O M Y ) (COND X ( E Q A Y) T) XT NIL))) X T (OR ( A T V A R O F A ( C A R Y ) ) ( A T V A R O F A (CDR Y ) ) ) ) ) ) ) ) ) #  35. 3.  The function EQGEN and supporting  routines.  > D E F I N E ( ( ( E Q G E N ( L A M B D A ( N U OU) X P R O G (NEW OLD P I P2 P3 NEU OEU RL F L A G 1 ) X S E T Q NEU ( S T R A I N N U ) ) ( S E T Q OEU ( S S R A I N O U ) ) X C O N D U N U L L NEU ) ( R E T U R N N I L ) ) > ((NULL OEUKGO NONLY))) X S E T Q NEW NEU) ( S E T Q OLD OEU) >SU ( S E T Q P I ( C A R N E W ) ) ( S E T Q P2 (CAR O L D ) ) >FSP ( C O N D ( ( A N D ( E Q (CAR P I ) P L U S S ) ( E Q (CAR P 2 ) P L U S S ) ) > (GO P P ) ) > ( ( A N D ( E Q ( C A R P I ) D A S H ) ( E Q (CAR P 2 ) P L U S S ) ) > (GO N P ) ) > ( ( A N D ( E Q ( C A R P I ) P L U S S ) ( E Q (CAR P 2 ) D A S H ) ) > (GO P N ) ) > ( T (GO C U ) ) ) >PP ( S E T Q P3 ( T R A N S 1 P I P 2 ) ) (GO S A ) >NP ( S E T Q P3 ( T R A N S 2 P I P 2 ) ) (GO S A ) >PN ( S E T Q P3 ( T R A N S 3 P I P 2 ) ) (GO S A ) >SA ( C O N D ( P 3 ( S E T Q RL ( A P P E N D 1 RL ( S T A N D P 3 ) ) ) ) ) XC0ND(FLAG1(G0 CU))) X S E T Q F L A G 1 T ) ( S E T Q P3 P 2 X S E T Q P2 P 1 ) ( S E T Q P I P 3 M G O F S P ) >CU ( S E T Q F L A G 1 N I L ) ( S E T Q OLD (CDR O L D ) ) > ( C O N D ( ( N U L L O L D X G O C N U ) ) ( T (GO S U ) ) ) >CNU ( S E T Q NEW (CDR N E W ) ) > ( C O N D ( ( N U L L NEW)(GO N O N L Y ) ) ) > ( S E T Q OLD O E U K G O S U ) >NONLY ( S E T Q RL (NCONC RL ( R E F L E X N E U ) ) ) > ( S E T Q RL (NCONC RL ( T R A N S N N E U ) ) ) XRETURN R L ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) > D E F I N E ( ( ( T R A N S ( L A M B D A (N P I P 2 ) X P R O G ( T l T 2 T 3 Tk S R ) X S E T Q T l (CADDR P 1 ) ) ( S E T Q T 2 ( C A R (CDDDR P I ) ) ) X S E T Q T3 (CADDR P 2 ) ) ( S E T Q T l * ( C A R (CDDDR P 2 ) ) ) XCONDUEQUAL N l)(GO PP)) > ((EQUAL N 2 X G O N P ) ) > ( T (GO P N ) ) ) > P P ( S E T Q S ( S I G M A ( L I S T T2 (QUOTE X 3 ) ) > ( L I S T T3 Tk))) X C O N D U N U L L S ) (RETURN N I L ) ) > ((EQUAL S T)(RETURN > ( L I S T P L U S S (QUOTE E ) T l 7k))) > ( T ( R E T U R N ( A P P E N D ( L I S T (QUOTE + X Q U O T E E ) ) > ( S U B S S ( L I S T T l (QUOTE X 3 ) ) ) ) ) ) ) >PN ( S E T Q S ( S I G M A ( L I S T (QUOTE X I ) T 2 X L I S T T3 Tk))) X C O N D ( ( N U L L S ) (RETURN N I L ) ) > ( ( E Q U A L S T ) ( R E T U R N ( L I S T P L U S S (QUOTE E ) T3 T l ) ) ) > ( T ( R E T U R N ( A P P E N D ( L I S S DASH (QUOTE E ) ) > ( S U B S S ( L I S T (QUOTE X I ) T l ) ) ) ) ) ) >NP ( S E T Q S ( S I G M A ( L I S T T l (QUOTE X 2 ) ) > ( L I S T T3 Tk))) X C O N D U N U L L S) (RETURN N I L ) ) #  36. > ( ( E Q U A L S T ) ( R E T U R N ( L I S T DASH (QUOTE E ) Tk T 2 ) ) ) > ( T ( R E T U R N ( A P P E N D ( L I S T DASH (QUOTE E ) ) > ( S U B S S ( L I S T (QUOTE X 2 ) T 2 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) > D E F I N E ( ( ( R E F L E X (LAMBDA ( N U ) X P R O G ( L I A U) X S E T Q L (LENGTH N U ) ) ( S E T Q I 1) >L1 ( S E T Q U (CAR N U ) ) X S E T Q A ( A P P E N D 1 A ( S T A N D ( L I S T (CAR U M Q U O T E E ) X C A R (CDDDR U ) ) ( C A D D R U ) ) ) ) ) X S E T Q I (ADD1 I ) ) >(COND((GREATERP I L)(RETURN A ) ) ) X S E T Q NU (CDR N U ) ) ( G O L l ) ) ) ) ) ) ) ) ) ) > D E F I N E ( ( ( T R A N S N (LAMBDA ( N U ) X P R O G ( A PCDR P l P2 P3 I R F L A G ) . >L1 ( S E T Q P l ( C A R N U ) ) ( S E T Q PCDR (CDR N U ) ) X C O N D U N U L L PCDR) ( R E T U R N A ) ) ) >L2 ( S E T Q P2 ( C A R P C D R ) ) >LO (COND( (AND ( E Q (CAR P l ) P L U S S X E Q (CAR P 2 ) P L U S S ) ) XSETQ I 1)) > ( ( A N D ( E Q (CAR P l ) D A S H ) ( E Q ( C A R P 2 ) P L U S S ) ) XSETQ I 2)) > ( ( A N D ( E Q (CAR P l ) P L U S S M ( E Q ( C A R P 2 ) DASH ) ) XSETQ I 3)) X T (GO L 3 ) ) ) X S E T Q R (TRANS I P l P 2 ) ) >(COND(R ( S E T Q A ( A P P E N D 1 A ( S T A N D R ) ) ) ) ) >L3 ( C O N D ( F L A G (GO Lk))) X S E T Q P3 P 2 ) ( S E T Q P2 P 1 ) ( S E T Q P l P 3 ) ( S E T Q F L A G T ) ( G O L O ) > L U ( S E T Q FLAG N I L ) X S E T Q P l P2) X S E T Q PCDR (CDR P C D R ) ) >(COND(PCDR (GO L 2 ) ) ) X S E T Q NU (CDR N U ) ) (GO L l ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) > D E F I N E C ( ( S T R A I N (LAMBDA ( N U ) X P R O G (UL X) >A ( C O N D ( ( N U L L N U ) ( R E T U R N U L ) ) ) X S E T Q X (CAR N U ) ) X C O N D U E Q (CADR X H Q U O T E E ) ) ( S E T Q UL ( A P P E N D 1 UL X ) ) )) X S E T Q NU (CDR N U ) ) XGO A ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) #  Appendix 6 A run of example 1 from Chang $R LISP:LISP SCARDS=*SOURCE* EXECUTION BEGINS ARGUMENTS FOR EVALQUOTE ... OPEN (UTP SYSFILE INPUT) TIME UTP  10MS,  VALUE IS ...  ARGUMENTS FOR EVALQUOTE ... RESTORE (UTP) COLLECTED 18140 CELLS AND STACK HAS TIME NIL  3259MS,  5994  UNITS LEFT.  VALUE IS ...  ARGUMENTS FOR EVALQUOTE ... UPROOF ( ( ( ( ( - P XI X2 X4) (- P X2 X3 X5) (- P XI X5 X6)(+ P X4 X3 X6)))) ((+ P (G X7 X8) X7 X8) (+ P X9 (H X9 X10) X10) (-P (K X l l ) X l l (K X l l ) ) ) " l 2 NIL) LEVEL OF CLAUSE USE 1 CLAUSES ( ( ( - P XI X2 X4) (- P X2 X3 X5) (- P XI X5 X6) '(+ P X4 X3 X6))) NEW UNITS FROM PREVIOUS LEVEL NIL CLAUSE USED ((+ P X4 X3 X6) (- P XI X2 X4) (- P X2 X3 X5) (- P XI X5 X 6 ) )  UNITS USED ( ( - P (K X0000009) X0000009 (K X0000009)) (+ P (G X0000003 X0000004) X0000003 X0000004) (+ P (G X0000005 X0000006) X0000005 X0000006)) RESULTANT UNIT CLAUSE (- P (G (G X0000005 X0000006) (K X0000005)) X0000006 (K X0000005)) CLAUSE USED ( ( - P XI X2 X4) (- P X2 X3 X5) (- P XI X5 X6) (+ P X4 X3 X6)) UNITS ((+ P (G X0000014 X0000015) X0000014 X0000015) (+ P X0000012 (H X0000012 X0000013) X0000013) (+ P (G X0000005 X0000006) X0000005 X0000006)) RESULTANT UNIT CLAUSE ( + P X0000006 (H X0000005 X0000005) X0000006) PROOF FOUND FOR THIS THEOREM (•r P (K X l l ) X l l (K.X11)) CONTRADICTS (+ P X0000017 (H X0000016 XOO00O16) X0000017) TIME T  524MS,  VALUE IS ...  

Cite

Citation Scheme:

        

Citations by CSL (citeproc-js)

Usage Statistics

Country Views Downloads
United States 7 4
China 7 5
United Kingdom 3 0
France 2 0
City Views Downloads
Ashburn 6 0
Shenzhen 6 5
Unknown 4 17
London 2 0
Beijing 1 0

{[{ mDataHeader[type] }]} {[{ month[type] }]} {[{ tData[type] }]}
Download Stats

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:
http://iiif.library.ubc.ca/presentation/dsp.831.1-0051190/manifest

Comment

Related Items