Implantation de l'algorithme de Stalmarck dans le cadre de la cooperation COQ/ELAN

Hassen Kacem 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Résumé : Il s'agit d'une implantation de l'algorithme de Stalmarck en ELAN en vue d'en faire une procedure de decision pour le compte du systeme de preuve COQ. l'algorithme de Stalmarck sert a tester la validite d'une formule propositionnelle. ELAN est un environnement pour specifier et prototyper des systemes de deduction, il se base sur le reecriture.
Mots-clés : réécriture stalmarck algorithm rewriting computational system tautology elan coq système de calcul tautologie algorithme de stalmarck
Type de document :
Rapport
[Stage] A00-R-359 || kacem00e, 2000, 76 p
Liste complète des métadonnées
https://hal.inria.fr/inria-00099219
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 08:51:57
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58

Identifiants

  • HAL Id : inria-00099219, version 1

Collections

INRIA | LARA | LORIA | UNIV-LORRAINE

Citation

Hassen Kacem. Implantation de l'algorithme de Stalmarck dans le cadre de la cooperation COQ/ELAN. [Stage] A00-R-359 || kacem00e, 2000, 76 p. 〈inria-00099219〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

117

Contact


archive-ouverte@inria.fr