Proc. of FGCS '94, ICOT, Tokyo, December 1994
Parallel Theorem-Proving System : MGTP
Ryuzo Hasegawa
Institute For New Generation Computer Technology
4-28, Mita 1-chome, Minato-ku, Tokyo 108, Japan
hasegawa@icot.or.jp
Abstract:
The parallel theorem-proving system MGTP has been developed at
ICOT.
MGTP exploits 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 with 256 processing
elements. Using MGTP, we succeeded in proving difficult mathematical
problems including open problems that cannot be proven on sequential
systems.
We added two new MGTP features: Non-Horn Magic Set (NHM) and
Constraint MGTP (CMGTP). NHM is a technique to enhance the search
capacity by suppressing generation of irrelevant model candidates,
thereby making MGTP a practical prover. CMGTP is an extension of MGTP
to deal with constraint satisfaction problems, enabling constraint
propagations with negative atoms. CMGTP can prune search spaces
required for the original MGTP by orders of magnitude.
We studied several techniques necessary for the development of
applications, such as negation as failure, abductive reasoning and
modal logic systems, on MGTP. These techniques share a basic idea,
which is to use MGTP as a meta-programming system for each
application.
All of this proceedings (Compressed PostScript file) :
Parallel Theorem-Proving System : MGTP (180KB)