Structuring of computer-generated proofs by cut introduction

DOI10.1007/3-540-63385-5_39MaRDI QIDQ4364511zbMATH OpenFDO

Authors Uwe Egly, Karin Genther

Publication date 17 November 1997

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-63385-5_39

zbMATH Keywords

cut-rulehuman-oriented presentation of computer-generated proofs

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Presenting intuitive deductions via symmetric simplification
• scientific article; zbMATH DE number 4164180
• Towards Algorithmic Cut-Introduction
• Atomic cut introduction by resolution: proof structuring and compression
• Cut elimination and automatic proof procedures

Cited in

(7)

• Structuring resolution proofs by introducing new lemmata or how to improve the readability of ATP-generated proofs
• Structure of proofs and the complexity of cut elimination
• Atomic cut introduction by resolution: proof structuring and compression
• Introducing quantified cuts in logic with equality
• scientific article; zbMATH DE number 4164180 (Why is no real title available?)
• scientific article; zbMATH DE number 515726 (Why is no real title available?)
• Presenting intuitive deductions via symmetric simplification

This page was built for publication: Structuring of computer-generated proofs by cut introduction

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