UBC Theses and Dissertations

UBC Theses Logo

UBC Theses and Dissertations

A unit resolution theorem proving system 1972

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

Item Metadata

Download

Media
UBC_1972_A6_7 L46.pdf
UBC_1972_A6_7 L46.pdf
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
Citation
1.0051190.ris

Full Text

A UNIT RESOLUTION THEOREM PROVING SYSTEM by PETER NEAVE LEQUESNE B.Sc, University of British Columbia, 1963 A THESIS SUBMITTED IN PARTIAL FULFILMENT OF THE REQUIREMENTS FOR THE DEGREE OF Master of Science in the Department of Computer Science We accept this thesis as conforming to the required standard THE UNIVERSITY OF BRITISH COLUMBIA April , 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 it 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 The University of British Columbia Vancouver 8, Canada Abstract A unit resolution theorem proving system is developed and compared with the previous work of C.L. Chang. This thesis includes a description of a particular approach to unit resolution and a description of the resulting program and i t s effectiveness. i i 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. Unification and Substitution for a Unit 4 Proof 5. Subsumption 5 6. The "hyper" Unit Resolution Strategy 5 7. Embedded Equality Axioms 7 II 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 III Evaluation of Experimental Results 16 1. Comparison with the work of Chang 16 2. Comments on the Differences in the Results 17 IV Possible Directions for Further Work 19 1. The Nature of Inferential Unit Resolution 19 2. Heuristic Tree Search 19 3. Concluding Remarks 20 Bibliography 22 Appendix 1 23 Appendix 2 25 Appendix 3 27 Appendix 4 28 i i i Appendix 5 29 Appendix 6 37 List of Tables Table 1 A Comparative Table of Chang's Exampl Acknowledgement v Most of the ideas developed in this thesis are the suggestions of Professor Raymond Reiter. I am deeply grateful for the patient assistance he has given me in completing this work. Thanks are also extended to the Department of Computer Science for a most satisfying 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 in a very large amount of matching and clause generation. Unit resolution is a means of reducing the size of such problems. This work is an implementation of a particular form of unit resolu- tion, paralleling closely that of CL. Chang [2]. This Chapter outlines the theoretical basis of the program produced and describes the notation and terminology used. A f u l l description of resolution is not attempted however unit resolution w i l l be described as a special case of the more general technique. 2. Preliminary Formulation of the Axioms and Proposed Theorem. For any resolution procedure, the axioms and proposed theorem of a given system must be expressed in a particular format for expressions of f i r s t order mathematical logic called conjunctive normal form. Procedures for converting to conjunctive normal form are given in [3] and [8]. A conjunctive normal form (cnf) has the following structure. Let C^,...,C^ be logical 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. is a conjunction of clauses. A clause is a disjunction of l i t e r a l s . 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 l i t e r a l is a logical 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 variable, a constant or a functional value where a functional value i s a functional symbol followed by a number of terms in brackets, e.g., f(t^,...,t£) for some H > 0. Consider the following examples of a) a free variable, 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 in the LISP 1.5 language the following notation is used for the date types described above 1) A free variable is designated by the letter x followed by any number, e.g. x20, xl5. 2) A constant is any other letter 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 is 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 is 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 is given in Chapter 2. Fundamental to this thesis is the concept of a unit clause. A unit clause is a clause of one l i t e r a l . 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 , is a unit clause. In practise, for example, in the context 3. of the program written, the outer set of brackets is 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 is normally sketched as an inverted binary tree whose bottom-most node is the • symbol. A unit proof is defined as a resolution proof such that for each node generated downwards in the proof tree, at least one parent node is 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 is a process combining clauses to form new clauses un t i l two clauses combine to n i l or •. In the above hypo- thetical diagram, three new unit clauses (U^, U^, U,.) and two new non-unit clauses (C^, Cj.) are generated. In each case the new clause has at least one parent which is a unit clause. Since we are describing what is really a combining process an.-advantage of unit resolution is 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 in search of a proof is 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 is dependent on the resolution of two non-unit clauses. 4. Unification and Substitution for a Unit Proof. Essentially, unification 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 in separate clauses and are associated with the same predicate symbols of differing signs. This common instance of two sets of terms is demonstrated by the generation of a substitution to be made to the two clauses in question, the result of which i s the presence of contradictory l i t e r a l s within the clauses in 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 substitution, i s the idea of a most general unifier. This notion which is developed in (10) basically means that there exists a substitution for two unifiable l i t e r a l s such that the most general common instance of the two is the result. In normal resolution systems i t is 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 unit r e s o l u t i o n has a s p e c i a l advantage. Because one of the parent clauses i n unit r e s o l u t i o n i s a unit clause, a given s u b s t i t u t i o n need only be applied to one clause (minus the resolved l i t e r a l ) . Since these substitutions are quite expensive t h i s i s a considerable advantage. 5. Subsumption Closely 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 clause M i s s a i d to be subsumed by a clause N i f there e x i s t s a s u b s t i t u t i o n 0 such that N 6 £ M. B a s i c a l l y , t h i s means whenever M i s true, N i s true and hence there i s l i t t l e value i n terms of the r e s o l u t i o n process i n keeping the subsumed clause. A check f o r subsumed clauses i n included i n t h i s theorem proving system. 6. The "hyper" Unit Resolution Strategy Consider a sequence of resolutions of the following type where a, a are unit clauses and 5, v 5L v ... v a v g i s a non-unit I n 1 2 n clause (axiom): cL v a 0 v . . . v a v 3 an 1 a a. 2 2 3 v v a 4 v v a v 3 n a n 6. In short where a l l the consequent l i t e r a l s may be matched with known unit clauses i t is possible that a new unit clause can be generated by in this case n resolutions. A necessary condition for this to occur is that the l i t e r a l s must have differing signs and matching predicate symbols with their corresponding units in {a^}. In additional each l i t e r a l / u n i t pair must unify at the appropriate stage of the overall resolution sequence. The "hyper" unit resolution strategy is simply to generate only unit resolvents in the above fashion. 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 is a unit clause, that i s , a l l l i t e r a l s appearing in a given axiom except the "target" l i t e r a l already exist 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 in the axiom. The use of this apparent restriction on clauses generated by unit resolution greatly reduces the number of clauses generated for further use in search of a contradiction. For instance (not including multiple instances of the same target l i t e r a l : which differ in their 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 in fact not a further restriction on the effectiveness of unit resolution. "A set of clauses can be proved insatisfiable 7. by unit resolution i f and only i f i t can be proved unsatisfiable by "hyper" unit resolution". Clearly, from the definition of unit resolution, any proof by regular unit resolution can be converted to a proof by "hyper" unit resolution and hence the proof is t r i v i a l . There i s significant combinatorial aspect of "hyper" resolution to be described. Consider the generation of unit resolvents from a clause C = L., v ... v L of r l i t e r a l s . There are r possible l i t e r a l s 1 r K which may become unit resolvents. These possible'"target" l i t e r a l s 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. In order to insure that a l l possible resolvents are generated at a particular level, i t is necessary to match each sequence of r - l l i t e r a l s corresponding to a particular target l i t e r a l with a l l possible l i s t s of length r - l of existing units. Since a given unit may be used more than once kfr—2 there are (r_^ ) such combinations of units. Each of these combinations may be ordered i n ( r - l ) ! ways hence for 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 results. Thus i t i s clear that while the number of retained units is significantly reduced with a "hyper" resolution approach there is no reduction apparent in the amount of matching which must take place in order to generate a particular unit clause. 7. Embedded Equality Axioms. The treatment of problems of proof generation with axiom sets expressing equality has had considerable attention in a number of papers on mechanical theorem proving [7 , 9 ] . The problem is a familiar one - only more so. Consider the following axiom (reflexive): 8. E (xl x2) => E (x2 xl) or in clausal form E (xl 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 in this clause. In consequence an abnormally 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 relatively mechanical in their effect, treating them as any other axiom unnecessarily marrs the efficiency of a theorem proving program. Such axioms may be embedded within the code of the program and thus produce much more effi c i e n t l y as required. In! light of this the axioms of r e f l e x i t i v i t y and transitivity of equality, i.e., E (xl x2) ^ E (x2-xl) and E (xl x2) A E (x2 x3) => E (xl x3) have been coded directly into this program and may be used by setting a switch variable on input. 9. II A Description of the Program and it s Use- The "hyper" unit resolution strategy described in Chapter I has been implemented as a theorem proving program written in 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 fi n a l l y a description of program output and it s interpretation. 1. Input to the Program A representation of the conjunctive normal form of a given proposed theorem and a few controlling parameters are passed to the predicate UPR00F in order to in 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 is an integer indicating the allowable number of times the CLAUSES may be used before quitting the search for a proof. FD, also an integer, indicates the maximum function depth in 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 latter three parameters have a self explanatory format as indicated in the example which follows. CLAUSES and UNITSET, however, require further description. CLAUSES has a certain amount of structure in i t s format in order to aid the search process of the program. As indicated earlier in Chapter I, a clause is represented as a l i s t of i t s 10. l i t e r a l s which in turn are l i s t s of signs, predicate symbols and variables etc. An example is ((+ P xl x2)(+ Q x l x2)(+ R x2 x3)). Given this format for a clause, CLAUSES is imply a set of clauses grouped by length. In other words, CLAUSES is a l i s t of l i s t s of clauses, each sublist containing clauses of the same length. The following is a set of four clauses so arranged: ((((+ P xl x2)(+ Q x2 x3()- R xl x2))) (((+ P x2 x3)(- Q x3 x2)(- P x3 x2)) ((- R xl x4)(+ Q x l x2)(+ P xl x2))) (((+ P xl x2)(- Rx2 xl)))) UNITSET is simply a l i s t of unit clauses. As earlier mentioned in 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 in the following example: ((+ P x l x2)(+ Q xl x3)(- R x2 x3)) A l l variables which appear in CLAUSES and UNITSET are x-standardized according to the following condition. The same variable name may appear in two or more non-unit clauses but may not appear in any unit clause. In addition those variable names occurring in a unit clause must be distinct from a l l other variable names appearing in unit clauses (as well as those appearing i n CLAUSES). This is done to avoid ambiguity in unification and substitution. In addition a l l variable names must include an integer larger than 20 to avoid conflict with internal variables in the equality processing. A complete example of a c a l l to UPR00F follows: 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 NIL) This is a formulation of example eight from Chang [2]. 2. Program Operation This program generates and tests unit clauses in a breadth f i r s t fashion using the general procedure outlined in the following steps. 7. 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 level of generation is greater than one test above units for presence of at least one unit from previous level. 4. Match UNITS against a l l clauses in SLCSET and generate any new resolvents possible. 5. Test newly generated resolvents for function depth and subsumption by other units. Is a new string 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 level for contradiction and subsumption among each other i f contradiction return T, i f no units remain return 1. 10. Has maximum depth of clause use been reached i f so return 0. 11. Update unitset with newly generated units and go to step 1. 6. Test remaining units generated for contradiction with other units already existing, i f found return T. 12. In short, this program matches every clause of length t-1 at a given level. Using clause rotation each l i t e r a l in a clause is treated as a possible unit resolvent. A simple combinatorial algorithm [4] is used to.generate l i s t s of units from the UNITSET of a given level. 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 in each l i t e r a l pair from l e f t to right. Given the success of the above test, unification and substitution 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 is exhausted or unification f a l l s . If a unit resolvent is generated i t i s tested for function depth, subsumption by existing units and for possible contradiction by resolution against one of the existing units. If i t does not contradict or f a i l the other test i t i s saved for use during the next level of resolution. There are three major sections or LISP functions in this theorem proving system. They are UPR00F, AL0NZ0I, and SIGMA. UPR00F is the overall driver of the system. It controls passage through the clauses, updates the set of units between levels of clause use, and communicates with the user. UPR00F calls 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 is 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 for sign and predicate symbol matching, controls and calls the unification and substitution functions as required, rotates clauses as needed, and performs subsumption, function depth and contradictory unit tests as needed. If a 13. contradiction is 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, is the controling LISP function for a collection of routines which perform unification ( i f possible) for a given pair of l i s t s of terms of a l i t e r a l pair. SIGMA produces a most general unifier i f unification i s possible or else returns the LISP atom NIL. In order to obtain a run which utilizes implicit 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 effective at the appropriate point in use of the clauses there are a few dynamic switch variables set in UPR00F and passed to AL0NZ0I. The function EQGEN is called by AL0NZ0I to generate new units resulting from said axioms, when such generation is signaled by UPR00F. Appendices 2 and 3 contain relatively 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 history of a unit just after i t has been generated. This history's format is as follows: 14. < parent clause or a r o t a t i o n of that clause > < the l i s t of units used to resolve against the clause above > < the unit resolvent > an example might be; CLAUSE 'USED ((- P x l x2)(- P x2 x3)(+ P x l x3)) UNITS USED ((+ P A B ) (+ P B C)) RESULTANT UNIT CLAUSE (+ P A C) Units generated by the use of i m p l i c i t e q u a l ity axioms are simply l i s t e d as such and normally are simply traced by checking with previous e x i s t i n g u n i ts. Upon the discovery of two contradictory u n i t clauses, UPR00F returns the value T. The two units which contradict are printed under the heading. PR00F F0UND F0R THIS THE0REM At this point the user may reconstruct the proof tree f o r the theorem i n question by t r a c i n g the printed h i s t o r i e s of the units i n question. Since variables are restandardized r e l a t i v e l y often within the proof generation process, the user must generally look back f o r a d i f f e r e n t instance ( i n respect of v a r i a b l e names) than the current unit being traced. Each time a new set of clauses i s passed to AL0NZ0I, the l e v e l of clause use, clauses passed, and new units from the previous l a b e l are p r i n t e d . If the program f a i l s to f i n d a proof i t w i l l be indicated by a return value of 0 or 1 or an obvious time over-run. A return value 15. of 0 indicates that a proof was not found at the maximum depth specified by the input parameter DEPTH. A return value of 1 signifies that at the last indicated level of clause use no new units were generated (or more specifically no new units were generated that passed both the subsumption and function depth tests). In the latter circumstance, i f a greater function depth does not change matters then no unit proof exists for the proposed theorem. The output format described above is motivated by two considera- tions; generation of a trace of a proof is costly and involves a considerable amount of programming and, secondly, to effectively study the possible implementation of heuristics in a theorem prover i t i s helpful to print as much as possible concerning the directions taken. A sample run is given of example 1 from Chang in Appendix 6. 16. I l l Evaluation of Experimental Results 1. Comparison with the work of Chang-- [2] Apart from his '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 Chang- EXAMPLE # UNITS CLAUSE UNITS TIME GENERATED DEPTH RETAINED (sec) 1 16 1 0 1.550 2 1 0 .524 2 109 3 3 7.510 72 2 4 28.222 3 44 3 3 3.417 14 2 3 3.821 4 32 2 2 2.650 14 1 0 2.0.51 5 21 1 0 0.667 1 1 0 0.646 6 32 2 1 2.300 74 1 0 15.267 7 58 2 5 3.566 6 1 0 5.602 8 65 ? 11 5.184 17 4 4 4.843 9 34 ? 10 4.050 15 4 9 6.640 10(a) 136 4 17 24.550 154 2 16 31.457 10(b) 59 3 6 9.367 169 2 16 37.228 10(c) 53 3 4 6.916 141 2 16 28.151 10(d) 48 3 5 7.317 167 2 16 37.055 TABLE I: A Comparative Table of Chang's Examples 17. For each entry in the table the value obtained by Chang is followed by that obtained with this system. The column headings have the following, more elaborate explanations: UNITS GENERATED - the total number of unit clauses produced before a proof was found. CLAUSE DEPTH - the number of times the set of non-unit clauses was used in order to find a proof. UNITS RETAINED - the number of generated unit clauses which were retained for use in 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 significantly fewer unit clauses than Chang's. (2) The clause depth necessary for proof for this system i s most often lower than that for Chang's. (3) Relative to the number of clauses generated, the number of clauses retained by both programmes is about the same. (4) The running times required by Chang's programme are (not withstanding differences in hardware and software) significantly lower than those required by this programme. 2. Comments on the Differences in the Results The conclusions stated here are by necessity somewhat speculative both for reasons of inadequate information about the internal 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 in deeper proofs than are necessary. In many circumstances an "inferential" proof exists at a shallower depth than one provided by set of support. The set of support programme must pass through, in general, more levels of clause use (and generate more clauses as a result) in order to find a contradiction. This fault in the set of support approach is probably not particularly significant for theorems which do not admit to a relatively simple inferential proof. It should be noted at this point that although not ex p l i c i t l y stated, Changes program is using the same basic strategy as the "hyper" unit resolution developed here. In addition, his routine includes a mechanism to avoid the generation of duplicate clauses. Point (3) is 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 effort expended on non-productive matching in the larger search tree a program without set of support techniques must face. Here also the effects of not having a means of avoiding duplicate clause generation are shown as well as a probable difference in programming s k i l l . In summary, our programme has a definite advantage over Chang's in respect to depth of search and units generated where a proof of a shallow inferential nature exists. It also seems likely that with or without set of support, either program could not prove significantly deeper theorems without additional techniques. 19. IV Possible Directions for Further Work 1. The nature of inferential unit resolution. While incomplete as an inference system, unit resolution appears to admit many proofs which are inferential in nature. That i s , a consequent of the axioms conflicts with the negation of the theorem. It 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 possible proof trees for development by regular unit resolution. In short this sort of idea points to the development of a "measure of complexity" for resolution proofs. 2. Heuristic Tree Search Insofar as unit resolution is not complete, i.e. there are possible theorems i t cannot theoretically prove, i t can therefore be thought of as a heuristic approach. As Chang states "If 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 certainly seem to be the direction to follow i f i t were clear that unit resolution, as now implemented can find proofs for a l l such lemmas. Results so far seem to indicate this i s not the case and that continued work on the development of stronger unit resolution procedures is very much needed. Most refinements to resolution have centered on the logical power of the technique i n order to reduce the overall size of the search tree. Like unit resolution in this system, they have generally been applied to that tree so defined 20. in a breadth f i r s t manner, normally plowing through masses of units in 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 is retained i t i s not evaluated for significance in further proof development. Secondly, axioms are selected and used rotely without any type of dynamic choice. When these types of concepts are entertained, much of the theory and philosophy of tree search becomes relevant to theorem proving. It is simply a matter of saying logical completeness or algorithmic process i s not worth much i f the program i s not able to reach interesting levels. A couple of facts drawn from runs with this theorem prover are worthy of consideration in developing a genuinely heuristic 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 in their tree structure and hence appear to be of more than average value when generated. The other fact i s the difference in time required for proof using varying orders of clause selection. For this program using breadth f i r s t search, the times may vary as much as the total processing time for the deepest level required. Obviously even a slight amount of selectively or dynamic clause ordering would reduce the mean time for such proofs. 3. Concluding Remarks The original intent of this work was twofold. First to provide a form of theorem proving system for 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 for "interesting" results is limited. The "hyper" unit resolution strategy seems to b o i l down to a method of description of internal workings of the program rather than an advancement as a natural approach. If the problems i t entails with respect to the internal ordering and construction of l i s t s can be reduced i t seems as good as any other unit resolution approach. Finally insofar as i t is relatively uncluttered in concept, unit resolution should perhaps be given more time and effort than i t : appears to have received. If the problems of resolution theorem proving are to be solved i t seems wise to work on the simpler case f i r s t . Bibliography 22. 1. Carson, D., Robinson, G., and Wos, L., The unit preference strategy in theorem proving, Proceedings, 1964 F a l l Joint Computer Conference, 615-621, Spartan Press, 1964. 2. Chang, CL. , The unit proof and the input proof in Theorem Proving. J.ACM 17, 4 (October 1970), 698-707. 3. Davis, M., Eliminating the irrelevant from mechanical proofs, Proc. Symp. App. Math XV, 1963, pp. 15-30. 4. Lehmer, D.H., The machine tools of Combinatorics, in 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 efficiency of proof procedures, A r t i f i c i a l Intelligence and Heuristic Programming, N.V. Findler, B. Meltzer, eds., American Elsevier, N.Y., 1971. 7. Morris, J.B., E resolution; extension of resolution to include the equality relation., 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 in A r t i f i c i a l Intelligence, McGraw-Hill, 1971. 9. Robinson, G., and Wos, L., Paramodulation and theorem proving in f i r s t order theories with equality, in Machine Intelligence IV, Meltzer and Michie, eds. , Edinburgh University Press, 1969. 10. Robinson, J.A., A machine oriented logic based on the resolution principle, 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 xl x3)) If we apply regular unit resolution the following clauses are generated: ((- E B x3) (+ E A x3)) ( ( - E C x3)(+ E B x3)) ( ( - E D x3) (+ E C x3)) 1st level resolvents ((- E xl A)(+ E xl B)) ((- E x l B) (+ E xl C)) ((- E x l C) (+ E xl D)) (+ E A C) 2nd level resolvents (+ E B D) ( ( - E C x3)(+ E A x3)) ((- E B x3)(+ E D x3)) ((- E x l A)(+ E x l C)) 3rd level 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 positive units in pairs and try to match them with the two negative l i t e r a l s of the non-unit clause. The only two pairs which work are ((+ E A B)(+ E B C)) and ((+ E B C)(+ E C D)) which in turn produce the pair of resolvents (+ E A C) and (+ E B D). Hence for the next level of clause use we have five unit clauses. From these five units only two pairs ((+ E A B)(+ E B D)) and ((+ E A C)(+ E C D)) w i l l produce a unit resolvent from our non-unit clause. (Repeated matchings from earlier levels are not used.) In both cases the unit result i s (+ E A D) which is the desired clause in this proof. The important difference in these two methods is clearly illustrated; the regular unit proof must retain 12 clauses before the desired result is found whereas the "hyper" unit resolution technique needs to hold only 2 intermediate results. Appendix 2 Flow of AL0NZ0I ENTRY Generate i n i t i a l unit l i s t Check each unit which has been generated for Function Depth Subsumption and contradition with other units. Save remaining units Return T and the contradictory units to UPR00F y t Generate a new l i s t of units Return units generated to UPR00F 26. CLAUSE-<-SLCSET(CP) CP^CP + 1 Enter unification and substitution procedure Rotate the clause Print clause, unit l i s t and resultant unit. Save the resultant unit CP - position in set of clauses of the same length. SLCSET - set of clauses of the same length. CLAUSE - a particular clause from SLCSET. Appendix 3 Flow of UPR00F •27. ENTRY Set SLCSET to I t n entry of CLAUSES IH-I + 1 DEPTH set to DEPTH -1 RETURN 0 Set LEVEL to LEVEL+1 > '•SI from two levels above current to UNITSET Save pre- vious level's generated units Print SLCSET LEVEL and new units X Call AL0NZ0I Screen out subsumed units in Save re- those maining generated at units this level 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.5 the following job set up must be used to run the program. 1) $SIG <ID> T= , etc. PW 2) $R LISP:LISP.-SCARDS=*SOURCE* 3) 0PEN(THRM:UTP SYSFILE INPUT) 4) RE S T0RE(THRM:UTP) 5) CL0SE(THRM:UTP) 6) UPR00F (<args as given in Chapter II>) 7) MTS() 8) $SIG 1) signon card 2) run card 3) 0PEN 4) REST0RE 5) CL0SE 6) UPR00F 7) MTSQ 8) signdff allow enough time and pages (program is somewhat verbose to say the least). note that the program does not use the regular LISP 1/5 system (for reasons of data c e l l space required). opens the data c e l l f i l e containing the compiled theorem prover. reads the compiled program into the LISP system. closes the source f i l e - must be included. statement to c a l l the program exactly as outlined in Chapter II., Can be several cards but don't use past column 72. this c a l l returns control to MTS. Note that there is a n i l argument. The f i l e THRM:UTP is marked public and takes approximately 3 seconds to restore. Finally, check input to UPR00F carefully before attempting a long run. LISP is not the cheapest way to f l y . Appendix 5 29. S0URCE C0DE 1. The functions AL0NZ0I and UPR00F and t h e i r supporting functions. >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 ) X P R O G O >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 (ATOMSUBST ( C A A R S ) (CADAR S " S T R I N G ) ) X S E T Q S (CDR S ) ) X G O S 2 ) ) ) ) ) ) ) ) ) ) ) ) > D E F I N E ( ( ( F E T C H (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 ( F E T C H ( S U B 1 J M C D R L I S T ) ) ) ) ) ) ) ) ) ) ) ) ) > D E F I N E ( ( ( R E P L A C E ( L A M B D A ( J B L I S T ) X P R O G ( T E M P l ) > A l ( C O N D ( ( E Q U A L J l ) ( G O E N D ) ) ) X S E T Q T E M P I ( A P P E N D 1 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 ( S U B 1 J ) ) (GO A l ) >END (RETURN (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 ) X P R O G ( X ) >L1 ( C O N D ( ( N U L L ULI 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 ) ) ) > ( C 0 N D ( ( S I G M A ( C D D R U N I T ) ( C D D R X ) ) ( R E T U R N X ) ) ( T N I L ) ) ) ) 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 CP 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 E Q S M G O 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 R E L A T I O N S ' ) ) X P R I N T A N S ) >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 CTRL ( 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 ) ) # X S E T Q COUNTER ( A D D 1 C O U N T E R ) ) J U * > ( 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 Z D ) ) >Z2 ( S E T Q K ( L E N G T H U N I T S E T ) ) >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 CTRL 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 ) ) > L 0 0 ( S E T Q U L I S T 1 N L I S T ) X S E T Q C L A U S E 1 C L A U S E ) > L 1 0 0 ( C O N D ( ( E Q ( C A A R U L I S T 1 M C A A R C L A U S E D X G O L M ) ) ) > ( 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 ) X C O N D ( ( N U L L U L I S T D ( G O L 2 2 ) ) ) X G O L l O O ) >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 (CAR 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 ) ) X G O L 7 7 ) >L66 ( 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 (STAND (CADR C T E M P ) ) ) ) ( G O lkk) > O U T ( C O N D ( ( N U L L A N S ) ( G O 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 E S ) ( G O 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 E D ) ) X C O N D ( ( S I G M A ( L I S T ( C A D D R V 1 ) ) ( C D D D R V l ) ) ( G O B Y ) ) ) X G O L 5 0 0 ) >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 ) X Q U O T E X ) ) ) V 1 > ) > ) > L 5 0 0 ( C O N D ( ( N O T ( E Q ( C A D R V 1 ) ( C A D A R V 2 ) ) ) ( G O L 5 0 D ) > ( ( E Q ( C A R 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 L 5 0 1 ) >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 ) ) ) > L 5 0 6 ( C O N D ( ( N O T ( A T V A R O F (CADAR Y ) ( C D D A R 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 ) ) ) > X 1 ( S E T Q R E S U L T S ( A P P E N D 1 R E S U L T S (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 ( ( G R E A T E R P E L E K ) ( G O L 3 ) ) ) X S E T Q X ( S T A N D ( F E T C H E L E U N I T S E T ) ) ) X S D T Q N L I S T ( R E P L A C E J X N L I S T ) ) X S E T Q CTRL ( R E P L A C E J E L E 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 (STAND 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 L 2 ) >L3 ( S E T Q J (ADD1 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))) X R E T U R N 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 DEPTH 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 L E V E L 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 ) ) X C O N D U N U L L E S X G O A A ) ) ) 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 ( L E N G T H NEW)) X C O N D U L E S S P I 2 ) ( G O S L 2 ) ) ) > S L U ( C O N D ( ( S U B S U M E D (CAR 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 ( S U B 1 I ) ) X C O N D U E Q U A L I 0 ) ( G O S L 2 ) ) ) 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 S L C S E T ) > ( 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 ) ) ) 32 >(COND(A (GO T E S T ) ) ( T ( G O G E T C ) ) ) > T E S T ( C O N D ( ( N U L L ( E Q U A L (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 ) ) (RETURN T ) >B1 ( S E T Q A l A ) >B2 ( S E T Q V (CONTRA (CAR A ) NEW)) 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 ) ) X R E T U R N T ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) > D E F I N E ( ( ( T A ( L A M B D A ( A R G ) X C O N D U N U L L A R G ) 0 ) ( ( A T O M A R G ) 0 ) X T ( M A X ( A D D 1 ( T A (CAR 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 ( C A R A R G ) ) X C O N D ( ( G R E A T E R P ( T A A ) F D ) ( R E T U R N T ) ) ) X S E T Q ARG (CDR A R G ) ) X C O N D U N U L L A R G ) (RETURN N I L ) ) ( T (GO L l ) ) ) ) ) ) ) ) ) ) ) ) ) ) > D E F I N E ( ( ( S U B S U M E D ( L A M B D A ( U U L ) 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 ( S I G M A V A R L I S T 2 V A R L I S T D ) > ( C O N D ( ( N U L L S X G O N E X T U N I T ) ) > ( ( E Q U A L S T ) ( R E T U R N ( C A R 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 (RETURN N I L ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) # 2. The Unification Routines >DEFINE ( ( ( V A R S E T (LAMBDA ( C ) X C O N D > ( ( A T O M C ) X C O N D X ( E Q (CAR ( E X P L O D E O ) (QUOTE X ) ) ( L I S T O ) X T N I L ) ) ) 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 ) X C O N D 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 (LAMBDA ( A B) X C O N D X ( N U L L B) N I L ) > ( ( E Q A (CAR B ) ) T ) X T (ATMEMBER A (CDR B 1 1 ) ) ) ) ) ) ) > D E F I N E ( ( ( S T A N D (LAMBDA ( C ) X P R O G ( A ) X S E T Q A ( V A R S E T O ) >TAG (COND X ( N U L L A) (RETURN C ) ) ) X S E T Q C (ATOMSUBST (GENSYM1 (QUOTE X ) ) (CAR A ) O ) X S E T Q A (CDR A ) ) X G O T A G ) ) ) ) ) ) >DEFIL E ( ( ( S I G M A (LAMBDA ( C D) X P R O G ( L A B ) X S E T Q L N I L ) >L1 ( S E T Q A (CAR C>) X S E T Q B (CAR D ) ) X C O N D > ( ( 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 ) ) ) (RETURN 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 ) ) ) X G O L l ) >lh (COND X ( E Q (CAR ( E X P L O D E A ) ) (QUOTE X ) ) (GO L 6 ) ) > ( ( N O T (ATOM B ) ) (RETURN N I L ) ) > ( ( E Q (CAR ( E X P L O D E B ) ) (QUOTE X ) ) (GO L 3 ) ) > ( ( N O T ( E Q 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 L 2 ) >L5 (COND >((NOT ( E Q (CAR ( E X P L O D E B ) ) (QUOTE X ) ) ) (RETURN N I L ) ) X ( A T V A R O F B A ) (RETURN N I L ) ) ) X G O L 3 ) >L6 (COND ( ( E Q A B " (GO L 7 ) ) # 34. > ( ( A T V A R O F A B " (RETURN N I L ) ) ) X S E T Q L ( A P P E N D 1 L ( L I S T B A ) ) ) X S E T Q C (ATOMSUBST B A (CDR C ) ) ) X S E T Q D (ATOMSUBST B A (CDR D ) ) ) >L2 (COND >((NOT ( N U L L O ) (GO L l ) ) > ( ( N U L L L ) ( R E T U R N 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 (ATOMSUBST A B (CDR C ) ) ) X S E T Q D (ATOMSUBSS A B (CDR D ) ) ) X G O L 2 ) ) ) ) ) ) > 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 (CAR X ) ( U N I O N (CDR X ) Y ) ) ) ) ) ) ) ) > D E F I N E ( ( ( E F F A C E (LAMBDA (A X ) X C O N D X C N U L L X ) N I L ) X ( E Q U A L A (CAR X ) ) (CDR X ) ) X T (CONS (CAR X ) ( E F F A C E A (CDR X ) ) ) ) ) ) ) ) ) > D E F I N E ( ( ( S U B S T (LAMBDA (X Y Z ) X C O N D > ( ( E Q U A L Y Z ) X ) X ( A T O M Z ) Z ) X T (CONS ( S U B S T X Y (CAR Z ) ) ( S U B S T X Y (CDR Z ) ) ) ) ) ) ) ) ) >DEFINE ( ( ( S T R I N G S U B (LAMBDA ( S T V Z ) X C O N D 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 ST V (CAR 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 (LAMBDA (X A Z ) X C O N D X ( E Q A Z ) X ) X C A T O M Z ) Z ) X T (CONS (ATOMSUBST X A (CAR Z ) ) X A T O M S U B S T X A (CDR Z ) ) ) ) ) ) ) ) ) > D E F I N E ( ( ( A T V A R O F (LAMBDA ( A Y ) X C O N D X ( A T O M Y ) (COND X ( E Q A Y ) T ) X T N I L ) ) ) X T (OR ( A T V A R O F A (CAR Y ) ) ( A T V A R O F A (CDR Y ) ) ) ) ) ) ) ) ) # 3. The function EQGEN and supporting routines. 35. > 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 ) (RETURN N I L ) ) > ( ( N U L L O E U K G O N O N L Y ) ) ) X S E T Q NEW NEU) ( S E T Q OLD OEU) >SU ( S E T Q P I (CAR 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 (TRANS 1 P I P 2 ) ) (GO S A ) >NP ( S E T Q P3 (TRANS 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 (STAND P 3 ) ) ) ) ) X C 0 N D ( F L A G 1 ( G 0 C U ) ) ) 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 NEW)) > ( 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 ) ) ) X R E T U R N 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 Tl* ( C A R (CDDDR P 2 ) ) ) X C O N D U E Q U A L N l ) ( G O P P ) ) > ( ( E Q U A L 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 ) ( R E T U R N 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 ) T l 7k))) > ( T (RETURN ( 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 ) ( R E T U R N 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 (RETURN ( 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 ) ( R E T U R N 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 (RETURN ( 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 ( L E N G T H 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 (STAND ( 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 ) ) > ( C O N D ( ( G R E A T E R P I L ) ( R E T U R N 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 (CAR N U ) ) ( S E T Q PCDR (CDR N U ) ) X C O N D U N U L L PCDR) (RETURN 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 ) ) X S E T Q I 1 ) ) > ( ( A N D ( E Q (CAR P l ) D A S H ) ( E Q (CAR P 2 ) P L U S S ) ) X S E T Q I 2 ) ) > ( ( A N D ( E Q (CAR P l ) P L U S S M ( E Q (CAR P 2 ) DASH ) ) X S E T Q 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 (STAND 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 LO) > L U ( S E T Q FLAG N I L ) X S E T Q P l P 2 ) 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 ( U L 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 ) ) X G O 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 10MS, VALUE IS ... UTP ARGUMENTS FOR EVALQUOTE ... RESTORE (UTP) COLLECTED 18140 CELLS AND STACK HAS 5994 UNITS LEFT. TIME 3259MS, VALUE IS ... NIL 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 Xll) 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 X6)) 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 Xll) X l l (K.X11)) CONTRADICTS (+ P X0000017 (H X0000016 XOO00O16) X0000017) TIME 524MS, VALUE IS ... T

Cite

Citation Scheme:

    

Usage Statistics

Country Views Downloads
France 2 0
United States 2 0
United Kingdom 1 0
China 1 0
City Views Downloads
Unknown 3 6
Beijing 1 0
London 1 0
Ashburn 1 0

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

Share

Share to:

Comment

Related Items