Logique du premier ordre

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)

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 = v_a, B = v_b tel que pour tout modèle M de la théorie induite par le programme, (v_a,v_b) ∈ gdparent^M.

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.

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

Clauses de Horn

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

∀x⃗(∃z⃗∧_iP_i(t_i)) ⇒ Q(t)

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

• 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

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

• Une formule du premier ordre sans quantificateur Q(y⃗).
• Énumérer les termes clos t₁, …, t_k tel que B ⊨ Q[y₁:=t₁,…,y_k:=t_k].

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].

Le problème

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

t₁[σ] = t₂[σ].

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 := f^i + 1(a), y := fⁱ(a)}

Unificateurs les plus généraux (mgu)

• Si t₁, t₂ 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 σ″ ∘ σ.

Algorithme d’unification

Problème plus général : étant donné (u₁=_?t₁, …, u_n=_?t_n trouver σ tels que pour tout i t_i[σ] = u_i[σ]

• Algorithme glouton d’application de règle :
  • si S contient g(v₁,…,v_k)=_?f(w₁,…,w_p) avec f ≠ g: FAIL
  • si S contient x=_?t avec x apparaît dans t et t ≠ x: FAIL
  • si S contient f(v₁,…,v_k)=_?f(w₁,…,w_k), le remplacer par v_i=_?w_i 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

Exemple 1

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

Exemple 2

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

Amélioration

• Fonctionne bien en pratique.
• Complexité exponentielle cependant à cause de la substitution: x₁=_?f(x₀,x₀), x₂=_?f(x₁,x₁), …, x_n + 1=_?f(x_n,x_n)
• 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.

Rappel

On a des clauses de Horn H₁, …, H_k en LPO :

• P(t)
• ∀x⃗(∃z⃗∧_iP_i(t_i)) ⇒ Q(t⃗)

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

Unifier pour résoudre

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

• Une clause de Horn H = (P₁(t₁)∧...∧P_k(t_k)) ⇒ R(u).
• Et t=_?u a un unificateur σ.

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

t[σ] est donc un modèle pour G si G₁ := P₁(t₁[σ]), …, G_k := P_k(t_k[σ]) ont un modèle.

Exemple 1

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

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

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).

Règle de résolution

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

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 !