1. Progression et objectifs
La semaine relie la logique étudiée précédemment à son automatisation. On part de connaissances exprimées en calcul des prédicats, on les transforme en clauses, puis on utilise une opération uniforme, la résolution, pour établir une conséquence par réfutation. Prolog fournit ensuite une traduction de ces connaissances et un moteur qui cherche les preuves à partir des faits, des règles et d’un but.
Le parcours est donc :
Code (text) · sélectionner pour copier
Énoncé et interprétation du problème
→ calcul des prédicats
→ forme clausale
→ preuve par résolution-réfutation
→ programme Prolog et requête
Il faut savoir appliquer le principe, construire ou expliquer une trace et reconnaître les substitutions. Le cours ne demande pas de démontrer le théorème qui fonde la résolution, ni de devenir expert de toutes les fonctions de Prolog. La récursivité et des possibilités plus avancées sont annoncées, mais aucun programme récursif n’est développé dans le matériel de cette semaine.
Les exercices donnent le niveau de difficulté attendu. La vidéo de conseils est une aide facultative si l’on sait déjà faire les exercices, tandis que pratiquer les conversions et les preuves reste recommandé. L’enseignante annonce des transformations en forme clausale à l’examen et apprécie les exercices où une trace fournie doit être justifiée. Cela indique une manière de se préparer, sans garantir que l’examen reproduira ces problèmes.
L’automatisation uniformise le mécanisme de preuve : on cherche des clauses et des substitutions compatibles, plutôt que choisir chaque fois une nouvelle règle d’inférence. Elle ne rend pas la logique du premier ordre décidable et ne garantit pas une terminaison pour tout problème. Cette précision corrige une confusion présente dans l’introduction et la conclusion des vidéos; elle est développée en §9.1.
Le cours rappelle aussi que les formalismes classiques ne suffisent pas à tous les besoins de représentation et de raisonnement, notamment statistiques. Il cite d’autres approches, dont les logiques floues, probabilistes et temporelles. La méthode étudiée convient à des connaissances et règles explicites; le choix d’un formalisme doit rester adapté au problème.