Logique du premier ordre

Prolog

Florent Capelli

Programmation déclarative

Exemple : base de connaissances

mere(alice, bob).
pere(bob, carol).

parent(X,Y):-mere(X,Y).
parent(X,Y):-pere(X,Y).

gdparent(X,Y):-parent(X,Z),parent(Z,Y).
  • mere(alice,bob). mere est un prédicat binaire et (alice, bob) est dans mere.
  • pere(bob,carol). pere est un prédicat binaire et (bob, carol) est dans pere.
  • parent(X,Y):-pere(X,Y). ∀X∀Y.pere(X,Y) ⇒ parent(X,Y)
  • gdparent(X,Y):-parent(X,Z),parent(Z,Y). ∀X∀Y∃Z.parent(X,Z) ∧ parent(Z,Y) ⇒ gdparent(X,Y)

On définit une base de connaissances, aka une théorie!

Exemple : requête

mere(alice, bob).
pere(bob, carol).

parent(X,Y):-mere(X,Y).
parent(X,Y):-pere(X,Y).

gdparent(X,Y):-parent(X,Z),parent(Z,Y).
?- gdparent(A,B).
A = alice
B = carol
  • Requête gdparent(A,B): trouver les assignations à A = va, B = vb tel que pour tout modèle M de la théorie induite par le programme, (va,vb) ∈ gdparentM.

Convention Prolog: les variables commencent par une majuscule ou _, les atomes (prédicats, constantes) par une minuscule.

Exemple : récursion

parent(alice, bob).
parent(bob, carol).
parent(alice, david).
parent(bob, emily).
parent(francisca, grace).
parent(herbert, grace).

ancetre(X,Y):-parent(X,Y).
ancetre(X,Y):-parent(X,Z), ancetre(Z,Y).

Hypothèse du monde clos

chien(medor).
chien(rex).
?- chien(happy).
false.
?- chien(medor).
true.

Prolog ne considère que des modèles contenant des faits donnés dans la base de connaissances ou qu’on peut déduire de la base.

chien(X).
?- chien(happy).
true.
?- chien(medor).
true.

Exemple: symbole de fonction

Les entiers de Peano en Prolog (aka encodage de Church) : on a une constante z (zéro) et on peut construire les successeurs!

nat(z).
nat(s(X)):-nat(X).
pair(z).
pair(s(s(X))):-pair(X).

Comment définir les nombres impairs ?

impair(s(z)).
impair(s(s(X))):-impair(X).

Programmation déclarative

  • On évoque des faits et des relations entre les prédicats.
  • On laisse le programme inférer les relations.
  • Prolog contient beaucoup plus de choses que les exemples :
    • structure de données (listes, chaînes de caractères, entiers).
    • définition de fonctions
    • arithmétique
    • négation

Lien avec LPO

Clauses de Horn

Une base de connaissances en Prolog est un ensemble de formule de la forme:

∀x⃗(∃z⃗∧iPi(ti)) ⇒ Q(t)

où ti, t sont des termes sur les variables x⃗, z⃗.

