zbMATH — the first resource for mathematics

On constructive cut admissibility in Deduction Modulo. (English) Zbl 1178.03021
Altenkirch, Thorsten (ed.) et al., Types for proofs and programs. International workshop, TYPES 2006, Nottingham, UK, April 18–21, 2006. Revised selected papers. Berlin: Springer (ISBN 978-3-540-74463-4/pbk). Lecture Notes in Computer Science 4502, 33-47 (2007).
Summary: Deduction Modulo is a theoretical framework that allows the introduction of computational steps in deductive systems. This approach is well suited to automated theorem proving. We describe a proof-search method based upon tableaux for Gentzen’s intuitionistic LJ extended with rewrite rules on propositions and terms . We prove its completeness with respect to Kripke structures. We then give a soundness proof with respect to cut-free LJ modulo. This yields a constructive proof of semantic cut elimination, which we use to characterize the relation between tableaux methods and cut elimination in the intuitionistic case.
For the entire collection see [Zbl 1120.68001].

03B35 Mechanization of proofs and logical operations
03B20 Subsystems of classical logic (including intuitionistic logic)
03F05 Cut-elimination and normal-form theorems
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI