MGTP: A model generation theorem prover-its advanced features and applications

Research output: Chapter in Book/Report/Conference proceedingConference contribution

8 Citations (Scopus)

Abstract

This paper outlines a parallel model-generation based theoremproving system MGTP that we have been developing, focusing on the recent developments including novel techniques for efficient proof-search and successful applications. We have developed CMGTP (Constraint MGTP) to deal with constraint satisfaction problems. By attaining the constraint propagation with negative atoms, CMGTP makes it possible to reduce search spaces by orders of magnitude compared to the original MGTP. To enhance the ability to prune search spaces, we have developed a new method called non-Horn magic sets (NHM) and incorporated its relevancy testing function into the folding-up (FU) method proposed by Letz. The NHM method suppresses useless model generation with clauses irrelevant to the goal. The FU method avoids generating duplicated subproofs after case-splitting. With these methods we can eliminate two major kinds of redundancies in model-generation based theorem provers. We have studied several applications in AI such as negation as failure, abductive reasoning and modal logic systems, through extensive use of MGTP. These studies share a basic common idea, that is, to use MGTP as a meta-programming system. We can build various reasoning systems on MGTP by writing the specific inference rules for each system in MGTP input clauses. Furthermore, we are now working on other applications such as machine learning with MGTP and heuristic proof-search based on the genetic algorithm.

Original languageEnglish
Title of host publicationAutomated Reasoning with Analytic Tableaux and Related Methods - International Conference, TABLEAUX 1997, Proceedings
EditorsDidier Galmiche
PublisherSpringer Verlag
Pages1-15
Number of pages15
ISBN (Print)3540629203, 9783540629207
DOIs
Publication statusPublished - Jan 1 1997
EventInternational Conference on Analytic Tableaux and Related Methods, TABLEAUX 1997 - Pont-a-Mousson, France
Duration: May 13 1997May 16 1997

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1227
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

OtherInternational Conference on Analytic Tableaux and Related Methods, TABLEAUX 1997
CountryFrance
CityPont-a-Mousson
Period5/13/975/16/97

Fingerprint

Proof Search
Theorem
Constraint satisfaction problems
Computer systems programming
Folding
Search Space
Reasoning
Redundancy
Learning systems
Negation as Failure
Constraint Propagation
Genetic algorithms
Model
Inference Rules
Heuristic Search
Constraint Satisfaction Problem
Atoms
Modal Logic
Testing
Machine Learning

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Hasegawa, R., Fujita, H., & Koshimura, M. (1997). MGTP: A model generation theorem prover-its advanced features and applications. In D. Galmiche (Ed.), Automated Reasoning with Analytic Tableaux and Related Methods - International Conference, TABLEAUX 1997, Proceedings (pp. 1-15). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1227). Springer Verlag. https://doi.org/10.1007/BFb0027401

MGTP : A model generation theorem prover-its advanced features and applications. / Hasegawa, Ryuzo; Fujita, Hiroshi; Koshimura, Miyuki.

Automated Reasoning with Analytic Tableaux and Related Methods - International Conference, TABLEAUX 1997, Proceedings. ed. / Didier Galmiche. Springer Verlag, 1997. p. 1-15 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1227).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Hasegawa, R, Fujita, H & Koshimura, M 1997, MGTP: A model generation theorem prover-its advanced features and applications. in D Galmiche (ed.), Automated Reasoning with Analytic Tableaux and Related Methods - International Conference, TABLEAUX 1997, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1227, Springer Verlag, pp. 1-15, International Conference on Analytic Tableaux and Related Methods, TABLEAUX 1997, Pont-a-Mousson, France, 5/13/97. https://doi.org/10.1007/BFb0027401
Hasegawa R, Fujita H, Koshimura M. MGTP: A model generation theorem prover-its advanced features and applications. In Galmiche D, editor, Automated Reasoning with Analytic Tableaux and Related Methods - International Conference, TABLEAUX 1997, Proceedings. Springer Verlag. 1997. p. 1-15. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/BFb0027401
Hasegawa, Ryuzo ; Fujita, Hiroshi ; Koshimura, Miyuki. / MGTP : A model generation theorem prover-its advanced features and applications. Automated Reasoning with Analytic Tableaux and Related Methods - International Conference, TABLEAUX 1997, Proceedings. editor / Didier Galmiche. Springer Verlag, 1997. pp. 1-15 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{46367a7344df4dfe993cf40deddca3d9,
title = "MGTP: A model generation theorem prover-its advanced features and applications",
abstract = "This paper outlines a parallel model-generation based theoremproving system MGTP that we have been developing, focusing on the recent developments including novel techniques for efficient proof-search and successful applications. We have developed CMGTP (Constraint MGTP) to deal with constraint satisfaction problems. By attaining the constraint propagation with negative atoms, CMGTP makes it possible to reduce search spaces by orders of magnitude compared to the original MGTP. To enhance the ability to prune search spaces, we have developed a new method called non-Horn magic sets (NHM) and incorporated its relevancy testing function into the folding-up (FU) method proposed by Letz. The NHM method suppresses useless model generation with clauses irrelevant to the goal. The FU method avoids generating duplicated subproofs after case-splitting. With these methods we can eliminate two major kinds of redundancies in model-generation based theorem provers. We have studied several applications in AI such as negation as failure, abductive reasoning and modal logic systems, through extensive use of MGTP. These studies share a basic common idea, that is, to use MGTP as a meta-programming system. We can build various reasoning systems on MGTP by writing the specific inference rules for each system in MGTP input clauses. Furthermore, we are now working on other applications such as machine learning with MGTP and heuristic proof-search based on the genetic algorithm.",
author = "Ryuzo Hasegawa and Hiroshi Fujita and Miyuki Koshimura",
year = "1997",
month = "1",
day = "1",
doi = "10.1007/BFb0027401",
language = "English",
isbn = "3540629203",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "1--15",
editor = "Didier Galmiche",
booktitle = "Automated Reasoning with Analytic Tableaux and Related Methods - International Conference, TABLEAUX 1997, Proceedings",
address = "Germany",

}

