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

DOI10.1093/JIGPAL/JZM040zbMATH Open1159.03038OpenAlexW1991481174MaRDI QIDQ5436992FDOQ5436992

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

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

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)

Cited In (6)

• The Taming of the Cut. Classical Refutations with Analytic Cut
• Algorithmic introduction of quantified cuts
• On the generation of quantified lemmas
• Physics and proof theory
• The problem of \(\Pi_{2}\)-cut-introduction
• Title not available (Why is that?)

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)