Soit F une formule atomique non close.Si une substitution ˇ est telle que l’instance Fˇ de F est une conséquence logique de P, alors ˇ est une réponse correcte à F. Si aucune instance de F n’est conséquence logique de P, alors “non” est la réponse correcte à F.
Répondre de manière correcte à une question F?, où F est une formule atomique non close, consiste à trouver toutes les instances Fˇ de F qui sont conséquences logiques de P. S’il existe de telles instances Fˇ, les réponses correctes sont les différentes substitutions ˇ, sinon la réponse correcte est non.
(Programmer en PROLOG, Jonathan Elbaz, Ellipses 1991, page 22)
Hé bé.