Cut-Simulation and Impredicativity

DOI10.2168/LMCS-5(1:6)2009zbMath1160.03004arXiv0902.0043MaRDI QIDQ3623018

Michael Kohlhase, Christoph Benzmüller, Chad Edward Brown

Publication date: 29 April 2009

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/0902.0043

zbMATH Keywords

cut eliminationsequent calculustype theorycut simulation impredicative higher-order logichigher-order proof automation

Mathematics Subject Classification ID

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

Related Items (7)

Cut-elimination for quantified conditional logic ⋮ The higher-order prover \textsc{Leo}-II ⋮ Extensional higher-order paramodulation in Leo-III ⋮ Proofs and Reconstructions ⋮ Analytic tableaux for higher-order logic with choice ⋮ Automating free logic in HOL, with an experimental application in category theory ⋮ Effective Normalization Techniques for HOL

This page was built for publication: Cut-Simulation and Impredicativity