scientific article; zbMATH DE number 1748575

MaRDI QIDQ4530460zbMATH OpenFDO

Authors Elmar Eder

Publication date 13 November 2002

zbMATH Keywords

automated theorem provingcut-free proofslength of proofs

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20)

Recommendations

• Cut rule for the resolution method
• Cut elimination and automatic proof procedures
• scientific article; zbMATH DE number 1552525
• Cut-elimination and redundancy-elimination by resolution
• scientific article; zbMATH DE number 48763

Cited in

(15)

• Controlled integration of the cut rule into connection tableau calculi
• Cut rule for the resolution method
• Cut elimination for the unified logic
• Cut rules and explicit substitutions
• \textbf{R}-calculus without the cut rule
• Restricting backtracking in connection calculi
• scientific article; zbMATH DE number 48763 (Why is no real title available?)
• scientific article; zbMATH DE number 1086658 (Why is no real title available?)
• Non-elementary speed-ups in proof length by different variants of classical analytic calculi
• From Schütte’s Formal Systems to Modern Automated Deduction
• Equal Rights for the Cut: Computable Non-analytic Cuts in Cut-based Proofs
• scientific article; zbMATH DE number 5059634 (Why is no real title available?)
• Backward reasoning in systems with cut
• Interpolants, cut elimination and flow graphs for the propositional calculus
• Cut and pay

This page was built for publication:

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