### Abstract

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.

Original language | English |
---|---|

Pages (from-to) | 178-213 |

Number of pages | 36 |

Journal | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |

Volume | 2408 |

Publication status | Published - Jan 1 2002 |

### Fingerprint

### All Science Journal Classification (ASJC) codes

- Theoretical Computer Science
- Computer Science(all)

### Cite this

**A model generation based theorem prover MGTP for first-order logic.** / Hasegawa, Ryuzo; Fujita, Hiroshi; Koshimura, Miyuki; Shirai, Yasuyuki.

Research output: Contribution to journal › Article

*Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)*, vol. 2408, pp. 178-213.

}

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/1/1

Y1 - 2002/1/1

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

M3 - Article

AN - SCOPUS:23044532240

VL - 2408

SP - 178

EP - 213

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

SN - 0302-9743

ER -