Previous Up Next
Eléments de logique pour l’informatique 2021–22


Chapitre 4  Automatiser les démonstrations

Dans ce chapitre nous introduisons plusieurs techniques pour automatiser les démonstrations en calcul propositionnel et logique du premier ordre.

4.1  Peut-on automatiser les démonstrations ?

Automatiser les démonstrations consiste à trouver un algorithme qui étant donnée une formule quelconque va pouvoir répondre à la question est-ce que cette formule est valide ?

On a vu que ce problème était équivalent à trouver un algorithme qui, pour une formule quelconque, répond à la question est-ce que cette formule est satisfiable ? En effet la validité de la formule A est équivalente à l’insatisfiabilité de la formule ¬ A.

4.1.1  Décidabilité de la logique propositionnelle

Proposition 1   La validité d’une formule propositionnelle est une propriété décidable.

Preuve: Etant donnée une formule de la logique propositionnelle, elle a un nombre fini de variables, n. On peut calculer sa valeur de vérité pour chacune des 2n interprétations et en fonction du résultat, répondre à la question de la validité.

Evidemment la méthode donnée ci-dessus n’est pas efficace et d’autres techniques existent pour rendre plus effective la procédure. On pourrait se dire que la question de la satisfiabilité d’une formule (problème SAT) est plus simple puisqu’il suffit de trouver une interprétation qui rend vraie la formule. Or ce n’est pas le cas, le problème reste intrinsèquement dur. On rappelle les définitions liées à la NP-complétude dans le cas du problème SAT :

Proposition 2 (théorème de Cook, 71)   Le problème de satisfiabilité d’une formule est un problème NP-complet en le nombre de variables propositionnelles.

Preuve: La preuve du fait que le problème de satisfiabilité est NP-complet va constituer à ramener la résolution du problème NP à une question de satisfiabilité en logique propositionnelle, en faisant un codage logique de la machine de Turing qui résoud le problème initial.

On peut chercher des solutions plus efficaces pour des classes particulières de formules.

Si la formule est déjà en forme normale disjonctive, alors la satisfiabilité est immédiate car la formule est soit la formule donc insatisfiable soit de la forme CD avec C une conjonction élémentaire et cette conjonction élémentaire a un modèle qui est un modèle de la formule complète. La formule est donc satisfiable. Ce résultat associé au théorème de Cook implique que la complexité de la satisfiabilité se retrouve dans la complexité de mettre une formule quelconque en FND.

On a vu que l’on avait des méthodes linéaires pour ramener la satisfiabilité d’une formule à la satisfiabilité d’une formule en forme normale conjonctive. Cependant, même en se limitant à une formule en FNC dont les clauses propositionnelles ont au plus trois littéraux (problème dit 3-SAT), le problème SAT reste NP-complet.

4.1.2  Semi-décidabilité de la logique du premier ordre

Contrairement au cas propositionnel, dans le cas de la logique du premier ordre il y a une infinité d’interprétations possibles pour les symboles. On ne peut donc pas les énumérer toutes en général ou construire des tables de vérité.

Dans le cas des formules universelles (avec uniquement des quantificateurs universels en forme prénexe), le théorème de Herbrand nous permet de nous restreindre à une recherche parmi les modèles de Herbrand (interprétation sur le domaine des termes clos). Associé au théorème de compacité, il nous donne une méthode algorithmique pour savoir si une formule P (ou un ensemble de formules) est insatisfiable.

  1. mettre la formule P en forme de Skolem x1xn,A avec A sans quantificateur. La formule P est satisfiable si et seulement si x1xn,A est satisfiable.
  2. énumérer les instances closes de A : A1,…,An,… (en remplaçant les variables x1,…,xn par des termes clos), et pour chaque préfixe A1,…,Ap, utiliser une méthode propositionnelle pour tester la satisfiabilité :
    1. si A1,…,Ap est insatisfiable alors x1xn,A est insatisfiable (en effet dans une interprétation où x1xn,A est vrai, a fortiori toutes les instances A1,…,Ap sont aussi vraies).
    2. si A1,…,Ap est satisfiable et s’il n’existe pas de nouvelle instance close (cas où le domaine de Herbrand est fini) alors x1xn,A est satisfiable car l’interprétation qui rend vraies toutes les formules de A1,…,Ap définit un modèle de Herbrand dans lequel la formule x1xn,A est vraie.
    3. sinon on ajoute une nouvelle instance Ap+1 et on relance le problème

On peut établir les propriétés suivantes de l’algorithme :

On en déduit les résultats suivants :

Proposition 3 (Semi-décidabilité de la logique du premier-ordre)   

Preuve: Le premier résultat est une conséquence de l’algorithme présenté ci-dessus et le second en découle en utilisant le fait que tester la validité de A est équivalent à tester l’insatisfiabilité de la formule ¬ A.

On peut s’interroger sur la possibilité de faire mieux, c’est-à-dire de décider de la validité d’une formule. La réponse est négative.

Proposition 4 (Indécidabilité de la logique du premier-ordre)   Les problèmes de satisfiabilité ainsi que de validité d’une formule du calcul des prédicats sont indécidables.

Preuve: La preuve se fait en ramenant un problème indécidable comme l’arrêt d’une machine de Turing ou la correspondance de Post à un problème de validité en logique du premier ordre.

Exercice 1 (Logique et problème de Post)  

On prend comme problème indécidable la correspondance de Post. Soit un ensemble à deux éléments a et b appelés caractères, on appelle mot une suite finie de caractères. On note є le mot vide qui correspond à une suite sans caractères et on note par simple juxtaposition uv, la concaténation de deux mots. On se donne un ensemble fini de couples de mots {(u1,v1);…;(un,vn)}. Une correspondance de Post est une manière d’assembler ces paires de mots en une séquence (non vide) i1,…,ik pour que le mot ui1uik formé en regardant la première composante soit le même que le mot vi1vik formé en regardant la seconde composante.

Exemple. Soit le système S =def  {(a,baa); (ab,aa); (bba,bb)}.

Avec les notations que précédentes, on pose u1 =def  a, v1 =def  baa, u2 =def  ab, v2 =def  aa,u3 =def  bba, v3 =def  bb. Le mot u3u2u3u1=bba ab bba a est égal au mot v3v2v3v1=bb aa bb baa. On a donc bien une correspondance de Post pour ce système. Par contre si on regarde le système {(ab,aa); (bba,bb)} on montre qu’il n’y a pas de solution : en effet un tel mot solution ne peut pas commencer par (ab,aa) (car cela donne des mots dont la deuxième lettre diffère) ni par (bba,bb) car alors le premier mot sera toujours plus long que le second.

On peut prouver qu’un système particulier a ou n’a pas de solution mais on ne peut pas décider en général (à l’aide d’un programme) si un ensemble de couples de mots {(u1,v1);…;(un,vn)} admet une correspondance de Post.

Nous allons maintenant montrer comment on peut ramener ce problème a un problème logique.

Pour cela on considère un langage avec une constante e pour représenter le mot vide et deux symboles de fonction unaires a et b qui permettent l’ajout de la lettre a ou de la lettre b au début d’un mot. Ainsi le mot baa est représenté dans la logique par le terme b(a(a(e))). Le domaine de Herbrand (ensemble des termes clos) associé à ce langage correspond à l’ensemble des mots sur l’alphabet {a,b} dans le sens où on peut faire correspondre un terme à un mot et réciproquement.

On introduit également un prédicat binaire P et les formules suivantes :

  A0 
def
=
 
  P(e,e)
A1 
def
=
 
  ∀ x yP(x,y)⇒ P(a(x),b(a(a(y)))) 
A2 
def
=
 
  ∀ x yP(x,y)⇒ P(a(b(x)),a(a(y)))
A3 
def
=
 
  ∀ x yP(x,y)⇒ P(b(b(a(x))),b(b(y))) 

