5. Preuves et interrogations travaillées

5. Preuves et interrogations travaillées

5.1 Propositionnel : prouver r

C={p,¬p∨q,¬q∨r}, B=r. La trace remonte de la négation du but :

Conclusion : r est déductible de C. Il serait aussi possible de dériver q depuis p, puis r depuis q, puis la contradiction avec ¬r. La justification de chaque ligne compte davantage que l’identité de l’ordre choisi avec celui du corrigé.

5.2 Variables : prouver une disjonction

La base est C={p(x)∨q(x,y), ¬p(a)∨r(b,z)}, avec a/b constantes. Le support écrit B=q(a,w)∨r(b,t) et fournit cette trace :

La quantification du but doit être explicite. Les clauses négatives à variables universelles correspondent à la négation d’un but existentiel. Si le but est ∀w∀t(q(a,w)∨r(b,t)), sa négation est ∃w∃t(¬q(a,w)∧¬r(b,t)), donc les lignes 3–4 deviennent ¬q(a,k1) et ¬r(b,k2), avec deux constantes nouvelles. La même preuve se ferme avec y↦k1, puis z↦k2.

On peut également résoudre directement les lignes 1 et 2 avec x↦a et obtenir q(a,y)∨r(b,z), universellement quantifiée. Cela confirme la conséquence universelle et montre pourquoi la portée des variables d’un but ne doit pas être laissée implicite lors de sa négation.

5.3 Charles et Marie : un but fermé

Dans cette base, pere(X,Y) et parent(X,Y) signifient que X est père/parent de Y :

C1 : pere(charles,marie)
C2 : parent(claude,julie)
C3 : ¬pere(x,y) ∨ parent(x,y)
B  : parent(charles,marie)

Le fait sur Claude et Julie n’est pas utilisé. Une preuve n’a pas à consommer toutes les connaissances disponibles. Conclusion : Charles est parent de Marie selon cette base.

5.4 Retrouver qui est parent de Marie

Un succès fermé ne donne pas forcément le témoin d’une question. Pour demander qui est parent de Marie, le cours ajoute un littéral de réponse :

La dernière clause conserve la valeur cherchée au lieu d’être vide. Prolog réalisera cette extraction en affichant les substitutions des variables de la requête, sans demander de coder reponse/1.

5.5 Etna : formalisation, témoin et quinze lignes

Les hypothèses sont : l’Etna dépasse en hauteur tous les volcans européens actifs; le Vésuve est un volcan italien actif de 1000 mètres; tout ce qui est italien est européen.

L’hypothèse générale fournie est :

∀x∀y∀z ((v(x) ∧ a(x) ∧ e(x) ∧ h(x,y) ∧ h(etna,z)) → d(z,y))

Elle donne une clause avec cinq conditions négatives et une conclusion positive. Les faits du Vésuve sont séparés en quatre clauses. La règle Italie→Europe devient ¬i(u)∨e(u).

La négation du but est donnée dans l’exercice :

∃t (h(etna,t) ∧ ¬d(t,1000))

Il ne faut pas la nier une deuxième fois. Son témoin devient une nouvelle constante k, appelée a dans le corrigé; k évite ici la confusion avec le prédicat a/1. Les deux clauses sont h(etna,k) et ¬d(k,1000).

Conclusion attendue : l’affirmation contraire conduit à une contradiction; la hauteur de l’Etna dépasse 1000 mètres selon la formalisation fournie.

Portée formelle : la négation donnée correspond au but ∀t(h(etna,t)→d(t,1000)). La preuve établit que toute hauteur associée à l’Etna dépasse 1000; l’existence d’une hauteur est implicite dans le problème naturel. Pour prouver séparément ∃t(h(etna,t)∧d(t,1000)) dans une base purement axiomatique, il faudrait aussi une hypothèse d’existence d’une hauteur. Cette distinction explique le rôle du témoin introduit par la négation donnée, sans changer la trace demandée.