Proof simplification for model generation and its applications

Miyuki Koshimura, Ryuzo Hasegawa

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

4 Citations (Scopus)

Abstract

Proof simplification eliminates unnecessary parts from a proof leaving only essential parts in a simplified proof. This paper gives a proof simplification procedure for model generation theorem proving and its applications to proof condensation, folding-up and completeness proofs for non-Horn magic sets. These indicate that proof simplification plays a useful role in theorem proving.

Original languageEnglish
Title of host publicationLogic for Programming and Automated Reasoning - 7th International Conference, LPAR 2000, Proceedings
EditorsAndrei Voronkov, Michel Parigot
PublisherSpringer Verlag
Pages96-113
Number of pages18
ISBN (Print)3540412859, 9783540412854
Publication statusPublished - Jan 1 2000
Event7th International Conference on Logic for Programming and Automated Reasoning, LPAR 2000 - Reunion Island, France
Duration: Nov 6 2000Nov 10 2000

Publication series

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

Other

Other7th International Conference on Logic for Programming and Automated Reasoning, LPAR 2000
CountryFrance
CityReunion Island
Period11/6/0011/10/00

Fingerprint

Theorem proving
Simplification
Condensation
Theorem Proving
Model
Folding
Completeness
Eliminate

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Koshimura, M., & Hasegawa, R. (2000). Proof simplification for model generation and its applications. In A. Voronkov, & M. Parigot (Eds.), Logic for Programming and Automated Reasoning - 7th International Conference, LPAR 2000, Proceedings (pp. 96-113). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1955). Springer Verlag.

Proof simplification for model generation and its applications. / Koshimura, Miyuki; Hasegawa, Ryuzo.

Logic for Programming and Automated Reasoning - 7th International Conference, LPAR 2000, Proceedings. ed. / Andrei Voronkov; Michel Parigot. Springer Verlag, 2000. p. 96-113 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1955).

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

Koshimura, M & Hasegawa, R 2000, Proof simplification for model generation and its applications. in A Voronkov & M Parigot (eds), Logic for Programming and Automated Reasoning - 7th International Conference, LPAR 2000, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1955, Springer Verlag, pp. 96-113, 7th International Conference on Logic for Programming and Automated Reasoning, LPAR 2000, Reunion Island, France, 11/6/00.
Koshimura M, Hasegawa R. Proof simplification for model generation and its applications. In Voronkov A, Parigot M, editors, Logic for Programming and Automated Reasoning - 7th International Conference, LPAR 2000, Proceedings. Springer Verlag. 2000. p. 96-113. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Koshimura, Miyuki ; Hasegawa, Ryuzo. / Proof simplification for model generation and its applications. Logic for Programming and Automated Reasoning - 7th International Conference, LPAR 2000, Proceedings. editor / Andrei Voronkov ; Michel Parigot. Springer Verlag, 2000. pp. 96-113 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{5639acda2d3f47a998da106c224eb6c5,
title = "Proof simplification for model generation and its applications",
abstract = "Proof simplification eliminates unnecessary parts from a proof leaving only essential parts in a simplified proof. This paper gives a proof simplification procedure for model generation theorem proving and its applications to proof condensation, folding-up and completeness proofs for non-Horn magic sets. These indicate that proof simplification plays a useful role in theorem proving.",
author = "Miyuki Koshimura and Ryuzo Hasegawa",
year = "2000",
month = "1",
day = "1",
language = "English",
isbn = "3540412859",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "96--113",
editor = "Andrei Voronkov and Michel Parigot",
booktitle = "Logic for Programming and Automated Reasoning - 7th International Conference, LPAR 2000, Proceedings",
address = "Germany",

}

TY - GEN

T1 - Proof simplification for model generation and its applications

AU - Koshimura, Miyuki

AU - Hasegawa, Ryuzo

PY - 2000/1/1

Y1 - 2000/1/1

N2 - Proof simplification eliminates unnecessary parts from a proof leaving only essential parts in a simplified proof. This paper gives a proof simplification procedure for model generation theorem proving and its applications to proof condensation, folding-up and completeness proofs for non-Horn magic sets. These indicate that proof simplification plays a useful role in theorem proving.

AB - Proof simplification eliminates unnecessary parts from a proof leaving only essential parts in a simplified proof. This paper gives a proof simplification procedure for model generation theorem proving and its applications to proof condensation, folding-up and completeness proofs for non-Horn magic sets. These indicate that proof simplification plays a useful role in theorem proving.

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

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

M3 - Conference contribution

AN - SCOPUS:84956866046

SN - 3540412859

SN - 9783540412854

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

SP - 96

EP - 113

BT - Logic for Programming and Automated Reasoning - 7th International Conference, LPAR 2000, Proceedings

A2 - Voronkov, Andrei

A2 - Parigot, Michel

PB - Springer Verlag

ER -