Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

A semantic method to prove strong normalization from weak normalization

Denis Cousineau 1, 2 
2 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : 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.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

Cited literature [17 references]  Display  Hide  Download
Contributor : Denis Cousineau Connect in order to contact the contributor
Submitted on : Tuesday, May 19, 2009 - 2:53:24 PM
Last modification on : Friday, February 4, 2022 - 3:17:00 AM
Long-term archiving on: : Monday, October 15, 2012 - 10:45:32 AM


Files produced by the author(s)


  • HAL Id : inria-00385520, version 1



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



Record views


Files downloads