Proof compressions with circuit-structured substitutions
From MaRDI portal
Publication:843604
DOI10.1007/s10958-009-9405-3zbMath1191.03043MaRDI QIDQ843604
Edward Hermann Haeusler, V. G. da Costa, L. N. Gordeev
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
unification; automatic theorem proving; cut-free proofs; atomic-cuts proofs; circuit-structured deductions; proof size
03B35: Mechanization of proofs and logical operations
03F05: Cut-elimination and normal-form theorems
03F07: Structure of proofs
03F20: Complexity of proofs
Cites Work