Atomic Cut Introduction by Resolution: Proof Structuring and Compression

DOI10.1007/978-3-642-17511-4_26zbMath1253.03085OpenAlexW1506262198MaRDI QIDQ3066113

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)

Related Items (9)

Towards the Compression of First-Order Resolution Proofs by Lowering Unit Clauses ⋮ Contextual Natural Deduction ⋮ Implementation and Evaluation of Contextual Natural Deduction for Minimal Logic ⋮ The problem of \(\Pi_{2}\)-cut-introduction ⋮ On the generation of quantified lemmas ⋮ Algorithmic introduction of quantified cuts ⋮ Physics and proof theory ⋮ Learning from Łukasiewicz and Meredith: investigations into proof structures ⋮ Complexity of translations from resolution to sequent calculus

This page was built for publication: Atomic Cut Introduction by Resolution: Proof Structuring and Compression