Normalization in Supernatural deduction and in Deduction modulo - Inria - Institut national de recherche en sciences et technologies du numérique Access content directly
Preprints, Working Papers, ... Year : 2007

Normalization in Supernatural deduction and in Deduction modulo

Abstract

Deduction modulo and Supernatural deduction are two extentions of predicate logic with computation rules. Whereas the application of computation rules in deduction modulo is transparent, these rules are used to build non-logical deduction rules in Supernatural deduction. In both cases, adding computation rules may jeopardize proof normalization, but various conditions have been given in both cases, so that normalization is preserved. We prove in this paper that normalization in Supernatural deduction and in Deduction modulo are equivalent, i.e. the set of computation rules for which one system strongly normalizes is the same as the set of computation rules for which the other is.
Fichier principal
Vignette du fichier
surded_modulo.pdf (167.14 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

inria-00141720 , version 1 (15-04-2007)
inria-00141720 , version 2 (16-11-2007)
inria-00141720 , version 3 (16-11-2007)

Identifiers

  • HAL Id : inria-00141720 , version 2

Cite

Paul Brauner, Gilles Dowek, Benjamin Wack. Normalization in Supernatural deduction and in Deduction modulo. 2007. ⟨inria-00141720v2⟩
283 View
129 Download

Share

Gmail Facebook X LinkedIn More