Automating Theories in Intuitionistic Logic

Guillaume Burel 1, *
* Auteur correspondant
1 PAREO - Formal islands: foundations and applications
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Deduction modulo consists in applying the inference rules of a deductive system modulo a rewrite system over terms and formulae. This is equivalent to proving within a so-called compatible theory. Conversely, given a first-order theory, one may want to internalize it into a rewrite system that can be used in deduction modulo, in order to get an analytic deductive system for that theory. In a recent paper, we have shown how this can be done in classical logic. In intuitionistic logic, however, we show here not only that this may be impossible, but also that the set of theories that can be transformed into a rewrite system with an analytic sequent calculus modulo is not co-recursively enumerable. We nonetheless propose a procedure to transform a large class of theories into compatible rewrite systems. We then extend this class by working in conservative extensions, in particular using Skolemization.
Type de document :
Communication dans un congrès
Silvio Ghilardi and Roberto Sebastiani. 7th International Symposium on Frontiers of Combining Systems -FroCoS'09, Sep 2009, Trento, Italy. Springer, 5749, pp.181-197, 2009, Lecture Notes in Artificial Intelligence. 〈10.1007/978-3-642-04222-5_11〉
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00395934
Contributeur : Guillaume Burel <>
Soumis le : mardi 23 juin 2009 - 18:30:19
Dernière modification le : jeudi 11 janvier 2018 - 01:49:21
Document(s) archivé(s) le : samedi 26 novembre 2016 - 10:09:20

Fichiers

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

Identifiants

Collections

Citation

Guillaume Burel. Automating Theories in Intuitionistic Logic. Silvio Ghilardi and Roberto Sebastiani. 7th International Symposium on Frontiers of Combining Systems -FroCoS'09, Sep 2009, Trento, Italy. Springer, 5749, pp.181-197, 2009, Lecture Notes in Artificial Intelligence. 〈10.1007/978-3-642-04222-5_11〉. 〈inria-00395934v2〉

Partager

Métriques

Consultations de la notice

163

Téléchargements de fichiers

141