TY - GEN

T1 - MGTP

T2 - A model generation theorem prover-its advanced features and applications

AU - Hasegawa, Ryuzo

AU - Fujita, Hiroshi

AU - Koshimura, Miyuki

PY - 1997/1/1

Y1 - 1997/1/1

N2 - This paper outlines a parallel model-generation based theoremproving system MGTP that we have been developing, focusing on the recent developments including novel techniques for efficient proof-search and successful applications. We have developed CMGTP (Constraint MGTP) to deal with constraint satisfaction problems. By attaining the constraint propagation with negative atoms, CMGTP makes it possible to reduce search spaces by orders of magnitude compared to the original MGTP. To enhance the ability to prune search spaces, we have developed a new method called non-Horn magic sets (NHM) and incorporated its relevancy testing function into the folding-up (FU) method proposed by Letz. The NHM method suppresses useless model generation with clauses irrelevant to the goal. The FU method avoids generating duplicated subproofs after case-splitting. With these methods we can eliminate two major kinds of redundancies in model-generation based theorem provers. We have studied several applications in AI such as negation as failure, abductive reasoning and modal logic systems, through extensive use of MGTP. These studies share a basic common idea, that is, to use MGTP as a meta-programming system. We can build various reasoning systems on MGTP by writing the specific inference rules for each system in MGTP input clauses. Furthermore, we are now working on other applications such as machine learning with MGTP and heuristic proof-search based on the genetic algorithm.

AB - This paper outlines a parallel model-generation based theoremproving system MGTP that we have been developing, focusing on the recent developments including novel techniques for efficient proof-search and successful applications. We have developed CMGTP (Constraint MGTP) to deal with constraint satisfaction problems. By attaining the constraint propagation with negative atoms, CMGTP makes it possible to reduce search spaces by orders of magnitude compared to the original MGTP. To enhance the ability to prune search spaces, we have developed a new method called non-Horn magic sets (NHM) and incorporated its relevancy testing function into the folding-up (FU) method proposed by Letz. The NHM method suppresses useless model generation with clauses irrelevant to the goal. The FU method avoids generating duplicated subproofs after case-splitting. With these methods we can eliminate two major kinds of redundancies in model-generation based theorem provers. We have studied several applications in AI such as negation as failure, abductive reasoning and modal logic systems, through extensive use of MGTP. These studies share a basic common idea, that is, to use MGTP as a meta-programming system. We can build various reasoning systems on MGTP by writing the specific inference rules for each system in MGTP input clauses. Furthermore, we are now working on other applications such as machine learning with MGTP and heuristic proof-search based on the genetic algorithm.

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

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

U2 - 10.1007/BFb0027401

DO - 10.1007/BFb0027401

M3 - Conference contribution

AN - SCOPUS:84958750697

SN - 3540629203

SN - 9783540629207

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

SP - 1

EP - 15

BT - Automated Reasoning with Analytic Tableaux and Related Methods - International Conference, TABLEAUX 1997, Proceedings

A2 - Galmiche, Didier

PB - Springer Verlag

ER -