Integrating folding-up and splitting lemmas into model generation

Makoto Matsushita, Ryuzo Hasegawa, Hiroshi Fujita, Miyuki Koshimura

Research output: Contribution to journalArticlepeer-review


MGTP (Model Generation Theorem Prover) is a first order theorem prover based on model generation method which tries to construct Herbrand models of a given problem. We have embedded the folding-up rule into MGTP. The folding-up rule is used to ignore duplicate subproofs. We also have embedded the splitting lemma rule into MGTP. The splitting lemma rule is used to prune redundant models. In this study, we integrate both folding-up and splitting lemma rules into MGTP in order to strengthen MGTP. We evaluate effects of the integration by proving some typical problems.

Original languageEnglish
Pages (from-to)23-28
Number of pages6
JournalResearch Reports on Information Science and Electrical Engineering of Kyushu University
Issue number1
Publication statusPublished - Mar 2002

All Science Journal Classification (ASJC) codes

  • General Computer Science
  • Electrical and Electronic Engineering


Dive into the research topics of 'Integrating folding-up and splitting lemmas into model generation'. Together they form a unique fingerprint.

Cite this