On remarque que l’axiome Ai correspond au couple (ui,vi) du problème de Post. On étudie le lien entre une solution au problème de Post et le fait que la formule x,P(a(x),a(x))∨ P(b(x),b(x)) est conséquence logique de A0, A1, A2, A3.

Pour cela on introduit une relation binaire sur l’ensemble des termes clos : uv si et seulement si il existe k≥ 0 et une séquence i1,…,ik (éventuellement vide) tels que le terme u correspond au mot ui1uik et le terme v correspond au mot vi1vik.

  1. Montrer que l’interprétation de Herbrand dans laquelle P(u,v) est vrai si et seulement si uv est un modèle des formules A0, A1, A2, A3.
  2. Montrer que si uv alors A0,A1,A2,A3P(u,v). On pourra raisonner par récurrence sur la taille de la séquence i1,…,ik.
  3. Montrer que A0 ⊨ ∃ x,P(x,x).
  4. Montrer que si le système S admet une solution pour le problème de correspondance de Post alors A0,A1,A2,A3⊨ ∃ x,(P(a(x),a(x))∨ P(b(x),b(x))).
  5. Sans utiliser le fait que l’on connait une solution pour le problème de Post du système S, montrer réciproquement que si A0,A1,A2,A3⊨ ∃ x,(P(a(x),a(x))∨ P(b(x),b(x))) alors le système de Post S admet une solution.

La preuve de semi-décidabilité nous a donné un algorithme naïf pour chercher une preuve d’une formule. En effet la méthode énumère au hasard l’ensemble des instances d’une formule et repose à chaque fois la question de la satisfiabilité. Pour améliorer cela, on peut chercher à engendrer des instances qui vont pouvoir interagir avec d’autres parties de la formule pour conduire à une contradiction.

Compétences 1  

4.2  Cas propositionnel

Dans cette section nous explorons plusieurs méthodes pour répondre à la question de la validité ou de la satisfiabilité d’une formule propositionnelle qui ne contient donc pour symboles que des variables propositionnelles et qui ne comporte pas de quantificateur.

4.2.1  Système G

Le système G est un calcul des séquents introduit au chapitre précédent (section 3.3.4).

Nous en rappelons les règles dans le cas propositionnel.

On a une règle “hypothèse(Hyp)

 
A,Γ ⊢ Δ,A 

et pour chaque connecteur, une règle gauche et une règle droite rappelées dans le tableau ci-dessous.

 gauchedroite 
 
⊥,Γ ⊢ Δ 
Γ ⊢ Δ 
Γ ⊢ Δ,⊥ 
Γ ⊢ Δ 
⊤,Γ ⊢ Δ 
 
Γ ⊢ Δ,⊤ 
¬
Γ ⊢ Δ,A 
¬ A,Γ ⊢ Δ 
A,Γ ⊢ Δ 
Γ ⊢ Δ,¬ A 
A,B,Γ ⊢ Δ 
A∧ B,Γ ⊢ Δ 
Γ ⊢ Δ,A    Γ ⊢ Δ,B 
Γ ⊢ Δ,A∧ B 
A,Γ ⊢ Δ    B,Γ ⊢ Δ 
A∨ B,Γ ⊢ Δ 
Γ ⊢ Δ,A,B 
Γ ⊢ Δ,A∨ B 
 ⇒
Γ ⊢ Δ,A    B,Γ ⊢ Δ 
A⇒ B,Γ ⊢ Δ 
A,Γ ⊢ Δ,B 
Γ ⊢ Δ,A⇒ B 
 

Ce système a de bonnes propriétés pour l’automatisation du raisonnement. En effet chaque séquent qui apparaît en prémisse d’une règle d’inférence contient moins de connecteurs logiques que celui qui est en conclusion et donc le processus qui consiste à appliquer les règles logiques s’arrête forcément.

On a vu aussi que toutes les règles étaient correctes et inversibles dans le sens qu’une interprétation rend vrai un séquent en conclusion d’une règle si et seulement si elle rend vrais tous les séquents qui apparaissent dans les prémisses.

En particulier, lorsqu’on construit un arbre de dérivation, si un nœud n’est pas valide, alors il existe une interprétation qui rend faux le séquent correspondant et on peut en déduire que la racine de la dérivation est également fausse pour cette interprétation. Et donc le séquent à la racine n’est pas valide. On en déduit une méthode de décision de la validité d’un séquent.

Proposition 1 (Validité d’un séquent)   Soit un arbre de dérivation suivant les règles du système G pour un séquent Γ ⊢ Δ dont les feuilles ne contiennent plus de connecteurs logiques.

Le séquent Γ ⊢ Δ est valide si et seulement si la règle hypothèse s’applique à chacune des feuilles.

Preuve: Si les feuilles A1,…,AnB1,…,Bp ne contiennent plus de connecteurs logiques, les formules A1,…,An,B1,…,Bp sont des variables propositionnelles.

Si toutes les feuilles sont des instances de la règle “hypothèse”, l’arbre peut être complété et la conclusion est alors valide.

S’il existe une feuille de l’arbre A1,…,AnB1,…,Bp qui n’est pas une instance de la règle “hypothèse” alors elle ne contient que des variables propositionnelles distinctes. On peut donc construire une interprétation qui rend vraies les variables Ai et fausses toutes les variables Bj. Comme les règles sont inversibles, le nœud qui est le parent de cette feuille est également faux dans cette interprétation. Et donc la racine de l’arbre qui est le séquent qui nous intéresse est faux dans cette interprétation. Ce séquent n’est pas valide.

Proposition 2 (Complétude du système G pour la logique propositionnelle)   Le système G est complet pour la logique propositionnelle, à savoir si le séquent Γ ⊢ Δ est valide alors Γ ⊢ Δ peut être prouvé par les règles du système G.

Preuve: Le résultat découle de la propriété 1. On montre la contraposée à savoir que si le séquent n’est pas prouvable alors il n’est pas valide. En effet, en décomposant tous les connecteurs, on peut toujours construire un arbre dont les feuilles sont uniquement composées de variables propositionnelles. Une des feuilles de cet arbre n’est pas une instance de la règle hypothèse (sinon le séquent serait prouvable) et donc par le résultat précédent, le séquent A1,…,AnB1,…,Bp n’est pas valide.

Exemple.

Soit la formule A ∨ (BC) ⇒ (AB) ∧ C. Un arbre de dérivation partiel est  :

d 
d 
 
 A ∨ (B ∧ C) ⊢ A ∨ B
         
g 
A ⊢ C
           B∧ C ⊢ C
 A ∨ (B ∧ C) ⊢ C
 A ∨ (B ∧ C) ⊢ (A ∨ B) ∧ C
  ⊢ A ∨ (B ∧ C) ⇒ (A ∨ B) ∧ C

On voit qu’une des feuilles AC n’est pas valide et donc on en déduit (sans finir la construction de l’arbre) que le séquent A ∨ (BC) ⇒ (AB) ∧ C n’est pas prouvable non plus.

Exercice 2 (Preuve à l’aide du système G)   En utilisant des arbres de dérivation dans le système G pour les formules suivantes, dire si elles sont valides ou non :
  1. ⊢ ((pq) ⇒ r) ⇒ (¬ pq) ⇒ (pr)
  2. ⊢ ((pq) ⇒ r) ∧ (¬ pq) ⇒ p

4.2.2  Résolution propositionnelle

Rappels.

Une clause est une disjonction de littéraux et peut se représenter par un ensemble de littéraux. Nous noterons une clause l1∨…∨ ln, chaque littéral apparaitra une seule fois et l’ordre est indifférent.

Le cas où cet ensemble est vide correspond à la proposition qui est toujours fausse.

