MGTP: A model generation theorem prover-its advanced features and applications

This paper outlines a parallel model-generation based theoremproving system MGTP that we have been developing, focusing on the recent developments including novel techniques for efficient proof-search and successful applications. We have developed CMGTP (Constraint MGTP) to deal with constraint satisfaction problems. By attaining the constraint propagation with negative atoms, CMGTP makes it possible to reduce search spaces by orders of magnitude compared to the original MGTP. To enhance the ability to prune search spaces, we have developed a new method called non-Horn magic sets (NHM) and incorporated its relevancy testing function into the folding-up (FU) method proposed by Letz. The NHM method suppresses useless model generation with clauses irrelevant to the goal. The FU method avoids generating duplicated subproofs after case-splitting. With these methods we can eliminate two major kinds of redundancies in model-generation based theorem provers. We have studied several applications in AI such as negation as failure, abductive reasoning and modal logic systems, through extensive use of MGTP. These studies share a basic common idea, that is, to use MGTP as a meta-programming system. We can build various reasoning systems on MGTP by writing the specific inference rules for each system in MGTP input clauses. Furthermore, we are now working on other applications such as machine learning with MGTP and heuristic proof-search based on the genetic algorithm.