Equal Rights for the Cut: Computable Non-analytic Cuts in Cut-based Proofs

DOI10.1093/JIGPAL/JZM040MaRDI QIDQ5436992zbMATH OpenOpenAlexFDO

Authors Marcelo Finger, Dov Gabbay

Publication date 18 January 2008

Published in Logic Journal of the IGPL (Search for Journal in Brave)

Full work available at URL https://semanticscholar.org/paper/b12bc34a9c1c5b7b1aff8b2872a02286f9c02449

zbMATH Keywords

proof theorycut eliminationsequent calculustableauxSAT-solversinference-based learningnon-analytic cutsdecision-based learning

Mathematics Subject Classification ID

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

Recommendations

• Analytic cut trees
• The Taming of the Cut. Classical Refutations with Analytic Cut
• scientific article; zbMATH DE number 1748575
• scientific article; zbMATH DE number 1552525
• Cut Elimination in the Presence of Axioms

Cited in

(6)

• Algorithmic introduction of quantified cuts
• The Taming of the Cut. Classical Refutations with Analytic Cut
• On the generation of quantified lemmas
• Physics and proof theory
• The problem of \(\Pi_{2}\)-cut-introduction
• scientific article; zbMATH DE number 1552525 (Why is no real title available?)

This page was built for publication: Equal Rights for the Cut: Computable Non-analytic Cuts in Cut-based Proofs

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