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.
Type de document :
Pré-publication, Document de travail
2007
Liste complète des métadonnées

Littérature citée [7 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00141720
Contributeur : Paul Brauner <>
Soumis le : vendredi 16 novembre 2007 - 11:16:01
Dernière modification le : jeudi 10 mai 2018 - 01:32:35
Document(s) archivé(s) le : vendredi 25 novembre 2016 - 17:11:14

Fichier

localisation.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

250

Téléchargements de fichiers

95