Cut-Simulation in Impredicative Logics

DOI10.1007/11814771_20MaRDI QIDQ3613411zbMATH OpenOpenAlexFDO

Authors Christoph Benzmüller, Michael Kohlhase, Chad E. Brown

Publication date 12 March 2009

Published in Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11814771_20

zbMATH Keywords

cut eliminationcut simulation impredicative higher-order logichigher-order proof automationsequent calculustype theory

Mathematics Subject Classification ID

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

Recommendations

• Cut-Simulation and Impredicativity
• Cut Elimination in the Presence of Axioms
• A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms
• Cut elimination in the intuitionistic theory of types with axioms and rewriting cuts, constructively
• On cut elimination in the presence of perice rule

Cited in

(2)

• Simulating non-prenex cuts in quantified propositional calculus
• Cut-Simulation and Impredicativity

This page was built for publication: Cut-Simulation in Impredicative Logics

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