Implantation de l'algorithme de Stalmarck dans le cadre de la cooperation COQ/ELAN - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport Année : 2000

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

Hassen Kacem
  • Fonction : Auteur
  • PersonId : 835365
Constraints, automatic deduction and software properties proofs

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.

Domaines

Autre [cs.OH]

Publications Loria  : Connectez-vous pour contacter le contributeur

https://inria.hal.science/inria-00099219

Soumis le : mardi 26 septembre 2006-08:51:57

Dernière modification le : jeudi 15 février 2024-03:32:06

Fichier non déposé

Dates et versions

inria-00099219 , version 1 (26-09-2006)

Identifiants

  • HAL Id : inria-00099219 , version 1

Citer

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 XML-TEI Dublin Core DC Terms EndNote DataCite

Collections

UNIV-RENNES1 CNRS INRIA IRISA UNIV-LORRAINE INRIA2 LORIA LARA UR1-MATH-STIC UR1-UFR-ISTIC UNIV-RENNES UR1-MATH-NUM
72 Consultations
0 Téléchargements

Partager

Gmail Facebook X LinkedIn More