HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

Normalization in Supernatural deduction and in Deduction modulo

Paul Brauner 1 Gilles Dowek 2 Benjamin Wack 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
2 LOGICAL - Logic and computing
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR8623
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.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

Cited literature [7 references]  Display  Hide  Download

Contributor : Brauner Paul Connect in order to contact the contributor
Submitted on : Friday, November 16, 2007 - 11:16:01 AM
Last modification on : Friday, February 4, 2022 - 3:23:47 AM
Long-term archiving on: : Friday, November 25, 2016 - 5:11:14 PM


Files produced by the author(s)


  • HAL Id : inria-00141720, version 3


Paul Brauner, Gilles Dowek, Benjamin Wack. Normalization in Supernatural deduction and in Deduction modulo. 2007. ⟨inria-00141720v3⟩



Record views


Files downloads