Sequent Calculus Viewed Modulo

Eric Deplagne 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : The first-order sequent calculus is generally considered as containing no computation but only pure deduction. But this is not completely true if we look at it carefully, using a deduction modulo framework. The origins of the computational part are first implicit behaviours of the calculus, then well known consequences that we do not want to prove any more. We end up with a calculus fully in the spirit of deduction modulo.
Type de document :
Communication dans un congrès
Catherine Pilière. 12th European Summer School in Logic, Language & Information - ESSLLI'2000 Student Session, 2000, Birmingham, england, University of Birmingham, 11 p, 2000
Liste complète des métadonnées

https://hal.inria.fr/inria-00099056
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 08:48:51
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58
Document(s) archivé(s) le : mercredi 29 mars 2017 - 12:48:50

Fichiers

Identifiants

  • HAL Id : inria-00099056, version 1

Collections

Citation

Eric Deplagne. Sequent Calculus Viewed Modulo. Catherine Pilière. 12th European Summer School in Logic, Language & Information - ESSLLI'2000 Student Session, 2000, Birmingham, england, University of Birmingham, 11 p, 2000. 〈inria-00099056〉

Partager

Métriques

Consultations de la notice

82

Téléchargements de fichiers

37