Si la clause contient la formule ou contient une variable propositionnelle et sa négation, elle est toujours vraie (clause triviale). Nous nous intéressons à la satisfiabilité d’un ensemble de clauses, et une clause toujours vraie est satisfiable dans toutes les interprétations. Une clause triviale peut donc être retirée de l’ensemble considéré sans changer le problème (E est satisfiable si et seulement si E∪{⊤} est satisfiable). Une clause non triviale peut donc toujours se représenter par un ensemble de littéraux qui sont soit des variables propositionnelles soit des négations de variables propositionnelles et la même variable n’apparaît pas deux fois.

Règle de résolution.

On suppose donné un ensemble de clauses E. On cherche à savoir si ces clauses sont satisfiables, c’est-à-dire s’il existe une interprétation I telle que IE. La notation IE représente le fait que pour toute formule PE, on a IP.

Pour cela on va se donner un système de règles qui nous permet de dériver de nouvelles clauses C telle que si IE alors on a aussi IC. Le but du jeu est d’aboutir à la clause vide qui représente et qui est insatisfiable et donc d’en conclure que l’ensemble de clauses initial n’est pas satisfiable (il n’existe pas d’interprétation I telle que IE).

Définition 1 (Déduction par résolution)   Soit C et C deux clauses propositionnelles et p une variable propositionnelle, la règle de résolution a la forme suivante :
C ∨ ¬ p      C′∨ p
C∨ C
La notation CC construit la clause qui contient tous les littéraux de C et C en supprimant les doublons.

Soit E un ensemble de clauses, une déduction par résolution à partir de E est une suite de clauses C1,…,Cn telle que pour toute clause Ci dans cette suite soit CiE, soit il existe deux clauses Cj et Ck telles que j,k< i et telle que Ci soit le résultat de la règle de résolution appliquée à Cj et Ck.

C’est-à-dire que

Cj       Ck 
Ci 

est un cas particulier de

C ∨ ¬ p      C′∨ p 
C∨ C′ 

De manière équivalente, l’ensemble des clauses déductibles par résolution à partir d’une ensemble de clauses E est le plus petit ensemble qui contient les clauses de E et qui satisfait la condition associée à la règle de résolution vue comme une règle d’inférence.

Exemple 1 (Déduction par résolution)   On se donne l’ensemble E suivant p ∨ ¬ qr, ¬ r, p}. On peut faire les étapes de résolution suivantes (on a mis en indice de chaque règle la variable propositionnelle sur laquelle porte la résolution) :
(r) 
(p) ¬ p ∨ ¬ q ∨ r          p
 ¬ q ∨ r
           ¬ r
 ¬ q
On obtient la déduction par résolution suivante :
¬ p ∨ ¬ q ∨ rp, ¬ q ∨ r, ¬ r,¬ q
Définition 2 (Preuve par résolution)   
Exemple 2 (réfutation)   Soit l’ensemble E suivant p ∨ ¬ qr, ¬ r, p, q}. On peut construire une réfutation :
(q) 
(r) 
(p) ¬ p ∨ ¬ q ∨ r          p
 ¬ q ∨ r
           ¬ r
 ¬ q
          q
 
Exemple 3 (Preuve par résolution)   Soit A la formule définie comme ¬ (p ∨ (qr)) ⇒ (¬ q ∨ ¬ r). Pour faire une preuve par résolution de A, on met la formule ¬ A en forme clausale:
¬ (¬ (p ∨ (q ∧ r)) ⇒ (¬ q ∨ ¬ r)) ≡ ¬ (p ∨ (q ∧ r)) ∧  (q ∧ r) ≡ ¬ p ∧ (¬ q ∨ ¬ r) ∧  q ∧ r 
On a donc quatre clauses : p, (¬ q ∨ ¬ r),q,r}. On construit une réfutation de la manière suivante :
(q) 
(r) ¬ q ∨ ¬ r          r
 ¬ q
          q
 
La formule ¬ A est instatisfiable et donc la formule A est valide.
Exercice 3   Faire une réfutation par résolution de l’ensemble des formules {pqp∨¬ q,p∨ ¬ q, ¬ pq}.
Proposition 3 (Correction de la résolution)   Soit E un ensemble de clauses

Preuve:

Complétude

On peut se poser la question de savoir si la méthode de résolution peut toujours nous donner la solution. C’est-à-dire si on se donne un ensemble E de clauses insatisfiable, est-ce qu’il existe une réfutation de E par la méthode de résolution. La réponse est oui.

Proposition 4 (Complétude de la résolution propositionnelle)   Soit E un ensemble de clauses insatisfiable, alors il existe une réfutation par résolution de E.

Preuve: On va faire la preuve dans le cas où d’un nombre fini ou dénombrable de variables propositionnelles (pi)i∈ℕ.

On construit un arbre binaire de décision. Chaque niveau est étiqueté par une variable propositionnelle, en partant de p0, le sous-arbre gauche correspond au cas où cette variable vaut V et le sous-arbre droit, au cas où elle vaut F. Chaque branche (possiblement infinie) correspond donc à une interprétation logique des variables propositionnelles (pi)i∈ℕ.

Si on a juste deux variables p et q, l’arbre de décision se présentera ainsi (on a indiqué pour chaque sommet l’interprétation correspondante)

Chaque nœud interne de l’arbre correspond à une interprétation partielle des variables. Au niveau de la racine, aucune variable n’a de valeur.

Si l’ensemble E est insatisfiable alors pour chaque interprétation I, il existe une clause CE telle que IC. Comme C n’a qu’un nombre fini de variables, on peut positionner la formule dans l’arbre le plus haut possible telle que l’interprétation I restreinte à p0,…,pn rend faux la clause C. Il est possible de faire cela pour toutes les branches de l’arbre. On va appeler un tel arbre un arbre de réfutation de E.

Par exemple un arbre de réfutation pour l’ensemble de clauses {pq , p ∨ ¬ q, ¬ p} est :

Un arbre à branchement fini dont toutes les branches sont finies est lui-même fini (lemme de König). Donc on a un arbre fini, et chaque feuille contient une clause de E qui est fausse dans l’interprétation correspondant à la branche. Soit un arbre de réfuytation pour un ensemble E de clauses insatisfiable. Il se peut que cet arbre soit réduit à une feuille, celle-ci doit correspondre à une formule qui est fausse dans l’interprétation vide, il ne peut s’agir que de et donc ⊥∈ E et on a une réfutation triviale par résolution.

Si l’arbre n’est pas vide, on a un nœud de la forme avec p une variable propositionnelle et C et D des clauses. Soit I l’interprétation des variables autres que p qui correspond au chemin de la racine de l’arbre jusqu’à p. Attention I ne définit pas la valeur de toutes les variables propositionnelles, c’est seulement une interprétation partielle et donc toutes les clauses ne peuvent pas être évaluées dans cette interprétation.

On a I,{pV}⊭C et I,{pF}⊭D par définition des arbres de réfutation. La variable propositionnelle p apparait dans C et dans D (sinon on aurait pu faire remonter l’une de ces clauses plus haut dans l’arbre). On a forcément C=C′∨ ¬ p et D=D′∨ p (sinon les clauses seraient vraies à l’endroit où elles sont positionnées). Ce qui signifie que l’on peut faire une étape de résolution entre les deux clauses, qui nous donnera une clause C′∨ D telle que IC′∨ D. On peut donc remplacer le sous arbre [.p C D ] par la clause C′∨ D.

On voit donc qu’au fur et à mesure que l’on construit la déduction par résolution, on a un ensemble de clauses pour lequel l’arbre de réfutation diminue. Au final on aura un arbre réduit à une feuille ce qui correspond à une réfutation.

Evidemment cette démonstration n’est pas une manière effective de guider la recherche d’une réfutation par la méthode de résolution puisque si on avait l’arbre de réfutation on pourrait conclure immédiatement que l’ensemble de clauses est insatisfiable sans avoir recours à la résolution. Il faut parfois une peu d’intuition pour aboutir à la clause vide. Suivant la forme des clauses on peut avoir des stratégies plus précises.

