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
Country/TerritoryFrance
CityReunion Island
Period11/6/0011/10/00

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Proof simplification for model generation and its applications'. Together they form a unique fingerprint.

Cite this