On Constructive Cut Admissibility in Deduction Modulo

DOI10.1007/978-3-540-74464-1_3zbMath1178.03021OpenAlexW1607964314MaRDI QIDQ3612434

Richard Bonichon, Olivier Hermant

Publication date: 10 March 2009

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-74464-1_3

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items (3)

First-order automated reasoning with theories: when deduction modulo theory meets practice ⋮ Resolution is cut-free ⋮ Automating Theories in Intuitionistic Logic

This page was built for publication: On Constructive Cut Admissibility in Deduction Modulo