Il se peut qu’en faisant une étape de résolution on trouve la clause triviale ou que l’on retombe sur une clause déjà connue. Cela ne signifie pas forcément que l’on s’est trompé ou que l’ensemble de clauses est satisfiable mais juste que les étapes de calcul faites étaient inutiles. Il faut alors chercher d’autres combinaisons ou s’interroger si l’ensemble de clauses de départ est bien insatisfiable.

4.2.3  Satisfiabilité

Il existe des méthodes qui, au lieu de chercher une contradiction dans un ensemble de clauses, vont au contraire chercher à construire une interprétation qui satisfait l’ensemble des clauses en collectant les contraintes sur les variables induites par ces clauses.

La procédure DPLL (du nom de ses inventeurs Davis, Putnam, Logemann et Loveland) permet de dire si une formule en forme normale conjonctive (représentée par un ensemble de clauses) est satisfiable. Pour cela, l’algorithme cherche à construire une interprétation qui rend la formule vraie.
L’algorithme DPLL travaille sur des problèmes de la forme : I ≫ Δ avec I une interprétation partielle des variables propositionnelles de la forme {x1b1;…;xnbn} (que l’on peut aussi représenter comme un ensemble de littéraux xi si bi=V et ¬ xi si bi=F) et Δ un ensemble de clauses C1,…,Cn. On note Δ,C le problème qui contient toutes les clauses de Δ plus la clause C. Le but de l’algorithme est de construire une interprétation qui étend I, c’est-à-dire de la forme {x1b1;…;xnbn;xn+1bn+1xpbp} et qui rend vraies toutes les clause Ci.

Les règles sont les suivantes :

Il y a deux cas triviaux. Le premier cas s’il n’y a plus de clauses, l’interprétation I répond au problème. Le second cas si l’une des clauses Ci est la clause vide alors le problème n’a pas de solution. Cela correspond aux deux règles :

Success
I≫ ∅
    Conflict
I≫ Δ,⊥

Par ailleurs on peut simplifier les problèmes : lorsque l’interprétation I fixe la valeur de la variable x, alors les clauses C qui contiennent un litteral l de la forme x ou ¬ x se simplifient :

Ceci est représenté par les deux règles suivantes :

BcpV
I ≫ Δ     I⊨ l
I≫ Δ,(l ∨ C)
    BcpF
I ≫ Δ,C     Il
I≫ Δ,(l ∨ C)

Maintenant si aucune des règles précédentes ne s’applique, alors il faut préciser l’interprétation en choisissant une valeur pour une nouvelle variable. Un cas simple est si une clause ne contient qu’un seul littéral alors pour que la clause soit vraie il faut choisir la valeur de la variable pour rendre ce littéral vrai. Ceci s’exprime par les règles suivantes :

AssumeV
I+{x↦ V}≫ Δ     xI
I≫ Δ,x
     AssumeF
I+{x↦ F}≫ Δ     xI
I≫ Δ,¬ x

Si maintenant, il n’y a aucune clause réduite à un littéral, alors il n’y a pas de choix évident. On va donc choisir une variable qui n’a pas encore de valeur et explorer les deux branches : celle où cette variable est interprétée par V et celle où elle est interprétée par F.

Unsat
I+{x↦ V} ≫ Δ     I+{x↦ F} ≫ Δ     xI
I≫ Δ

On part d’un ensemble de clauses Δ et d’une interprétation vide. On construit un arbre en utilisant les règles précédentes et on cherche à arriver à une feuille de succès de la forme I≫∅. L’interprétation I est une solution de notre problème, elle rend vraies l’ensemble des clauses Δ.

Si toutes les feuilles de l’arbre correspondent à des conflits alors l’ensemble de clauses initial n’est pas satisfiable.

Exercice 4  
  1. Appliquer l’algorithme précédent aux formules
    1. p ∨ ¬ q ∨ ¬ r) ∧ (¬ pqr) ∧ (pq ∨ ¬ r)
    2. (pr) ∧ (¬ qp) ∧ ¬ p ∧ ¬ r
  2. Justifier que la construction de l’arbre par les règles DPLL est toujours finie (trouver une quantité qui diminue le long des branches de l’arbre).
  3. Montrer que les règles de DPLL sont correctes. C’est-à-dire que si un arbre DPLL de racine I≫ Δ contient une feuille de succès J ≫ ∅ alors l’interprétation J étend l’interprétation I (c’est-à-dire que I(x)=J(x) pour toutes les variables x qui apparaissent dans I) et l’interprétation J rend vraies toutes les clauses de Δ.
  4. En déduire un méthode pour trouver un modèle d’une formule.
  5. A votre avis, la méthode est-elle complète, c’est-à-dire s’il existe un modèle est-on sûr de le trouver ? Peut-on trouver avec cette méthode tous les modèles d’une formule ?
Compétences 2  

4.3  Unification

On a vu que la question de la satisfiabilité nécessitait de produire des instances de formules, c’est-à-dire de remplacer des variables par des termes ayant de bonnes propriétés. Dans cette section, nous allons introduire un outil, l’unification, qui nous sera utile dans la méthode de résolution pour produire des instances particulières de formules. L’unification traite une classe de problèmes très simples à savoir des équations entre termes avec variables. C’est un problème qui a des applications multiples comme la question de l’inférence de types dans les langages fonctionnels.

L’unification est également l’ingrédient majeur des systèmes de réécritures qui sont des théories logiques dans lesquelles le seul symbole de prédicat est celui de l’égalité et les axiomes en plus de ceux de l’égalité sont de la ∀(t=u) de tels systèmes sont à la fois utilisés pour le raisonnement et comme langage de programmation.

4.3.1  Définitions

On se donne une signature F pour les termes et un ensemble X de variables. On rappelle qu’une substitution est une application σ ∈ XT(F,X). On s’intéresse à des substitutions dites à support fini c’est-à-dire telles que σ(x)=x sauf pour un nombre fini de variables. De telles substitutions se représentent facilement comme des ensembles finis {x← σ(x) | xX ∧ σ(x)≠x}. Ainsi, la substitution identité telle que σ(x)=x pour tout xX se représentera simplement par un ensemble vide {}.

Étant donnée une substitution, on a défini dans la section 1.5.3 une application de T(F,X)→ T(F,X) qui à un terme t associe le terme noté t[σ] dans lequel on a remplacé chaque variable x par σ(x).

Définition 1 (Composition de substitutions)   On peut composer deux substitutions σ1 et σ2 en une nouvelle substitution notée σ1σ2 définie par 1σ2)(x)=σ1(x)[σ2].
Pour tout terme
t : on a t1σ2]=(t1])[σ2].

D’un point de vue fonctionnel, la notation σ1σ2 correspond à appliquer la substitution σ1 suivie de σ2, ce qui d’un point de vue mathématiques correspond à la composition de fonctions σ2∘σ1

Remarque.

Il ne faut pas confondre la composition de deux substitutions qui correspond à deux substitutions successives avec la substitution simultanée. Ainsi si on pose σ1={xy} et σ2={yz}. On a σ1σ2={xz;yz} et (x+y)[σ1σ2]=z+z alors que la substitution simultanée est définie par {xy;yz} et donne le résultat (x+y)[xy;yz]=y+z.

Définition 2 (Problème d’unification)   Un problème d’unification est donné par deux termes avec variables t et u. Ce problème admet une solution s’il existe une substitution σ telle que t[σ]=u[σ]. On dira que σ est solution du problème t=? u, on dira aussi que σ est un unificateur des termes t et u ou encore qu’il unifie les termes t et u.

De manière plus générale, on peut se donner un ensemble de couples de termes {(ti,ui)|iI}. Résoudre ce problème d’unification revient à chercher une substitution σ telle que ti[σ]=ui[σ] pour tout iI.

Il s’agit de la résolution d’une équation (ou d’un système d’équations), on trouve des valeurs pour les variables qui apparaissent dans t et u, telles que si on remplace les variables par ces valeurs, alors les deux termes obtenus sont syntaxiquement égaux. On rappelle que les termes f(t1,…,tn) et g(u1,…,up) sont (syntaxiquement) égaux uniquement lorsque les symboles f et g sont égaux, on a alors la même arité donc p=n et on doit avoir récursivement ti=ui pour i=1… n.

Exemple 4   Si on se donne deux expressions sur la signature pour les nombres plus(x,0) et plus(y,z) une solution est {x← 0;y← 0; z← 0}. Une autre solution est {xy; z← 0}. Certaines équations n’ont pas de solution, par exemple plus(x,0) et 0 car on s’intéresse à une égalité syntaxique entre les termes et les symboles plus et 0 sont distincts.
Exercice 5   La signature sur les arbres est donnée avec la constante є et la fonction binaire N. Les problèmes d’unification suivants ont-ils des solutions ? si oui lesquelles ?
  1. N(x,є)=? N(є,y)
  2. N(N(x,y),є) =? N(є,y)
  3. N(x,є) =? x

4.3.2  Ensemble des solutions

Si σ1 est une solution du problème d’unification t=? u alors il en est de même de σ1σ2 pour toute substitution σ2. En effet on a t1]=u1] car σ1 est solution du problème et donc t1σ2]=t1][σ2]=u1][σ2]=u1σ2].

Si on a deux solutions σ et τ a notre problème d’unification, on dira que σ est plus générale que τ s’il existe une substitution σ′ telle que σσ′=τ.

Exemple 5   Si on reprend l’exemple 4, on a une solution σ =def  {xy; z← 0} et une solution τ =def  {x← 0;y← 0; z← 0}. On a τ=σ{y← 0} donc σ est plus général.

Une bonne propriété de l’unification sur les termes syntaxiques est que si un problème a une solution alors il existe une solution qui est plus générale que toutes les autres. Et donc pour calculer l’ensemble de toutes les solutions, il suffit de calculer cette substitution que l’on appelle aussi unificateur principal.

Proposition 1 (Unification, algorithme de Robinson)   Soit E={ti=? ui|iI} un problème d’unification. Si ce problème admet une solution, alors il existe un unificateur principal σ et celui-ci est calculé par la fonction suivante :

Preuve: On vérifie que chaque cas possible pour l’ensemble E est couvert par une équation unique : l’ensemble est soit vide soit il contient une équation et cette équation a son terme gauche qui est ou non une variable et si le terme gauche n’est pas une variable on regarde le cas où le terme droit est ou non une variable.

Un problème plus délicat à justifier est la terminaison de cette définition vue comme un procédé de calcul. Dans les cas récursifs, on regarde ce qui diminue :

En résumé pour un problème E si on regarde le triplet nbvars(E),taille(E),nbeqs(E) avec nbvars(E) le nombre de variables différentes dans E, taille(E) le nombre d’occurrences de symboles dans E, et nbeqs(E) le nombre d’équations dans E, alors on remarque que chaque appel se fait sur un problème strictement plus petit si on prend l’ordre lexicographique, sauf celui où on change l’équation t=x en x=t. Mais cette règle n’est appliquée que lorsque t n’est pas une variable et sera donc immédiatement suivie de l’application d’une règle qui fait diminuer le “poids” du problème. Une autre possibilité est de définir taille(t=? u) =def  2× nbsymb(t)+nbsymb(u) au lieu de taille(t=? u) =def  nbsymb(t)+nbsymb(u). On a alors taille(x=? t)<taille(t =? x) lorsque t n’est pas une variable.

On vérifie que les cas d’échec correspondent à des problèmes sans solution et que dans les cas où une solution est trouvée, il s’agit bien de l’unificateur principal.

Exercice 6   Soit g une fonction binaire, f une fonction unaire et a une constante. Résoudre les problèmes d’unification suivants :
  1. g(x,f(y))=? g(f(y),z)
  2. g(g(x,f(y)),z)=? g(g(y,z),a)

L’algorithme de Robinson est naturel mais n’est pas efficace à cause en particulier de l’opération de substitution lorsqu’on élimine l’équation x=? t. On peut utiliser une représentation des termes qui rend cette opération moins coûteuse. Il existe d’autres algorithmes plus complexes mais plus efficaces.

Autres applications de l’unification.

L’unification est une opération utilisée dans de nombreuses applications, par exemple dans l’algorithme de typage des programmes Ocaml afin de trouver le type le plus général que peut traiter une fonction. L’unification se généralise également à des théories plus complexes dans lesquelles l’égalité entre termes n’est plus syntaxique mais prend en compte des propriétés des opérations comme la commutativité ou l’associativité. Suivant les théories, on va perdre la décidabilité ou l’existence d’un unificateur principal.

Unification de littéraux.

L’unification sur les termes se généralise en une unification entre des littéraux. Si on a deux littéraux P et Q, ils s’unifient s’il existe une substitution σ telle que P[σ]=Q[σ]. Si P est de la forme R(t1,…,tn) (resp. ¬ R(t1,…,tn)) alors σ est un unificateur de P et Q si et seulement si Q est de la forme R(u1,…,un) (resp. ¬ R(u1,…,un)) et σ est un unificateur de l’ensemble de problèmes {ti=? ui|i=1… n}.

Exercice 7   Résoudre les problèmes d’unification suivants entre littéraux :
  1. (plus(x,0)≤ x)=? (plus(0,y)≤ y)
  2. (plus(x,0)≤ x)=? ¬ (yz)
  3. (plus(x,0)≤ x)=? (yplus(y,0))
Exercice 8   On se donne n termes t1,…,tn et on cherche à unifier ces n termes, c’est-à-dire trouver une substitution σ telle que t1[σ]=… =tn[σ].
On dispose d’un algorithme
unif qui donne l’unificateur principal de deux termes, comment peut-on procéder ?

4.3.3  Ordre sur les termes et filtrage

Définition 3 (Instance)   On définit un ordre sur les termes avec variables
t≤  u  
def
=
 
  il existe  σ  tel que  u=t[σ]

Si u=t[σ], on dit que t est plus général que u et que u est une instance de t.

Un terme avec variables tT(F,X) représente un ensemble de termes clos (sans variables), les instances closes de t:

inst(t
def
=
 
  {uT(F)|il existe  σ  tel que  u=t[σ]}
Proposition 2   Si tu alors inst(u)⊆ inst(t).

Preuve: Si tu alors u=t[σ] et toute instance close de u est de la forme u[τ]=t[σ][τ]=t[στ] et est donc une instance close de t.

Définition 4 (Filtrage, motif)   

Le langage Ocaml permet de définir une expression par cas suivant un ensemble de motifs

match e with 1 -> "un" | 2 -> "deux" | x -> "beaucoup" type form = Var of int | Bot | Neg of form | Bin of form * form let rec print_form e = match e with Var n -> string_of_int n | Bot -> "False" | Neg f -> "~"^(print_form f) | Bin(f,g) -> (print_form f)^"/\\"^(print_form g)

A l’exécution, e a pour valeur un terme clos (v)

On peut analyser les motifs

Exercice 9   On se donne une définition avec des motifs p1,…,pn, traduire les propriétés précédentes en conditions sur les ensembles inst(p1),…,inst(pn)
Compétences 3  

4.4  Résolution générale

On s’intéresse ici au problème de savoir si un ensemble de formules de la logique du premier ordre est satisfiable ou non, c’est-à-dire s’il existe une interprétation qui rend vraies simultanément toutes les formules. On rappelle qu’un ensemble fini de formules est satisfiable si et seulement si la conjonction de toutes les formules est elle-même une formule satisfiable. On a vu au chapitre 3 que l’on pouvait se ramener au cas où les formules manipulées sont uniquement des clauses (disjonction de littéraux), universellement quantifiées dans le cas de la logique du premier ordre.

La technique de preuve par résolution est importante car elle est à la base non seulement de systèmes de démonstration automatique mais aussi de systèmes de programmation logique. Le plus connu est le langage de programmation Prolog, dans lequel le programme est modélisé comme un ensemble de clauses et un calcul se fait par la recherche d’une preuve.

Nous avons traité le cas de la résolution en logique propositionnelle, nous voyons ici comment la méthode se généralise en logique du premier ordre.

4.4.1  Résolution au premier ordre

En logique propositionnelle, une clause est un ensemble de littéraux (variable propositionnelle ou négation de variable propositionnelle) et on se ramène au cas où chaque variable propositionnelle apparaît une seule fois.

Dans le cas du premier ordre, les littéraux sont de la forme R(t1,…,tn) ou ¬ R(t1,…,tn) avec R un symble de prédicat et ti des termes. Le même symboles peut donc apparaître plusieurs fois dans la clause de manière positive ou négative associée à des termes différents.

Par ailleurs les termes qui apparaissent dans les clauses peuvent contenir des variables. De fait une clause C qui contient les variables {x1,…,xn} est juste une représentation sans quantificateur de la formule ∀ (C) (notation pour x1 … xn,C).

Une autre interprétation de la clause avec variables C est l’ensemble des instances closes (sans variable) de la formule c’est-à-dire l’ensemble des clauses C0] avec σ0 une substitution qui remplace chaque variable de C par un terme clos. Le théorème de Herbrand nous a permis d’établir que la satisfiabilite de la formule ∀ (C) était équivalente à la satisfiabilité de l’ensemble (potentiellement infini) de toutes les instances closes de C. C’est ce qui est exploité dans la résolution au premier ordre.

