Cut-Simulation and Impredicativity
From MaRDI portal
Publication:3623018
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
cut eliminationsequent calculustype theorycut simulation impredicative higher-order logichigher-order proof automation
Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05)
Related Items
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
