9. Corrections et points de vigilance

9.1 Logique et preuves

Correction, complétude et terminaison sont distinctes. Un système peut avoir des règles saines sans fournir un algorithme de décision terminant sur toute entrée. Les affirmations de temps fini des vidéos ne constituent pas une garantie générale du premier ordre. Voir §1 et §4.3.
Skolem n’est pas une simple substitution par un objet existant. Employer un symbole nouveau, avec les bonnes dépendances; conserver les symboles entre clauses issues du même témoin. Voir §3.2–3.3.
Les variables sont locales aux clauses. L’exemple d’unification du support donne une instance spécialisée, pas la résolvante la plus générale. Renommer puis calculer les liaisons réellement imposées. Voir §4.2.
Nier un but exige sa quantification. Un but universel nié produit des témoins existentiels; un but existentiel nié produit des universels. La preuve de §5.2 et la négation donnée pour l’Etna illustrent pourquoi cette portée doit être explicite.
Clause vide et base vide ne signifient pas la même chose. La première est une contradiction; la seconde ne contient aucune exigence. Donner la conclusion de la preuve après la clause vide.
Une trace doit être cohérente dans ses noms. La ligne 7 du corrigé d’Arthur peut être lue avec un renommage implicite; la version de §5.6 choisit une substitution compatible avec le nom affiché.

La distinction entre preuve correcte et décision est corroborée par les notes de logique de Stanford; le cours sur la résolution explicite le renommage et la réfutation. Ces références servent à contrôler les précisions mathématiques; elles ne sont pas des lectures supplémentaires imposées par IFT-2003.

9.2 Prolog et modèles

parent/2 change d’orientation entre exemples. Lire sa convention avant de construire une règle; ne pas mélanger les deux programmes. Voir §6.5 et §8.4.
Le résultat W=julie de la petite console en page 11 du diaporama est erroné pour parent(nathalie,W). Les faits, l’arbre et la démonstration donnent Anne et Jimmy. Le lapsus « frère/sœur de Y » de la page 10 doit aussi se lire entre X et Z.
Le parent commun doit être le même. La portée des quantificateurs de la formule de fratrie du support gagne à être rendue explicite; §6.5 donne une formule cohérente avec le code.
Une règle simple n’encode pas automatiquement toutes les propriétés d’une relation naturelle. L’identité admise par la première fratrie est diagnostiquée et corrigée dans la démonstration. Les termes sexués nécessiteraient une information supplémentaire pour être établis formellement.
Valeur unique et preuve unique sont différentes. Deux parents communs donnent deux chemins même après exclusion de soi; la déduplication n’est pas automatique.
La négation par échec dépend de l’instanciation et de l’ordre. Le manuel SWI-Prolog de not/1 le décrit comme l’échec de preuve du but; la documentation pédagogique sur la négation par échec explique le rôle des variables. Le code du cours reste présenté avec not/1.
Échec logique, branche échouée, erreur et recherche infinie diffèrent. Une première incompatibilité peut être suivie d’une autre solution; une absence de résultat immédiat n’est pas une preuve de fausseté.