Proof compressions with circuit-structured substitutions

DOI10.1007/S10958-009-9405-3zbMATH Open1191.03043OpenAlexW2073542215MaRDI QIDQ843604FDOQ843604

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

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}\)

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)

Cites Work

• The intractability of resolution
• Polynomial size proofs of the propositional pigeonhole principle
• Finite investigations of transfinite derivations
• On cut elimination in the presence of perice rule
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (8)

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

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)