C’est une clause de Horn.

  • Les règles gdparent(X,Y):-parent(X,Z),parent(Z,Y) doit se comprendre comme ∀X, Y(∃Z(parent(X,Z)∧parent(Z,Y)) ⇒ gdparent(X,Y)
  • Les faits chien(medor). sont des clauses de Horn un peu particulière où le membre de gauche est vide! C’est un sucre syntaxique pour chien(medor) :- ..
  • Une règle chien(X). se lira ∀X(chien(X)).

Répondre à une requête : formalisation

Base de connaissances :

  • B = {H1, …, Hk} : ensemble de clauses de Horn.
  • Contiennent des constantes C et des symboles de fonctions F.

Requête :

  • Une formule du premier ordre sans quantificateur Q(y⃗).
  • Énumérer les termes clos t1, …, tk tel que B ⊨ Q[y1:=t1,…,yk:=tk].
nat(z).
nat(s(X)):-nat(X).
pair(z).
pair(s(s(X))):-pair(X).
?- pair(s(X)).
X = s(z)
X = s(s(s(z)))
X = s(s(s(s(s(z))))).
...

L’unification : brique de base

r(f(X), f(f(X))). 
?- r(f(Y),Z).
  • Y=z, Z=f(f(z)) est une solution.
  • Y=f(z), Z=f(f(f(z))) aussi etc.
  • Solutions : tous les termes t, u tels que il existe un terme v avec
    • r(f(Y),Z)[Y:=t, Z:=u] = r(f(X), f(f(X)))[X:=v].

Problème très courant : l’unification !

Unification

Le problème

Étant donné deux termes t1, t2, est-ce qu’il existe une substitution de leurs variables σ telle que

t1[σ] = t2[σ].

Quiz!

Unifiez (ou pas) :

  1. x et f(y) {x := f(y)}, {x := f(a), y := a}…
  2. f(x) et g(y) Impossible ! Le premier commencera toujours pas f, le second par g
  3. x et f(x). Impossible ! Il faut compter le nombre de f !
  4. f(x) et f(g(y)) {x ↦ g(y)}
  5. f(x,x) et f(h(y),h(z)) {x ↦ h(y), z ↦ y}

Les bons unificateurs et les mauvais unificateurs

x et f(y) ont une infinité d’unificateurs : {x := fi + 1(a), y := fi(a)}

Quel sont les meilleurs?

σ1 := {x ↦ f(y)} σ2 := {x ↦ f(z), y ↦ z}

  • Ils sont idempotents: (t[σ])[σ] = t[σ]
  • Ils sont les plus généraux: tout unificateur σ tel que x[σ] = f(y)[σ] s’écrit σ′ ∘ σ1

Exemple:

  • σ := {x := f(f(a)), y := f(a)}
  • σ := {y := f(a)} ∘ σ1 car
    • x[σ1][y:=f(a)] = f(f(a)) = x[σ] et
    • y[σ1][y:=f(a)] = f(a) = y[σ].

Unificateurs les plus généraux (mgu)

  • Si t1, t2 peuvent être unifiés, alors il existe σ tel que :
    • σ est idempotent
    • σ est un unificateur le plus général (mgu), ie, tout unificateur σ′ s’écrit σ″ ∘ σ.

Comment trouver un tel σ ?

Algorithme d’unification

Problème plus général : étant donné (u1=?t1, …, un=?tn trouver σ tels que pour tout i ti[σ] = ui[σ]

  • Algorithme glouton d’application de règle :
    • si S contient g(v1,…,vk)=?f(w1,…,wp) avec f ≠ g: FAIL
    • si S contient x=?t avec x apparaît dans t et t ≠ x: FAIL
    • si S contient f(v1,…,vk)=?f(w1,…,wk), le remplacer par vi=?wi pour i = 1..k.
    • si S contient t=?t, l’enlever de S.
    • si S contient t=?x avec x une variable et t qui n’est pas une variable, remplacer par x=?t.
    • si S contient x=?t et que x n’apparaît pas dans t, remplacer toutes les occurences de x par t les autres termes.

Terminaison

Si les termes sont unifiables, l’algorithme précédent termine sans FAIL et donne un ensemble de la forme x1=?t1, …, xk=?tk.

{x1 ↦ t1, …, xk ↦ tk} est un mgu idempotent!

Exemple 1

Unifier f(h(y),h(z))=?f(x,x).

  • Déconstruire h(y)=?x, h(z)=?x.
  • Mettre la variable à gauche x=?h(y), h(z)=?x?
  • Remplacer: x=?h(y), h(z)=?h(y).
  • Déconstruire x=?h(y), z=?y.

x ↦ h(y), z ↦ y est un MGU!

Exemple 2

Unifier f(x,g(x))=?f(g(x),y).

  • Déconstruire x=?g(x), g(x)=?y.
  • FAIL

Les termes ne sont pas unifiables !

Amélioration

  • Fonctionne bien en pratique.
  • Complexité exponentielle cependant à cause de la substitution: x1=?f(x0,x0), x2=?f(x1,x1), …, xn + 1=?f(xn,xn)
  • Plusieurs algorithmes en temps linéaires existent en évitant de faire une substitution explicite.
    • Martelli and Montanari
    • Paterson & Wegman, etc.

Voir Chapitre 4, Terms rewriting and all that, Franz Baader, Tobias Nipkow.

Résolution et clauses de Horn

Rappel

On a des clauses de Horn H1, …, Hk en LPO :

  • P(t)
  • ∀x⃗(∃z⃗∧iPi(ti)) ⇒ Q(t⃗)

On a une requête (appelé GOAL) : G(y⃗) formule du première ordre.

On va simplifier : le but est une conjonction G1 ∧ … ∧ Gp de buts de la forme Ri(ti) où Ri est un prédicat et ti un terme.

Unifier pour résoudre

On veut trouver un terme satisfaisant un but G = R(t). Si on a :

  • Une clause de Horn H = (P1(t1)∧...∧Pk(tk)) ⇒ R(u).
  • Et t=?u a un unificateur σ.

En particulier, H[σ] ⇒ R[σ]

t[σ] est donc un modèle pour G si G1 := P1(t1[σ]), …, Gk := Pk(tk[σ]) ont un modèle.

On remplace donc le but G par des sous-buts G1, …, Gk jusqu’à n’avoir plus de but !

Si aucune clause de Horn ne peut être utilisée, on backtrack à la dernière fois où on a dû choisir une règle.

Exemple 1

pair(z).
pair(s(s(X))) :- pair(X).

BUT : pair(s(s(s(s(z))))).

  • pair(z) et pair(s(s(s(s(z))))).: pas unifiable
  • pair(s(s(X))) s’unifie avec pair(s(s(s(s(z))))) avec X := s(s(z)).
  • Nouveau but: pair(X)[X := s(s(z))] donc pair(s(s(z))).
  • pair(s(s(X))) s’unifie avec pair(s(s(z))) avec X := z.
  • Nouveau but: pair(z).
  • C’est un axiome, on a plus de but! Donc on retourne true.

Exemple 2

parent(alice, david). parent(alice, bob). parent(bob, carol). parent(bob, emily).

gdparent(X,Y):-parent(X,Z),parent(Z,Y).

BUT : gdparent(alice, C).

  1. gdparent(alice, C). s’unifie avec gdparent(X,Y) avec X := alice, Y:=C
  2. Nouveaux buts: parent(alice,Z), parent(Z,C).
  3. parent(alice,Z) s’unifie avec parent(alice, david) avec Z := david.
  4. Nouveau but: parent(david,C).
  5. parent(david,C) ne peut pas s’unifier ! Backtrack à 3!
  6. Buts : parent(alice,Z), parent(Z,C).
  7. parent(alice,Z) s’unifie avec parent(alice, bob) avec Z := bob.
  8. Nouveau but: parent(bob,C).
  9. parent(bob,C) s’unifie avec parent(bob, carol) avec C := carol! On a gagné!

Pour trouver tous les C, on peut backtracker encore sur 8 et remarquer que parent(bob,C) s’unifie avec parent(bob,emily)!

Règle de résolution

On a utilisé implicitement la règle de résolution :

A ⇒ B

A

B

Qui est complète pour la logique propositionnelle et aussi pour la logique du première ordre !

  • Au premier ordre, on autorise une substitution sur les variables universellement quantifiées !

∀x⃗(A⇒B)

A[x⃗:=σ]

B[σ]