On part d’un ensemble de clauses (disjonction de littéraux vue comme un ensemble de littéraux). On rappelle que l’unification sur les termes s’étend de manière naturelle à l’unification sur les littéraux. Deux littéraux L1 et L2 s’unifient s’ils sont de la forme R(t1,…,tn) et R(u1,…,un) ou bien ¬ R(t1,…,tn) et ¬ R(u1,…,un) et que le problème (ti=? ui)i=1… n admet une solution. Dans ce cas on note unif(L1,L2) l’unificateur principal.

Règles pour la résolution

Définition 1   La méthode de résolution en calcul des prédicats utilise trois règles qui manipulent des clauses :
  1. Factorisation : si σ est l’unificateur principal de L1 et L2, la règle de factorisation s’écrit :
    L1 ∨ L2 ∨ C
    L1[σ]∨ C[σ]
  2. Renommage : si σ est une bijection sur les variables, la règle de renommage s’écrit :
    C
    C[σ]
  3. Résolution binaire : si les clauses L1C et ¬ L2C n’ont pas de variables communes et si σ est l’unificateur principal de L1 et L2, la règle de résolution s’écrit :
    L1 ∨ C      ¬ L2 ∨ C
    C[σ]∨ C′[σ]
L’ensemble des clauses que l’on peut déduire par résolution à partir d’un ensemble de clauses E est le plus petit ensemble défini par les règles précédentes et qui contient E (et donc vérifie la règle
CE 
C 
).

Les définitions de réfutation par résolution et de preuve par résolution sont les mêmes que dans le cas propositionnel (définition 2) mais avec la notion de déduction par résolution générale.

Exemple 6   Soit l’ensemble de clauses P(x), ¬ P(y) ∨ Q(y), ¬ Q(a) avec P et Q deux symboles de prédicat unaires et a une constante.

On construit la déduction par résolution (on indique pour chaque règle la substitution qui est utilisée)

[xa] 
[yx] ¬ P(y) ∨ Q(y)            P(x)
 Q(x)
          ¬ Q(a)
 

La règle de renommage sert juste à préparer les clauses pour appliquer la règle de résolution dont une des conditions est que les deux clauses ne partagent pas de variable.

La règle de factorisation permet de faire disparaitre plusieurs littéraux lors d’une étape de résolution binaire. Elle est indispensable comme l’illustre l’exemple ci-dessous.

Ces deux règles sont triviales dans le cas propositionnel. La règle de résolution générale généralise la règle de résolution propositionnelle.

Exemple 7 (Règle de factorisation)   On souhaite montrer que l’ensemble {P(x,y)∨ P(y,x), ¬ P(u,z) ∨ ¬ P(z,u)} est insatisfiable. Si on applique la règle de résolution avec les formules P(x,y)∨ P(y,x) et ¬ P(u,z) ∨ ¬ P(z,u) alors on obtient
[xu,yz] P(x,y)∨ P(y,x)          ¬ P(u,z) ∨ ¬ P(z,u)
 P(z,u)∨ ¬ P(z,u)
qui est la clause triviale et donc n’aboutit pas à une contradiction.

Par contre, on peut commencer par effectuer des factorisations sur les deux clauses dont on déduit facilement une contradiction

[yu] 
[xy] P(x,y)∨ P(y,x)
 P(y,y)
              
¬ P(u,z) ∨ ¬ P(z,u) [zu]
¬ P(u,u) 
 
Exemple 8 (Preuve par résolution)   Soit A =def  ∃ x, ∀ y, (S(y)⇒ R(x)) ⇒ (S(x)⇒ R(y)). Pour prouver A, on fait une réfutation de la formule ¬ A.

On commence par mettre ¬ A en forme clausale.

On procède ensuite aux étapes de résolution en vue de produire la clause vide :

[xf(z)] 
[yf(x)] ¬ S(f(x))∨ R(x)           S(y)
 R(x)
          ¬ R(f(z))
 

On conclut : ¬ A est insatisfiable donc A est valide.

Exercice 10   En utilisant la résolution, montrer que
(∃ x,¬ P(x)), (∀ x,(P(x) ∨ Q(x)))⊨ ∃ xQ(x)

Propriétés de la résolution

La correction de la méthode de résolution établit que si l’on peut déduire une clause C à partir d’un ensemble de clauses E alors la formule ∀(C) est conséquence logique de l’ensemble des formules {∀ (D)|DE}.

On commence par établir quelques propriétés simples qui relient entre elles les clauses généralisées et leurs instances. Soient A et B deux formules, x une variable et t un terme.

Ces résultats se généralisent au cas de plusieurs formules et plusieurs variables. Si σ est une substitution alors ∀ (C) ⊨ C[σ] qui se déduit du lien entre substitution et vérité :

val(ρ,C[σ])=val({x↦ val(ρ,σ(x))|xVl(C)},C)

Par ailleurs si E est un ensemble de formules, si EB et si les variables libres de B ne sont pas libres dans les formules de E, alors E ⊨ ∀ (B).

Proposition 1 (Correction de la résolution)   Soit E un ensemble de clauses, chacune des étapes possibles de déduction par résolution produit une clause C telle que {∀ (D)|DE}⊨ ∀(C).

En particulier s’il existe une réfutation de E, alors {∀ (D)|DE}⊨ ⊥ et donc {∀ (D)|DE} est insatisfiable.

