Un calcul des séquents extensible

Paul Brauner 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Résumé : Ce rapport présente un calcul des séquents où les théories exprimées sous la forme de systèmes de réécriture sont traduites en règles ad hoc pour le calcul des séquents. Cela permet à la fois de réduire la taille des démonstrations en vue de la mise en oeuvre d'un assistant et de raisonner dans la théorie vide, ce qui ramène la preuve de la cohérence d'une théorie à une démonstration d'élimination des coupures dans le système de déduction dérivé de cette théorie. Le rapport expose différentes versions classiques et intuitionnistes du système, ainsi que l'ébauche d'un langage de termes de preuve. Après quelques exemples d'application du système, un prototype d'assistant à la démonstration fondé sur la version classique y est présenté.
Type de document :
Rapport
[Stage] 2006, pp.64
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00133578
Contributeur : Paul Brauner <>
Soumis le : lundi 26 février 2007 - 17:32:40
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58
Document(s) archivé(s) le : vendredi 21 septembre 2012 - 12:05:36

Fichiers

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

Identifiants

  • HAL Id : inria-00133578, version 1

Collections

Citation

Paul Brauner. Un calcul des séquents extensible. [Stage] 2006, pp.64. 〈inria-00133578〉

Partager

Métriques

Consultations de la notice

97

Téléchargements de fichiers

59