Proof compressions with circuit-structured substitutions

DOI10.1007/S10958-009-9405-3MaRDI QIDQ843604zbMATH OpenOpenAlexFDO

Authors 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

automatic theorem provingunificationcut-free proofsatomic-cuts proofscircuit-structured deductionsproof size

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 515726
• Cut Elimination In Situ
• Proof compression and NP versus PSPACE
• Atomic cut introduction by resolution: proof structuring and compression
• Exponentially huge natural deduction proofs are redundant: preliminary results on \(M_{\supset}\)

Cites work

• scientific article; zbMATH DE number 5910658 (Why is no real title available?)
• scientific article; zbMATH DE number 1179974 (Why is no real title available?)
• scientific article; zbMATH DE number 1526721 (Why is no real title available?)
• Finite investigations of transfinite derivations
• On cut elimination in the presence of perice rule
• Polynomial size proofs of the propositional pigeonhole principle
• The intractability of resolution

Cited in

(8)

• Proof compression and NP versus PSPACE
• Exponentially huge natural deduction proofs are redundant: preliminary results on \(M_{\supset}\)
• A compact representation of proofs
• A Subatomic Proof System for Decision Trees
• On strong normalization in proof-graphs for propositional logic
• scientific article; zbMATH DE number 1552526 (Why is no real title available?)
• Proof compression and NP versus PSPACE. II
• Propositional proof compressions and DNF logic

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

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