10. Acquis à maîtriser
À l’issue de cette semaine, pouvoir :
- distinguer atome, littéral, clause, base conjointe et clause de Horn;
- effectuer les neuf étapes, expliquer les étapes sans opération et justifier les dépendances de Skolem;
- distinguer variables locales, constante et terme composé, puis appliquer une substitution à toutes les occurrences concernées;
- préparer C∪{¬B}, construire des résolvantes et justifier chaque ligne jusqu’à la clause vide;
- donner la conclusion d’une preuve et utiliser un littéral de réponse pour conserver un témoin;
- traduire une règle simple en tête et corps Prolog, écrire les faits et poser des buts à variables communes;
- tracer les sous-buts, les liaisons et les choix de retour arrière;
- expliquer les six puis quatre réponses de Nathalie et le rôle exact de not(X=Z);
- résoudre les unifications, les questions de parcelles et les relations généalogiques de §8;
- distinguer preuve, correction et limites de terminaison, puis vérifier le sens des arguments d’un modèle.
La pratique active demandée est de réaliser les deux séries d’exercices et confronter les réponses aux solutions. Lire ce document ne constitue pas une attestation que les exercices, un examen ou une remise ont été réalisés personnellement.