Preuve: On va montrer la correction de chacune des règles en montrant que la généralisation de la conclusion (clause sous la barre) est une conséquence logique de la généralisation des hypothèses (clause(s) au-dessus de la barre):

  1. Factorisation. Soit σ l’unificateur principal de L1 et L2, la règle de factorisation s’écrit 
    L1 ∨ L2 ∨ C
    L1[σ]∨ C[σ]
    On veut montrer ∀ (L1L2C) ⊨ ∀ (L1[σ]∨ C[σ]).
    On a
    ∀ (L1L2C) ⊨ L1[σ]∨ L2[σ]∨ C[σ] mais comme L1[σ]=L2[σ] (propriété de l’unificateur), on peut simplifier et on obtient ∀ (L1L2C) ⊨ L1[σ]∨ C[σ] puis ∀ (L1L2C) ⊨ ∀ (L1[σ]∨ C[σ]) car ∀ (L1L2C) ne contient pas de variable libre.
  2. Renommage. Si σ est une bijection sur les variables, la règle de renommage s’écrit
    C 
    C[σ] 
    .
    On a
    ∀ (C)≡∀ (C[σ]) (il s’agit d’une simple permutation des quantificateurs universels) d’où le résultat ∀ (C)⊨∀ (C[σ]) .
  3. Résolution binaire. Si σ est l’unificateur principal de L1 et L2, la règle de résolution s’écrit
    L1 ∨ C      ¬ L2 ∨ C
    C[σ]∨ C′[σ]
    On veut montrer ∀(L1C),∀(¬ L2C′)⊨ ∀(C[σ]∨ C′[σ]).
    On a
    ∀(L1C) ⊨ L1[σ]∨ C[σ] et ∀(¬ L2C′) ⊨ ¬ L2[σ]∨ C′[σ].
    On a
    L1[σ]=L2[σ] (propriété de l’unificateur) donc le même raisonnement que dans le cas propositionnel nous donne que L1[σ]∨ C[σ],¬ L2[σ]∨ C′[σ]⊨ C[σ]∨ C′[σ].
    Et donc
    ∀(L1C),∀(¬ L2C′)⊨ C[σ]∨ C′[σ] et finalement ∀(L1C),∀(¬ L2C′)⊨ ∀ (C[σ]∨ C′[σ]) car les variables libres de C[σ]∨ C′[σ] ne sont pas libres dans ∀(L1C),∀(¬ L2C′).

La méthode de résolution est aussi complète dans le cas de la logique du premier ordre, c’est-à-dire que si E est un ensemble de clauses et que est une conséquence logique de {∀(C)|CE} alors on peut déduire la clause vide par la méthode de résolution à partir de l’ensemble E.

Ce résultat utilise le Théorème de Herbrand et la compacité qui nous permettent d’établir qu’il existe un ensemble fini insatisfiable d’instances closes des clauses de E :

F={C11],…,Cnn]}

.

L’ensemble F est propositionnel, on peut donc par le théorème de complétude de la résolution propositionelle construire une réfutation par résolution de cet ensemble.

La clé de la preuve est ensuite le Lemme de relèvement qui permet d’établir que les étapes faites au niveau de la déduction propositionnelle peuvent se simuler au travers des règles de résolution au premier ordre.

Proposition 2 (Lemme de relèvement)   Soit C et D deux clauses du premier ordre sans variable commune. Si on peut faire une étape de résolution propositionnelle entre deux instances closes
C[σ]    D[σ]
P
alors il existe une clause E et une substitution τ telle que E peut être obtenu à partir des clauses C et D par des règles de résolution du premier ordre et P=E[τ].

Nous ne détaillerons pas la preuve ici. On pourra regarder plus précisément les points suivants.

  1. pourquoi peut-on utiliser la même substitution pour C et D?
  2. à quoi sert la règle de factorisation ? de renommage ?

4.4.2  Questions de stratégie

La méthode de résolution consiste à combiner des clauses dans le but d’obtenir la clause vide. Néanmoins il y a de nombreuses manières différentes de la faire et on peut s’interroger s’il existe des stratégies plus efficaces que d’autres.

Eliminer les clauses inutiles

Supposons qu’un des symboles de prédicat R n’apparaisse que de manière positive dans les clauses. Alors toutes les clauses dans lesquelles ce symbole apparaît peuvent être éliminées.

Exercice 11  
  1. Soit E un ensemble de clauses, tel que chacune des clauses contient au moins un littéral R(t1,…,tn) Montrer que E est satisfiable.
  2. Soit E un ensemble de clauses, qui ne contient aucun littéral négatif ¬ R(u1,…,un). Montrer que E est satisfiable si et seulement si l’ensemble {CE|C ne contient pas de littéral R(t1,…,tn)} est satisfiable.

Le même résultat s’applique si le symbole R n’apparait que de manière négative dans les clauses.

Il arrive que dans une dérivation, on puisse retomber sur une clause qui ressemble à une clause déjà rencontrée. Supposons qu’on ait à la fois une clause C et une clause C[σ]∨ D, alors la clause C[σ]∨ D peut être ignorée. En effet on a ∀(C)⊨ ∀ (C[σ]∨ D) donc E,∀(C),∀ (C[σ]∨ D)⊨ ⊥ si et seulement si E,∀(C)⊨ ⊥

Stratégie unitaire et clauses de Horn

Lorsque l’on combine deux clauses par la méthode de résolution, on peut obtenir en général une clause qui est aussi grosse voir plus grosse que les clauses dont on est parti. Sauf si une des deux clauses est composée d’un seul litteral (on dit que la clause est unitaire) auquel cas la clause obtenue après résolution est plus petite que la clause dont on était parti.

Malheureusement, la stratégie de choisir de faire toujours une résolution avec une clause réduite à un littéral ne fonctionne pas. En effet il y a des ensembles de clauses contradicatoires qui ne contiennent pas de clause unitaire et la stratégie de choisir toujours une clause unitaire peut nous amener à ne jamais considérer ces clauses. C’est ce qui se passe dans l’exemple suivant :

{P(a),¬ P(x)∨ P(f(x)),¬ p ∨ ¬ q,¬ p ∨ qp ∨ ¬ q,p∨ q}

La stratégie unitaire engendre un ensemble infini de clauses {P(f(a)),P(f(f(a))),…,P(fn(a)),…} qui ne mêne pas à une contradiction alors que l’ensemble p ∨ ¬ qpq, p ∨ ¬ q,pq} est lui insatisfiable (comme montré dans l’exercice 3).

Les clauses de Horn sont des cas particuliers de clauses qui contiennent au plus un seul littéral positif (sans négation). Les règles de la résolution appliquées à des clauses de Horn produisent des clauses de Horn.

L’intérêt des clauses de Horn réside dans le résultat suivant.

Proposition 3 (Résolution unitaire pour les clauses de Horn)   Soit S un ensemble de clauses de Horn, si S est insatisfiable, alors on peut dériver la clause vide en utilisant à chaque étape de résolution au moins une clause unitaire (résolution unitaire).

Preuve: La preuve suit les étapes suivantes

Application à la programmation logique

En 1972, l’informaticien Alain Colmerauer qui s’intéressait au traitement automatique des langues introduit, avec Philippe Roussel, le langage ProLog.

Le principe de base est de modéliser un problème à l’aide de Clauses de Horn.

Une clause avec un littéral positif p : ¬ p1∨ … ∨ ¬ pnp est écrite sous la forme p:- p1,…, pn. et peut se lire comme (p1∧ … ∧ pn) ⇒ p qui est bien équivalent à ¬ p1∨ … ∨ ¬ pnp

Lorsque la clause ne contient pas de littéral positif, elle s’écrira sous la forme :- p1,…, pn. et peut se lire comme (p1∧ … ∧ pn) ⇒ ⊥ qui est bien équivalent à ¬ p1∨ … ∨ ¬ pn ≡ ¬(p1∧ … ∧ pn).

Lorsque la clause est composée uniquement d’un littéral positif p, elle s’écrit simplement p.

Pour exécuter un programme, on va poser des questions sous la forme d’une conjonction de littéraux positifs qui peuvent contenir des variables.

Le système va rechercher les instances de ce programme qui sont conséquence logique des clauses du programme. Pour cela il va utiliser la méthode de résolution pour rechercher des contradictions à partir de la négation de ces prédicats.

Exemple 9   Une base qui modélise les relations de parenté peut se décrire avec les clauses suivantes.
1 fratrie(X,Y) :- parent(Z,X), parent(Z,Y), X \= Y. 2 parent(X,Y) :- pere(X,Y). 3 parent(X,Y) :- mere(X,Y). 4 pere(tom, sally). 5 pere(tom, erica).
Les questions que l’on peut poser sont ”est-ce que sally et erica sont dans la même fratrie” ou bien qui est dans la fratrie de sally. Cela se décrira en ProLog par les clauses suivantes :
?-fratrie(sally,erica). ?-fratrie(sally,x).
Supposons que la question soit
6 ?-fratrie(sally,erica).
Les seuls clauses unitaires sont les clauses 4 et 5. on peut combiner les clauses 2 et 4 ainsi que 2 et 5 pour obtenir les clauses unitaires suivantes :
7 parent(tom,sally). 8 parent(tom,erica).
On peut ensuite faire la résolution de la clause 1 avec ces clauses 7 puis 8 et on obtient
9 fratrie(sally,Y) :- parent(tom,Y), sally \= Y. 10 fratrie(sally,erica).
La contrainte sallyerica est résolue indépendament.
La clause 10 se combine alors avec la question 6 pour obtenir la clause vide ce qui établit le résultat.

