A semantic method to prove strong normalization from weak normalization

Denis Cousineau (1, 2)

1 LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
2 TYPICAL - Types, Logic and computing

Deduction modulo is an extension of first-order predicate logic where axioms are replaced by rewrite rules and where many theories, such as arithmetic, simple type theory and some variants of set theory, can be expressed. An important question in deduction modulo is to find a condition of the theories that have the strong normalization property. In a previous paper we proposed a refinement of the notion of model for theories expressed in deduction modulo, in a way allowing not only to prove soundness, but also completeness: a theory has the strong normalization property if and only if it has a model of this form. In this paper, we present how we can use these techniques to prove that all weakly normalizing theories expressed in minimal deduction modulo, are strongly normalizing.

Mots clés: strong normalization; weak normalization; deduction modulo; proof theory; model theory

Domaines: Logique en informatique [cs.LO]

Denis Cousineau. A semantic method to prove strong normalization from weak normalization. 2009. ⟨inria-00385520⟩