8. Unification et preuves du premier ordre

8. Unification et preuves du premier ordre

8.1 Principe d'unification

Unifier deux expressions consiste à trouver une substitution qui les rend identiques. Une substitution est appliquée uniformément à toutes les occurrences de la variable.

Exemple : homme(x) s'unifie avec homme(Socrate) par {x := Socrate}. La même substitution transforme mortel(x) en mortel(Socrate).

Une unification échoue notamment lorsque :

• les symboles de prédicat ou de fonction à la même position diffèrent;
• les arités diffèrent;
• une constante devrait devenir un terme composé incompatible;
• une variable devrait contenir elle-même son propre terme — échec du contrôle d'occurrence.

8.2 Socrate

Prémisses :

• ∀x(homme(x)→mortel(x));
• homme(Socrate).

Après spécification universelle avec x := Socrate, on obtient homme(Socrate)→mortel(Socrate). Le modus ponens conclut mortel(Socrate).

8.3 Preuve de t(a,b)

Soit :

• E1 : ∀x∀y((p(x)∧q(y))→t(x,y));
• E2 : ∃y(r(y)∧∀z(s(z)→t(y,z)));
• E3 : ∀y(r(y)→q(y));
• E4 : ∀x∀y∀z((t(x,y)∧t(y,z))→t(x,z));
• E5 : p(a);
• E6 : s(b).

Progression :

1. Instancier E2 avec un témoin frais c : r(c)∧∀z(s(z)→t(c,z)).
2. Simplifier : r(c) et ∀z(s(z)→t(c,z)).
3. Instancier E3 avec c, puis modus ponens : q(c).
4. Conjoindre p(a) et q(c), instancier E1 avec x:=a, y:=c, puis modus ponens : t(a,c).
5. Instancier la seconde partie de E2 avec z:=b; avec s(b), obtenir t(c,b).
6. Conjoindre t(a,c) et t(c,b), instancier E4 avec x:=a, y:=c, z:=b, puis conclure t(a,b).

La logique du premier ordre est indécidable en général. La résolution est une procédure de preuve semi-décidable : avec une stratégie complète, une conséquence démontrable peut finir par être trouvée, mais l'absence de conséquence ne garantit pas toujours l'arrêt. La forme clausale ne transforme donc pas magiquement tous les problèmes en calculs toujours terminants.