Cut-Simulation in Impredicative Logics

DOI10.1007/11814771_20zbMath1159.03303OpenAlexW1489391956MaRDI QIDQ3613411

Michael Kohlhase, Christoph Benzmüller, Chad Edward 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 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)

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