Si maintenant la question est de chercher toutes les personnes dans la fratrie de sally, cela se traduit par :

6 ?-fratrie(sally,x).

il s’agit de trouver pour quelles valeurs de x ce problème a une solution. Les étapes vont être analogues

7 parent(tom,sally). 8 parent(tom,erica).
9 fratrie(sally,Y) :- parent(tom,Y), sally \= Y. 10 fratrie(sally,erica).

La clause 10 se combine alors avec la question 6 pour obtenir la clause vide au travers de la substitution xerica qui est renvoyée à l’utilisateur.

Ce langage a des applications en intelligence artificielle, linguistique, bases de données, etc.

Un important aspect est la possibilité de retour en arrière (back-tracking) après avoir trouvé une solution pour énumérer l’ensemble des instances possibles solutions du problème.

Compétences 4   Savoir effectuer une preuve par réfutation d’une formule arbitraire en appliquant toutes les étapes.

4.5  Calcul des séquents

Nous avons vu que le système G avait des bonnes propriétés dans le cas propositionnel. Au premier ordre, les règles g et d nécessitent de trouver le bon terme à appliquer et il peut aussi être nécessaire de les appliquer plus d’une fois sans que l’on puisse a priori borner cette recherche.

Le calcul des séquents est la base théorique des méthodes de démonstration automatique appelées méthodes des tableaux.

Le principal ingrédient est d’ajouter au langage des termes une nouvelle sorte de variables, les inconnues qui seront utilisées lors de l’application des règles g et d à la place du terme t à “deviner”. On décompose tous les connecteurs pour chercher des solutions au niveau des feuilles afin de pouvoir appliquer la règle axiome. Là encore c’est l’unification qui va nous permettre de trouver des solutions pour nos inconnues.

Les règles modifiées sont les suivantes, au lieu d’un terme quelconque, t nous remplaçons la variable liée par une “inconnue X :

(∀′ g
P[x← X],(∀ x,P),Γ ⊢ Δ 
(∀ x,P),Γ ⊢ Δ 
        (∃′ d)
Γ ⊢ Δ,(∃ x,P),P[x← X
Γ ⊢ Δ,(∃ x,P

Un arbre de dérivation qui contient des inconnues ne constitue pas une preuve. Il sera souvent incomplet car les inconnus peuvent empécher l’application de la règle hypothèse aux feuilles.

Exemple 10  
g (1) 
d (2) 
∀′ g 
 
∃′ d R(X,y),(∀ xR(x,y))⊢  (∃ y,R(x,y)),R(x,Y)
 R(X,y),(∀ xR(x,y))⊢  ∃ y,R(x,y)
 ∀ xR(x,y)⊢  ∃ y,R(x,y)
 ∀ xR(x,y)⊢  ∀ x, ∃ y,R(x,y)
 ∃ y, ∀ xR(x,y)⊢  ∀ x, ∃ y,R(x,y)

Pour que l’arbre puisse être complété par une règle hypothèse, on voit qu’il faut appliquer la substitution {Xx,Yy}

Une difficulté supplémentaire est que les règles droites pour le et gauche pour le ont des conditions sur les noms des variables ordinaires de termes; et que cela ajoute des contraintes sur les solutions pour les inconnues. Il faut donc vérifier que les solutions trouvées par l’unification respectent ces conditions. C’est le cas de l’exemple précédent, les règles g (1) qui introduit y et d (2) qui introduit x sont utilisées avant l’introduction d’inconnues et respectent la condition que les variables introduites ne sont pas utilisées ailleurs.

Si maintenant on essaie avec la même méthode de faire une preuve de la propriété réciproque.

∃′ d 
   
∀′ g 
g (1) 
 
d (2) R(X,y),(∀ x, ∃ y,R(x,y)) ⊢ (∃ y, ∀ xR(x,y)),R(x,Y)
 R(X,y),(∀ x, ∃ y,R(x,y)) ⊢ (∃ y, ∀ xR(x,y)),(∀ xR(x,Y))
 (∃ y,R(X,y)),(∀ x, ∃ y,R(x,y)) ⊢ (∃ y, ∀ xR(x,y)),(∀ xR(x,Y))
 ∀ x, ∃ y,R(x,y) ⊢ (∃ y, ∀ xR(x,y)),(∀ xR(x,Y))
 ∀ x, ∃ y,R(x,y) ⊢ ∃ y, ∀ xR(x,y)

Il est tentant de compléter la preuve comme précédemment en appliquant la substitution {Xx,Yy}. Cependant cela nous donnerait l’arbre suivant (pour ne pas alourdir l’arbre, on a retiré les formules dupliquées dans les règles d et g)

d 
   
g 
g (1) 
 
d (2) 
hyp  
 R(x,y) ⊢ R(x,y)
 R(x,y) ⊢ ∀ xR(x,y)
 ∃ y,R(x,y) ⊢ ∀ xR(x,y)
 ∀ x, ∃ y,R(x,y) ⊢ ∀ xR(x,y)
 ∀ x, ∃ y,R(x,y) ⊢ ∃ y, ∀ xR(x,y)

L’arbre n’a plus de feuilles mais ne constitue pas néanmoins un arbre de preuve (le séquent est d’ailleurs non valide). En effet la condition que y est une variable non utilisée dans la règle g (1) n’est pas vérifiée puisque y est libre dans la conclusion x, R(x,y) et de même la condition de la règle d (2) qui impose que x n’est pas utilisé par ailleurs n’est pas respectée puisque x est libre dans l’hypothèse R(x,y). On voit donc que l’utilisation des règles g et d va imposer des restrictions sur les variables qui peuvent être utilisées pour les valeurs des inconnues. Ces conditions devront être vérifiées globalement lorsqu’on cherche les solutions pour compléter les feuilles par des règles hypothèses.

4.6  Théories décidables

A propos de théories

Une théorie est un ensemble (fini ou infini) de formules closes. Une théorie peut se voir comme un ensemble de contraintes sur les symboles de la signature. Des exemples sont la théorie des ensembles, fondement des mathématiques modernes, l’arithmétique de Peano, cadre logique plus restreint mais qui permet de parler des fonctions calculables ou encore dans le cadre informatique des théories correspondant à des structures de données comme la théorie des piles.

Soit A une théorie, on s’intéresse aux formules qui sont vraies dans une théorie A, c’est-à-dire que toute interprétation qui satisfait les axiomes de la théorie, satisfait la formule P, ce qui est noté AP. La calcul des prédicats est indécidable en général mais certaines théories sont décidables.

Propriétés des théories

Soit une théorie A

Théories incomplètes

Beaucoup de théories sont incomplètes

Proposition 1 (Décidabilité des théories complètes)   Une théorie complète, récursive sur un ensemble dénombrable de symboles est décidable.

Preuve: Les preuves de AP peuvent être énumérées car la théorie est récursive et l’ensemble des symboles est dénombrable. On cherche en parallèle des preuves de AP et de A⊢ ¬ P, l’un des deux va aboutir.

Théorème d’incomplétude de Gödel
Proposition 2   Toute théorie non contradictoire qui contient l’arithmétique élémentaire PA0 n’est pas complète.

Il n’y a pas de théorie “universelle” (ex. théorie des ensembles) qui permette de montrer soit A soit ¬ A, pour toute formule.


Previous Up Next