Proof compressions with circuit-structured substitutions

DOI10.1007/s10958-009-9405-3zbMath1191.03043OpenAlexW2073542215MaRDI QIDQ843604

V. G. da Costa, L. N. Gordeev, Edward Hermann Haeusler

Publication date: 15 January 2010

Published in: Journal of Mathematical Sciences (New York) (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10958-009-9405-3

zbMATH Keywords

unificationautomatic theorem provingcut-free proofsatomic-cuts proofscircuit-structured deductionsproof size

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) Complexity of proofs (03F20)

Related Items (2)

Proof compression and NP versus PSPACE ⋮ On strong normalization in proof-graphs for propositional logic

Cites Work

• The intractability of resolution
• Finite investigations of transfinite derivations
• Polynomial size proofs of the propositional pigeonhole principle
• On cut elimination in the presence of perice rule
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Proof compressions with circuit-structured substitutions