Proof Normalization Modulo

Abstract : 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. This extension enhances the power of first-order logic and various formalisms, including higher-order logic, can be described in this 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 higher-order logic. At last, we extend these results to classical sequent calculus.
Type de document :
[Research Report] RR-3542, INRIA. 1998
Liste complète des métadonnées
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 11:58:45
Dernière modification le : vendredi 25 mai 2018 - 12:02:05
Document(s) archivé(s) le : dimanche 4 avril 2010 - 23:35:34



  • HAL Id : inria-00073143, version 1



Gilles Dowek, Benjamin Werner. Proof Normalization Modulo. [Research Report] RR-3542, INRIA. 1998. 〈inria-00073143〉



Consultations de la notice


Téléchargements de fichiers