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

Ryuzo Hasegawa, Hiroshi Fujita, Miyuki Koshimura, Yasuyuki Shirai

Research output: Contribution to journalArticle

5 Citations (Scopus)

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 languageEnglish
Pages (from-to)178-213
Number of pages36
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2408
Publication statusPublished - Jan 1 2002

Fingerprint

First-order Logic
Theorem
Or-parallelism
Negation as Failure
Constraint Propagation
Constraint satisfaction problems
Computer systems programming
Minimal Model
Constraint Satisfaction Problem
Modal Logic
Pruning
Research and Development
Simplification
Algebra
Parallelism
Open Problems
Speedup
Fold
Eliminate
Programming

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

@article{391c9d63c4c042e280afaa0e3a56e47d,
title = "A model generation based theorem prover MGTP for first-order logic",
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.",
author = "Ryuzo Hasegawa and Hiroshi Fujita and Miyuki Koshimura and Yasuyuki Shirai",
year = "2002",
month = "1",
day = "1",
language = "English",
volume = "2408",
pages = "178--213",
journal = "Lecture Notes in Computer Science",
issn = "0302-9743",
publisher = "Springer Verlag",

}

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 -