On the elimination of quantifier-free cuts

DOI10.1016/J.TCS.2011.08.035MaRDI QIDQ650922zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Daniel Weller

Publication date 7 December 2011

Published in Theoretical Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International

Full work available at URL https://doi.org/10.1016/j.tcs.2011.08.035

zbMATH Keywords

complexityfirst-order logicHerbrand's theoremcut-eliminationexponential upper boundquantifier-free cuts

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Classical first-order logic (03B10)

Recommendations

• The role of quantifier alternations in cut elimination
• Cut Elimination in ε‐Calculi
• Cut Elimination in the Presence of Axioms
• Bounds for cut elimination in intuitionistic propositional logic
• scientific article; zbMATH DE number 48659
• scientific article; zbMATH DE number 777292
• Elimination of Quantifiers on Łukasiewicz Logics
• Elementary elimination of prenex cuts in disjunction-free intuitionistic logic
• A cut-elimination proof in intuitionistic predicate logic
• Cut-elimination for quantified conditional logic

Cites work

• scientific article; zbMATH DE number 1215493 (Why is no real title available?)
• scientific article; zbMATH DE number 627412 (Why is no real title available?)
• scientific article; zbMATH DE number 1497485 (Why is no real title available?)
• A compact representation of proofs
• Computer Science Logic
• Cut elimination and automatic proof procedures
• Depth of proofs, depth of cut-formulas and complexity of cut formulas
• Describing proofs by short tautologies
• Herbrand Sequent Extraction
• Lower bounds to the size of constant-depth propositional proofs
• Reducing redundancy in cut-elimination by resolution
• The Complexity of Propositional Proofs
• The role of quantifier alternations in cut elimination
• Untersuchungen über das logische Schliessen. I

Cited in

(4)

• On the elimination of some higher type quantifiers
• Quantifier elimination for o-minimal structures expanded by a valuational cut
• scientific article; zbMATH DE number 2051382 (Why is no real title available?)
• The role of quantifier alternations in cut elimination

This page was built for publication: On the elimination of quantifier-free cuts

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