Axiom directed Focusing - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Pré-Publication, Document De Travail Année : 2008

Axiom directed Focusing

Résumé

Superdeduction is a focusing method especially designed to ease the use of first-order theories in predicate logic. Superdeduction modulo, which results of the combination of deduction modulo and superdeduction, enables then the user to make a distinct use of computational and reasoning axioms. Although soundness and completeness of superdeduction modulo are squarely ensured, it is not the case of cut-free superdeduction modulo since both deduction modulo and superdeduction may break cut-elimination. In this paper we prove the soundness and completeness of cut-free superdeduction modulo: we show that by using permutations of inference rules, any cut-free proof in deduction modulo can be transformed into a cut-free proof in superdeduction modulo and conversely. As a corollary we obtain that cut-elimination for deduction modulo (which is well-studied) is equivalent to cut-elimination for superdeduction modulo provided that some hypotheses on the synchrony of reasoning axioms are verified. Finally we propose a tableau method based on superdeduction modulo which is sound and complete provided that cut-elimination holds.
Fichier principal
Vignette du fichier
axiom_directed_focusing.pdf (300.66 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

inria-00212059 , version 1 (22-01-2008)
inria-00212059 , version 2 (10-04-2008)
inria-00212059 , version 3 (02-07-2008)

Identifiants

  • HAL Id : inria-00212059 , version 2

Citer

Clément Houtmann. Axiom directed Focusing. 2008. ⟨inria-00212059v2⟩
107 Consultations
181 Téléchargements

Partager

Gmail Facebook X LinkedIn More