TY - JOUR

T1 - A model generation based theorem prover MGTP for first-order logic

AU - Hasegawa, Ryuzo

AU - Fujita, Hiroshi

AU - Koshimura, Miyuki

AU - Shirai, Yasuyuki

PY - 2002

Y1 - 2002

N2 - This paper describes the major results on research and development of a model generation theorem prover MGTP. It exploits OR parallelism for non-Horn problems and AND parallelism for Horn problems achieving more than a 200-fold speedup on a parallel inference machine PIM with 256 processing elements. With MGTP, we succeeded in proving difficult mathematical problems that cannot be proven on sequential systems, including several open problems in finite algebra. To enhance the pruning ability of MGTP, several new features are added to it. These include: CMGTP and IV-MGTP to deal with constraint satisfaction problems, enabling negative and interval constraint propagation, respectively, non-Horn magic set to suppress the generation of useless model candidates caused by irrelevant clauses, a proof simplification method to eliminate duplicated subproofs, and MM-MGTP for minimal model generation. 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.

AB - This paper describes the major results on research and development of a model generation theorem prover MGTP. It exploits OR parallelism for non-Horn problems and AND parallelism for Horn problems achieving more than a 200-fold speedup on a parallel inference machine PIM with 256 processing elements. With MGTP, we succeeded in proving difficult mathematical problems that cannot be proven on sequential systems, including several open problems in finite algebra. To enhance the pruning ability of MGTP, several new features are added to it. These include: CMGTP and IV-MGTP to deal with constraint satisfaction problems, enabling negative and interval constraint propagation, respectively, non-Horn magic set to suppress the generation of useless model candidates caused by irrelevant clauses, a proof simplification method to eliminate duplicated subproofs, and MM-MGTP for minimal model generation. 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.

UR - http://www.scopus.com/inward/record.url?scp=23044532240&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=23044532240&partnerID=8YFLogxK

U2 - 10.1007/3-540-45632-5_8

DO - 10.1007/3-540-45632-5_8

M3 - Article

AN - SCOPUS:23044532240

SN - 0302-9743

VL - 2408

SP - 178

EP - 213

JO - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

JF - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

ER -