HAL - INRIA :: [inria-00141720, version 3] Normalization in Supernatural deduction and in Deduction modulo

inria-00141720, version 3

Normalization in Supernatural deduction and in Deduction modulo

Paul Brauner ()^a^, 1, Gilles Dowek ², Benjamin Wack^b^, 1

(2007)

Résumé : 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.

a – Institut National Polytechnique de Lorraine
b – ENS LYON
1 : PROTHEO (INRIA Lorraine - LORIA)
INRIA – CNRS : UMR7503 – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
2 : LOGICAL (INRIA Futurs)
INRIA – CNRS : UMR8623 – CNRS : FRE 2653 – Université Paris XI - Paris Sud – Polytechnique - X

inria-00141720, version 3
http://hal.inria.fr/inria-00141720
oai:hal.inria.fr:inria-00141720
Contributeur : Paul Brauner <>
Soumis le : Vendredi 16 Novembre 2007, 11:16:01
Dernière modification le : Vendredi 16 Novembre 2007, 11:17:43

Voir la fiche détaillée

Documents associés

PDF :

Exporter

Bibtex EndNote TEI RefWorks

<?xml version="1.0" encoding="UTF-8"?>
<listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML">
<listBibl type="article"><head>Documents sans référence de publication</head>
<biblStruct type="article" xml:id="inria-00141720"><analytic>
<author><persName><forename>Paul</forename><surname>Brauner</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Lorraine - LORIA</orgName>
<orgName type="team">PROTHEO</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : UMR7503</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
</author>
<author><persName><forename>Gilles</forename><surname>Dowek</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Futurs</orgName>
<orgName type="team">LOGICAL</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : UMR8623</orgName>
<orgName type="institution">CNRS : FRE 2653</orgName>
<orgName type="institution">Université Paris XI - Paris Sud</orgName>
<orgName type="institution">Polytechnique - X</orgName>
</affiliation>
</author>
<author><persName><forename>Benjamin</forename><surname>Wack</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Lorraine - LORIA</orgName>
<orgName type="team">PROTHEO</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : UMR7503</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
</author>
<title type="main" level="a">Normalization in Supernatural deduction and in Deduction modulo</title></analytic><monogr><imprint/></monogr><idno type="HALid">http://hal.inria.fr/inria-00141720</idno><idno type="HALFile">http://hal.inria.fr/inria-00141720/PDF/localisation.pdf</idno></biblStruct>
</listBibl>
</listBibl>