Model Generation Theorem Proving and Its Elementary Techniques.

Research output: Contribution to journalArticle

Abstract

A theorem prover MGTP is known as one of the main results of the Fifth Generation Computer Project in 80's. MGTP is based on model generation that is considered suitable for implementing high performance provers on a parallel inference machine (PIM). This article overviews several improvements, extensions, applications, and current research topics of MGTP.

Original languageEnglish
Pages (from-to)2-10
Number of pages9
JournalComputer Software
Volume25
Issue number3
DOIs
Publication statusPublished - Jan 1 2008

Fingerprint

Theorem proving

All Science Journal Classification (ASJC) codes

  • Software

Cite this

Model Generation Theorem Proving and Its Elementary Techniques. / Hasegawa, Ryuzo; Fujita, Hiroshi; Koshimura, Miyuki.

In: Computer Software, Vol. 25, No. 3, 01.01.2008, p. 2-10.

Research output: Contribution to journalArticle

@article{f44cf1e7581544cfbfe067d34a0d486f,
title = "Model Generation Theorem Proving and Its Elementary Techniques.",
abstract = "A theorem prover MGTP is known as one of the main results of the Fifth Generation Computer Project in 80's. MGTP is based on model generation that is considered suitable for implementing high performance provers on a parallel inference machine (PIM). This article overviews several improvements, extensions, applications, and current research topics of MGTP.",
author = "Ryuzo Hasegawa and Hiroshi Fujita and Miyuki Koshimura",
year = "2008",
month = "1",
day = "1",
doi = "10.11309/jssst.25.3_2",
language = "English",
volume = "25",
pages = "2--10",
journal = "Computer Software",
issn = "0289-6540",
publisher = "Japan Society for Software Science and Technology",
number = "3",

}

TY - JOUR

T1 - Model Generation Theorem Proving and Its Elementary Techniques.

AU - Hasegawa, Ryuzo

AU - Fujita, Hiroshi

AU - Koshimura, Miyuki

PY - 2008/1/1

Y1 - 2008/1/1

N2 - A theorem prover MGTP is known as one of the main results of the Fifth Generation Computer Project in 80's. MGTP is based on model generation that is considered suitable for implementing high performance provers on a parallel inference machine (PIM). This article overviews several improvements, extensions, applications, and current research topics of MGTP.

AB - A theorem prover MGTP is known as one of the main results of the Fifth Generation Computer Project in 80's. MGTP is based on model generation that is considered suitable for implementing high performance provers on a parallel inference machine (PIM). This article overviews several improvements, extensions, applications, and current research topics of MGTP.

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

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

U2 - 10.11309/jssst.25.3_2

DO - 10.11309/jssst.25.3_2

M3 - Article

AN - SCOPUS:85024726181

VL - 25

SP - 2

EP - 10

JO - Computer Software

JF - Computer Software

SN - 0289-6540

IS - 3

ER -