Structuring resolution proofs by introducing new lemmata or how to improve the readability of ATP-generated proofs

DOI10.1023/A:1005890730317MaRDI QIDQ1369079zbMATH OpenOpenAlexFDO

Authors K. Hörwein

Publication date 7 October 1997

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1023/a:1005890730317

zbMATH Keywords

function introduction rulesreadabilityreduction of proof heightstructuring of resolution proofs

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 4043813
• scientific article; zbMATH DE number 4164180
• scientific article; zbMATH DE number 1088197
• An efficient and flexible approach to resolution proof reduction
• On the generation of quantified lemmas

Cited in

(1)

• scientific article; zbMATH DE number 4043813 (Why is no real title available?)

This page was built for publication: Structuring resolution proofs by introducing new lemmata or how to improve the readability of ATP-generated proofs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1369079)