| AITEC Contract Research Projects in FY1997 : Software |
| Principal Investigator : | Katsumi Inoue, Associate Professor |
| Kobe University |
MGTP (Model Generation Theorem Prover) is a model generation theorem proving system that has been developed by Institute for New Generation Computer Technology (ICOT). MGTP checks the satisfiability of axiom sets in full first-order predicate logic, and computes minimal models of clause sets in a bottom-up and incremental manner. MGTP has been widely used as a theorem prover for full first-order logic. However, for purposes other than theorem proving, MGTP has been less used. In particular, the methodology for non-Horn clause programming has not been well developed as compared with Horn clause logic programming. In particular, MGTP has the following weak points. First, as a bottom-up reasoning system for disjunctive logic programming, MGTP does not have a sophisticated control module with the variety of search methods. Second, as a first-order theorem prover, MGTP has three search strategies, but each strategy uses depth-first search only. Then, MGTP may not terminate for theorem proving problems that have both finite and infinite models. Third, Inoue et al. have recently developed advanced reasoning systems on top of MGTP. However, these systems restrict the class of problems to be solved, and thus cannot solve optimization problems that have cost functions for various applications. To expand the application range of MGTP and to use MGTP for more practical problems, a function to search based on costs or probabilities is necessary. To solve these problems, we developed several search strategies for MGTP. First, we introduce depth-first iterative-deepening search (DFID) to MGTP in order to improve the termination of MGTP. Next, we propose a general programming language in the form of disjunctive logic programs with costs. In this language, each disjunct in a disjunctive clause is associated with its cost. Then, to apply MGTP to optimization problems, we incorporate a new search algorithm into MGTP called best-first iterative-deepening search (BFID), which can deal with problems with costs in a best-first manner. Finally, we apply Non-Horn Magic-Sets (NHM) method in order to increase the efficiency of the optimization problem. NHM has been used to simulate goal-oriented top-down reasoning in bottom-up theorem proving by MGTP. Using NHM for disjunctive programming in MGTP, we can increase the efficiency of MGTP in solving optimization problems since we can restrict the search space in bottom-up reasoning only to subgoals that are related to the given goal. As a result, we improved the termination of MGTP in theorem proving, and extended MGTP to solve problems with costs. Moreover, by applying the NHM method to MGTP with BFID, the experimental results shows that our system has a good performance for optimization problems. Consequently, we extended MGTP to deal with more advanced problems, and developed the methodology for non-Horn clause programming.
Prolog on UNIX Workstation. The software is tested for running in SICStus Prolog v.2.1#9 on SunOS 4.1.3.
The expanded directory has the following directories and files:
There has been no English manual for MGTP-BF. If you are interested in using MGTP-BF, please contact the copyright owner:
www-admin@icot.or.jp