Prouvabilité et correction des formules implicatives

Résumé : Dans ce papier, nous proposons une méthode permettant d'étudier la prouvabilité des formules implicatives par analyse statique. Elle consiste à caractériser les formules et les programmes par des (in)équations mathématiques permettant de vérifier si une formule est satisfiable ou non sans effectuer le processus de preuve. Nous nous sommes aussi intéressés à la correction des formules fausses. En effet, nous proposons une méthode qui permet de synthétiser, pour une classe particulière de programmes et de formules implicatives, les prédicats de correction qui symbolisent les hypothèses manquantes à la formule pour qu'elle devienne vraie.
Type de document :
Communication dans un congrès
Gilles Trombettoni. JFPC 2008- Quatrièmes Journées Francophones de Programmation par Contraintes, Jun 2008, Nantes, France. pp.391-395, 2008
Liste complète des métadonnées

Littérature citée [7 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00293706
Contributeur : Service Ist Inria Sophia Antipolis-Méditerranée / I3s <>
Soumis le : lundi 7 juillet 2008 - 13:57:36
Dernière modification le : jeudi 10 juillet 2008 - 15:40:06
Document(s) archivé(s) le : vendredi 28 mai 2010 - 23:13:08

Fichier

pages-391-395-article24.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00293706, version 1

Collections

Citation

Rim Zarrad, Moussa Demba, Khaled Bsaïes. Prouvabilité et correction des formules implicatives. Gilles Trombettoni. JFPC 2008- Quatrièmes Journées Francophones de Programmation par Contraintes, Jun 2008, Nantes, France. pp.391-395, 2008. 〈inria-00293706〉

Partager

Métriques

Consultations de la notice

179

Téléchargements de fichiers

150