Refinements to depth-first iterative-deepening search in automatic theorem proving

摘要

This paper will discuss two refinements to the depth-first iterative-deepening search strategy. The first refinement, the priority system, is an attempt to simulate best-first search using depth-first iterative-deepening search. A new data structure, the priority list, is introduced into depth-first iterative-deepening search by the refinement. Some complexity results about the priority system are also given. 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. We quantify this process to control the depth-first iterative-deepening search. Both refinements have been implemented in a sequent-style back chaining theorem prover and tested on a large number of problems and have been shown to be effective.