Argonne proving system(ID:8405/)Argonne proving system Places Related languages
References: External link: Online copy Extract: Introduction Introduction When resolution was first introduced, resolution-based theorem-proving programs had to deal with only a few rules of inference. The main ones were binary resolution and factoring. These rules were usually applied in a fixed order, e.g. as in the unit preference strategy of Twos, et al. [6], In addition, most of the early strategies had a minor effect on the question of when to do which operation. For example, the set-of-support strategy allows one to skip certain attempts at resolution but does not alter the order in which the memory is searched for clauses to operate on. Similar remarks hold for many other strategies such as tautology deletion, subscription, demodulation, and merging. Thus it is not uncommon for theorem-proving programs to be written to handle only a limited number of inference rules in a fairly rigid order with possibly a limited set of options concerning strategies. As research tools, such programs have two disadvantages: (1) in order to add a new inference rule, in addition to the code for the new rule, major modification of the section of the program that controls the sequence of operations will be required; and (2) experiments comparing different strategies, comparing different orders for performing given operations, and comparing different rules of inference are difficult to perform. The need for such capabilities arises from the many new rules of inference being developed for special areas of application. Examples of these are perambulation for equality [4], naming for higher-order logic [2], and the various rules for set theory developed by Slag le [5]. When new rules of inference are added to those already in the theorem-proving program, one is faced with the following question: in what order should the expanded set of rules be applied? For example, is it better to par a-modulate first and then resolve, or to perform many resolutions and perambulate only when resolution is blocked, etc.? In addition to the experiments arising from such questions, one would like to compare various existing strategies under various restrictions, especially for particular classes of problems. An example of such a class is the class of justifiable sets of clauses in which no clause has more than one positive literal. For any member of this class it is known that both an input refutation without the use of factoring exists, and a unit refutation without the use of factoring exists in which the unit is always positive [3]. One would like to compare, both with and without factoring, input resolution, unit resolution, and positive-unit resolution for such problems. This paper contains a general description of one language of a class of languages which provides for inference rule adjunction and experimentation of the kind mentioned above. Instructions of this rather simple language basically specify both an operation or inference rule and lists of clauses to which the operation is applied. An interpreter reads these instructions one by one, sets up the internal addresses and flags, then transfers to the appropriate routine that executes the operation. Thus to add a new rule of inference, one merely has to write the routine that performs the operation and make a minor addition to the interpreter. Such a program, then, might contain the operations resolution, factoring, paramodulation, and (higher-order) naming, as well as others, and the user could specify in what order he wants these operations performed by means of this new language. He could specify resolution, then naming, then resolution again, then paramodulation, etc., or specify some other order. With the language under discussion, strategies such as unit resolution and positive-unit resolution can be made available by specifying which instructions and clause lists are to be used. The reader might ask at this point if such a large program would be cumbersome or inefficient. It is the case that, for a given run on a given problem, routines that are not called for by the user's theorem-proving algorithm may be present in the memory. However, such routines will not be executed for the given problem, and their presence does not affect the execution of the other routines that are used. Moreover, the interpreter for the language can be very simple, giving a very small overhead. Thus, the efficiency of execution will be approximately the same as for programs with a fixed control section. Finally, the amount of memory required for the code for the unused routines and the interpreter is very small compared to the memory required to store large numbers of clauses. In addition, many of the basic routines are used by most or all operations and would be present in any event. Thus the memory requirements are not significantly greater, either. One major problem with implementing several rules of inference is the amount of memory needed to maintain restart information for each rule. In previous programs the amount of memory needed for restart information was dependent on the maximum number of clauses allowed. In Section 2, we give a method of handling restart information using tables whose size is dependent on the square of the number of lists, giving a reduction factor in the size of the restart tables of approximately 100. Section 3 contains an outline of a language of the type under consideration being implemented by the authors, and Section 4 contains some examples of programs in this language. The authors would like to state at the outset that it is the concept of a theorem-proving language that is important, not the details of the language or its implementation. The major thrust of this paper is to promote the development of theorem-proving systems that will provide adequate research tools for the development of useful theorem-proving algorithms. The basic ideas for this work developed out of a program, RW1, written by G. Robinson and L. Wos. The present paper is an extension and formalization of these ideas. Extract: Concluding Remarks Concluding Remarks The material of Section 2 concerning lists and restart tables is useful in that it allows implementation of several rules each requiring restart information. But it is the type of language and system of Section 3 that is of major importance, and not the particular implementation of such a system. An interpreter is suggested only because most programs of the size of the system proposed are assembled once and saved as object modules. If this approach is taken, a program in the new language would just be part of the input. The proposed system could instead be implemented just as well, for example, as a set of Fortran routines. The theorem-proving algorithm would then be a simple Fortran program. The ease and convenience of a system of the type proposed as a research tool is the most important aspect of this work. As seen by the examples, the language is very easy to use. In addition, such a language is extendable with theoretically no limit. An aspect that was not demonstrated, but may be very useful in practice, is the dynamic nature of strategies and options. For example, a program using demodulation may in fact fail to find a proof because a needed term was demodulated. In the proposed system, the user could arrange to generate some resolvents without demodulation. Finally, the system allows experimentation with a great many different theorem-proving algorithms using a variety of inference rules with relative ease. The user will also be able to specify virtually any combination of operations in any order. Thus, when a new strategy or heuristic is proposed, it can be tested and compared with other strategies. Experiments can be performed whose purpose is the testing of a program change intended to sharpen the efficiency of an algorithm. When an algorithm is found by experience to work well on a particular class of problems (even if the algorithm is not complete), it can be saved to be used again on problems of the same class. In the presence of new rules of inference, such experimental capability will be essential in developing effective theorem-proving algorithms. |