Correction de conjectures fausses par synthèse de programmes
Dans le domaine de la vérification, les preuves ne terminent pas toujours avec succès, à cause des formules non prouvables. Parfois, le prouveur signale simplement l'échec. Cependant, dans certains cas il est intéressant de connaître la cause de cet échec et de la corriger. Les méthodes classiques sont insuffisantes pour qu'un prouveur détecte et corrige automatiquement les incohérences dans les programmes ou les formules logiques. Dans cet article, nous proposons une méthode permettant de corriger des formules fausses. Soit [...]
It's highlighted that when proving conjectures or synthesising programs, we are sometimes faced with unprovable conjectures. In general, a theorem prover will do nothing more but indicates the conjecture is false. However, in many cases it is hightly desirable to have an automated means for detecting and correcting faulty conjectures. Classical methods are not able to detect automatically unconsistancy in programs or conjectures. In this paper, we present a method for patching faulty conjetures. Let [...]
Prédicats de correction, synthèse de programmes, pliage, dépliage.
Corrective predicates, program synthesis, folding, unfolding.
Français
|
