«Correction et complétude des sémantiques PLC revisitée par
(co-)induction»
Gérard Ferrand (LIFO,Orléans) et Alexandre Tessier (INRIA, Rocquencourt)
Résumé - Cet article propose une reformulation de la sémantique des programmes logiques avec contraintes en termes de sémantique positive et sémantique négative dans un cadre inductif uniforme. Dans ce cadre, les résultats de correction et complétude s'expriment de manière naturelle et élégante. En particulier, nous montrons un résultat de complétude de la sémantique négative en utilisant des ensembles infinis de contraintes. Ce cadre théorique est une extension originale de la «vision grammaticale de la programmation logique».
Mots clés - sémantique, programmation logique avec contraintes, correction, complétude, induction, co-induction.