Skip to Main content Skip to Navigation
Reports

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é.
Document type :
Reports
Complete list of metadatas

Cited literature [1 references]  Display  Hide  Download

https://hal.inria.fr/inria-00133578
Contributor : Brauner Paul <>
Submitted on : Monday, February 26, 2007 - 5:32:40 PM
Last modification on : Thursday, January 11, 2018 - 6:19:58 AM
Long-term archiving on: : Friday, September 21, 2012 - 12:05:36 PM

Files

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00133578, version 1

Collections

Citation

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

Share

Metrics

Record views

114

Files downloads

82