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

DOI10.1093/JIGPAL/JZM040zbMath1159.03038OpenAlexW1991481174MaRDI QIDQ5436992

Marcelo Finger, Dov M. Gabbay

Publication date: 18 January 2008

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

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

zbMATH Keywords

tableauxcut eliminationsequent calculusproof theorySAT-solversinference-based learningnon-analytic cutsdecision-based learning

Mathematics Subject Classification ID

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

Related Items (4)

The problem of \(\Pi_{2}\)-cut-introduction ⋮ On the generation of quantified lemmas ⋮ Algorithmic introduction of quantified cuts ⋮ Physics and proof theory

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