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)


www-admin@icot.or.jp