Simulating non-prenex cuts in quantified propositional calculus

DOI10.1002/MALQ.201020093MaRDI QIDQ3096088zbMATH OpenOpenAlexFDO

Authors

Publication date 7 November 2011

Published in Mathematical Logic Quarterly (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1002/malq.201020093

zbMATH Keywords

prenex cutsproof complexityquantified propositional calculus

Mathematics Subject Classification ID

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

Recommendations

• Cut-Simulation in Impredicative Logics
• Cut-elimination for quantified conditional logic
• Introducing quantified cuts in logic with equality
• Interpolants, cut elimination and flow graphs for the propositional calculus
• Bounds for cut elimination in intuitionistic propositional logic
• scientific article; zbMATH DE number 48659
• Examining Fragments of the Quantified Propositional Calculus
• Tractability of cut-free Gentzen type propositional calculus with permutation inference
• Theory and Applications of Satisfiability Testing
• The computational complexity of propositional cirquent calculus

Cites work

• Logical Foundations of Proof Complexity
• On induction-free provability
• Quantified propositional calculi and fragments of bounded arithmetic
• Quantified propositional calculus and a second-order theory for NC\(^{\text \textbf{1}}\)

Cited in

(5)

• An answer to an open problem of Urquhart
• Induction rules in bounded arithmetic
• Examining Fragments of the Quantified Propositional Calculus
• scientific article; zbMATH DE number 1507229 (Why is no real title available?)
• Tree grammars for the elimination of non-prenex cuts

This page was built for publication: Simulating non-prenex cuts in quantified propositional calculus

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