Skip to Main content Skip to Navigation
Reports

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

https://hal.inria.fr/inria-00099219
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 8:51:57 AM
Last modification on : Friday, February 26, 2021 - 3:28:06 PM

Identifiers

  • HAL Id : inria-00099219, version 1

Collections

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⟩

Share

Metrics

Record views

150