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.
Cite
CITATION STYLE
Koshimura, M., & Hasegawa, R. (2000). Proof simplification for model generation and its applications. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1955, pp. 96–113). Springer Verlag. https://doi.org/10.1007/3-540-44404-1_8
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
