Automatic theorem-proving in problem reduction formats
Xumin Nie, David A. Plaisted · 1989
This thesis explores several topics concerning the sequent-style inference system--the modified problem reduction format. Chapter 1 is the introductory chapter. In Chapter 2, we will present how caching is performed with the depth-first iterative deepening search to implement the modified problem reduction format, in order to avoid the repeated work involved in solving a subgoal more than once. In Chapter 3, we present the formalization of goal generalization and how it is implemented by augmenting the modified problem reduction format, where goal generalization is a special case of Explanation-Based Generalization in maching learning. In Chapter 4, we will present how subgoal reordering is performed in the modified problem reduction format and how it is implemented. In Chapter 5 and Chapter 6, we will present two refinements to the depth-first iterative deepening search strategy in the implementation. The first refinement, the priority system, concerns how to incorporate the use of priority of subgoals into the depth-first iterative deepening search. We show that the time complexity of the priority systems is within a constant factor of the complexity of the depth-first iterative deepening search. The second refinement is based on a syntactic viewpoint of proof development, which views the process of finding proofs as an incremental process of constructing instances with a certain property. In Chapter 7, we present how semantics, or domain dependent knowledge, can be used in the inference system. In particular, we will present a semantic variant of the modified problem reduction format which selects its inference rules from any interpretation. This results in an inference system which is a true set-of-support strategy and allows back chaining. We will also discuss how contrapositives are used in the modified problem reduction format and its semantic variant. We will show that only some contrapositives are needed according to some interpretation.