Atomic cut introduction by resolution: proof structuring and compression

DOI10.1007/978-3-642-17511-4_26MaRDI QIDQ3066113zbMATH OpenOpenAlexFDO

Authors Bruno Woltzenlogel Paleo

Publication date 7 January 2011

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-17511-4_26

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03) Complexity of proofs (03F20)

Recommendations

• Towards Algorithmic Cut-Introduction
• Algorithmic introduction of quantified cuts
• The problem of \(\Pi_{2}\)-cut-introduction
• scientific article; zbMATH DE number 515726
• scientific article; zbMATH DE number 1088197

Cited in

(13)

• The problem of \(\Pi_{2}\)-cut-introduction
• Learning from Łukasiewicz and Meredith: investigations into proof structures
• Physics and proof theory
• On the generation of quantified lemmas
• Implementation and evaluation of contextual natural deduction for minimal logic
• Introducing quantified cuts in logic with equality
• Towards the compression of first-order resolution proofs by lowering unit clauses
• Contextual Natural Deduction
• Algorithmic introduction of quantified cuts
• scientific article; zbMATH DE number 1088197 (Why is no real title available?)
• Complexity of translations from resolution to sequent calculus
• Lemmas: generation, selection, application
• Proof compressions with circuit-structured substitutions

This page was built for publication: Atomic cut introduction by resolution: proof structuring and compression

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