zbMATH — the first resource for mathematics

Proof normalization modulo. (English) Zbl 0944.03052
Altenkirch, Thorsten (ed.) et al., Types for proofs and programs. International workshop, TYPES ’98. Kloster Irsee, Germany, March 27-31, 1999. Selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 1657, 62-77 (1999).
Summary: We consider a class of logical formalisms, in which first-order logic is extended by identifying propositions modulo a given congruence. We particularly focus on the case where this congruence is induced by a confluent and terminating rewrite system over the propositions. We show that this extension enhances the power of first-order logic and that various formalisms, including Church’s higher-order logic (HOL) can be described in our framework. We conjecture that proof normalization and logical consistency always hold over this class of formalisms, provided some minimal conditions over the rewrite system are fulfilled. We prove this conjecture for some subcases, including HOL.
For the entire collection see [Zbl 0929.00065].

03F05 Cut-elimination and normal-form theorems
03B35 Mechanization of proofs and logical operations
03B15 Higher-order logic; type theory (MSC2010)
03B10 Classical first-order logic