Strong Contraction in Model Elimination Calculus: Implementation in a PTTP-Based Theorem Prover

Koji IWANUMA; Kazuhiko OOTA

Strong Contraction in Model Elimination Calculus: Implementation in a PTTP-Based Theorem Prover

Koji IWANUMA, Kazuhiko OOTA

Full Text Views

0

Cite this

Summary :

In this paper, we propose a new lemma facility, called the strong contraction rule, for model elimination calculus, and we study some implementation issues of strong contraction in a PTTP-based theorem prover. Strong contraction has the ability to shorten possible proofs and prevent some irrelevant computation to a target goal. Strong contraction never broadens the search space, in principle, and thus, has a stable effect on the acceleration of top-down proof search. However, it is difficult to embed the strong contraction into a PTTP-based theorem prover, because strong contraction imposes a truncation operation of center chains in model elimination calculus. We show a self-truncation-style Prolog code, which makes it possible to retain the high performance of a PTTP-based prover with strong contraction. Finally, we evaluate the performance and effect of strong contraction by performing some experiments.

Publication: IEICE TRANSACTIONS on Information Vol.E81-D No.5 pp.464-471

Publication Date: 1998/05/25

Publicized

Online ISSN

DOI

Type of Manuscript

Category: Artificial Intelligence and Cognitive Science

Cite this

Copy

Koji IWANUMA, Kazuhiko OOTA, "Strong Contraction in Model Elimination Calculus: Implementation in a PTTP-Based Theorem Prover" in IEICE TRANSACTIONS on Information, vol. E81-D, no. 5, pp. 464-471, May 1998, doi: .
Abstract: In this paper, we propose a new lemma facility, called the strong contraction rule, for model elimination calculus, and we study some implementation issues of strong contraction in a PTTP-based theorem prover. Strong contraction has the ability to shorten possible proofs and prevent some irrelevant computation to a target goal. Strong contraction never broadens the search space, in principle, and thus, has a stable effect on the acceleration of top-down proof search. However, it is difficult to embed the strong contraction into a PTTP-based theorem prover, because strong contraction imposes a truncation operation of center chains in model elimination calculus. We show a self-truncation-style Prolog code, which makes it possible to retain the high performance of a PTTP-based prover with strong contraction. Finally, we evaluate the performance and effect of strong contraction by performing some experiments.
URL: https://global.ieice.org/en_transactions/information/10.1587/e81-d_5_464/_p

Copy

@ARTICLE{e81-d_5_464,
author={Koji IWANUMA, Kazuhiko OOTA, },
journal={IEICE TRANSACTIONS on Information},
title={Strong Contraction in Model Elimination Calculus: Implementation in a PTTP-Based Theorem Prover},
year={1998},
volume={E81-D},
number={5},
pages={464-471},
abstract={In this paper, we propose a new lemma facility, called the strong contraction rule, for model elimination calculus, and we study some implementation issues of strong contraction in a PTTP-based theorem prover. Strong contraction has the ability to shorten possible proofs and prevent some irrelevant computation to a target goal. Strong contraction never broadens the search space, in principle, and thus, has a stable effect on the acceleration of top-down proof search. However, it is difficult to embed the strong contraction into a PTTP-based theorem prover, because strong contraction imposes a truncation operation of center chains in model elimination calculus. We show a self-truncation-style Prolog code, which makes it possible to retain the high performance of a PTTP-based prover with strong contraction. Finally, we evaluate the performance and effect of strong contraction by performing some experiments.},
keywords={},
doi={},
ISSN={},
month={May},}

Copy

TY - JOUR
TI - Strong Contraction in Model Elimination Calculus: Implementation in a PTTP-Based Theorem Prover
T2 - IEICE TRANSACTIONS on Information
SP - 464
EP - 471
AU - Koji IWANUMA
AU - Kazuhiko OOTA
PY - 1998
DO -
JO - IEICE TRANSACTIONS on Information
SN -
VL - E81-D
IS - 5
JA - IEICE TRANSACTIONS on Information
Y1 - May 1998
AB - In this paper, we propose a new lemma facility, called the strong contraction rule, for model elimination calculus, and we study some implementation issues of strong contraction in a PTTP-based theorem prover. Strong contraction has the ability to shorten possible proofs and prevent some irrelevant computation to a target goal. Strong contraction never broadens the search space, in principle, and thus, has a stable effect on the acceleration of top-down proof search. However, it is difficult to embed the strong contraction into a PTTP-based theorem prover, because strong contraction imposes a truncation operation of center chains in model elimination calculus. We show a self-truncation-style Prolog code, which makes it possible to retain the high performance of a PTTP-based prover with strong contraction. Finally, we evaluate the performance and effect of strong contraction by performing some experiments.
ER -