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

https://hal.inria.fr/inria-00141720
Contributor : Brauner Paul <>
Submitted on : Friday, November 16, 2007 - 11:16:01 AM
Last modification on : Friday, February 26, 2021 - 3:28:06 PM
Long-term archiving on: : Friday, November 25, 2016 - 5:11:14 PM

File

localisation.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00141720, version 3

Collections

Citation

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

Share

Metrics

Record views

449

Files downloads

202