Interactive advice system for automated theorem provers
Lawrence J. Henschen, Yusuf Öztürk · 1989
Two major obstacles faced by a Theorem Proving (TP) system user are the interaction between the system and the user and the need to learn the basic TP concepts such as the resolution technique, the strategy, and the representation of the problem. This study focuses on these problems, and suggests solutions by offering a new window-based TP user-interface and an expert advice system which will be a part of a TP system and help the user to implement his problem in a TP environment. The first part of the research emphasizes the improvements in the computer hardware, and offers advanced solutions for the user-interface of a TP system. Some of those suggestions have been implemented on a VAX 11/785 system to observe the feasibility of such improvements. Those experiments have shown that the user-interface of a TP can easily be improved with advanced programming by using the today's mini or mainframe computers as well as the fast microcomputers. An expert system based on first-order logic as the knowledge-base and resolution technique as the accessing mechanism constitutes the second part of the study. The basic criteria behind the design of the expert advice system is the portability between different TP systems and the ease of use. An expert database has been created for three different topics to examine the ease of creation and the use of such a system. Filling out the advice tree required some experimental runs made on a database of problems that lead us the definition of a class of clause sets for which the hyperresolution technique reached the proof without the use of function substitution axioms. The condition to define such a class of clause sets has been described and shown to be sufficient to eliminate the function substitution axioms.