Prouvabilité et correction des formules implicatives - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2008

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.
Fichier principal
Vignette du fichier
pages-391-395-article24.pdf (188.03 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00293706 , version 1 (07-07-2008)

Identifiants

  • HAL Id : inria-00293706 , version 1

Citer

Rim Zarrad, Moussa Demba, Khaled Bsaïes. Prouvabilité et correction des formules implicatives. JFPC 2008- Quatrièmes Journées Francophones de Programmation par Contraintes, LINA - Université de Nantes - Ecole des Mines de Nantes, Jun 2008, Nantes, France. pp.391-395. ⟨inria-00293706⟩
103 Consultations
121 Téléchargements

Partager

Gmail Facebook X LinkedIn More