A Model Generation Theorem Prover MGTP

MGTP can exploit OR-parallelism for non-Horn problems and
AND-parallelism for Horn problems. MGTP achieves a more than 200-fold
speedup on a parallel inference machine PIM/m consisting of 256
processing elements. Using MGTP, we succeeded in proving some
difficult mathematical problems that could not be proven on sequential
systems, such as condensed detachment problems and quasigroup
existence problems.

To enhance the ability to prune search spaces, we have developed a new
method called {\it Non-Horn Magic Sets} (NHM). The NHM method
suppresses useless model generation with clauses irrelevant to the
goal.

We have also developed an extended version of MGTP called CMGTP to
tackle with constraint satisfaction problems. CMGTP allows the
description of negative atoms in its input clauses, and enables
negative constraint propagation by incorporating unit refutation and
unit simplification mechanisms. In many cases, CMGTP makes it
possible to reduce search spaces by orders of magnitude compared to
the original MGTP without constraint handling.

We have studied several applications in AI, such as negation as
failure and abductive reasoning 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.