Cut Elimination In Situ

DOI10.1007/978-3-319-10103-3_10MaRDI QIDQ5361251zbMATH OpenOpenAlexFDO

Authors Samuel R. Buss

Publication date 27 September 2017

Published in Gentzen's Centenary (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-10103-3_10

zbMATH Keywords

cut eliminationfirst-order logicpolynomial time methodspropositional logic

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Complexity of proofs (03F20)

Recommendations

• Methods of cut-elimination
• Multi-focused cut elimination
• Cut elimination in categories
• scientific article; zbMATH DE number 1471986
• Novikov's cut elimination
• Fast cut-elimination by CERES
• scientific article; zbMATH DE number 2051382
• scientific article; zbMATH DE number 1550359
• Don't eliminate cut
• Cut as consequence

Cited in

(30)

• Describing proofs by short tautologies
• Don't eliminate cut
• Cut elimination and automatic proof procedures
• Cut normal forms and proof complexity
• Herbrand's theorem as higher order recursion
• Efficient elimination of Skolem functions in \(\text{LK}^\text{h} \)
• The arithmetics of a theory
• Interpretability degrees of finitely axiomatized sequential theories
• Cuts and gluts
• Algorithmic introduction of quantified cuts
• Cut Elimination in the Presence of Axioms
• scientific article; zbMATH DE number 2006630 (Why is no real title available?)
• scientific article; zbMATH DE number 2051382 (Why is no real title available?)
• scientific article; zbMATH DE number 1471986 (Why is no real title available?)
• The cost of a cycle is a square
• scientific article; zbMATH DE number 7580067 (Why is no real title available?)
• The small-is-very-small principle
• Removing cycles from proofs
• The interpretation existence lemma
• Elementary elimination of prenex cuts in disjunction-free intuitionistic logic
• Tree grammars for the elimination of non-prenex cuts
• Proof Search Tree and Cut Elimination
• Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 12--17, 2023
• Cut formulas in propositional logic
• Corrected upper bounds for free-cut elimination
• Title not available (Why is no real title available?)
• Cut elimination for S4C: A case study
• Proof compressions with circuit-structured substitutions
• Transductions in arithmetic
• On the form of witness terms

This page was built for publication: Cut Elimination In Situ

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