Previous Up Next
Eléments de logique pour l’informatique 2019–20                  http://www.lri.fr/~paulin/Logique


Chapitre 2  Logique propositionnelle classique

Dans cette section nous allons étudier plusieurs résultats de la logique propositionnelle, c’est-à-dire un fragment de la logique qui ne s’intéresse qu’aux connecteurs propositionnels , , , , , .

2.1  Syntaxe

La principale différence avec le langage introduit informellement dans la section précédente est l’introduction de variables propositionnelles dans le langage. Les variables propositionnelles sont juste des noms (on utilisera des lettres minuscules p, q, x, …) qui apparaissent dans la formule. On notera Vp l’ensemble des variables propositionnelles qui est a priori infini. Les variables propositionnelles sont considérées comme des formules atomiques.

Substitution.

Si P et Q sont des formules et x est une variable propositionnelle, on note P[xQ], le résultat du remplacement de la variable x par la formule Q dans la formule P.

La fonction de substitution peut être définie de manière récursive sur la structure de la formule :

x[x← Q]Q 
P[x← Q]PP est atomique Px
(¬ P)[x← Q]= ¬ (P[x← Q])
(P1 ∘  P2)[x← Q]= (P1[x← Q])  ∘  (P2[x← Q])∘ ∈{∧,∨,⇒,⇔}
Exemple 1   ((¬ xy) ∨ ¬ yx)[xpp]
Exercice 1   Définir de manière récursive la fonction qui calcule l’ensemble vars(P) des variables propositionnelles qui apparaissent dans la formule P.

2.2  Sémantique

On note B l’ensemble des booléens (appelés ainsi en l’honneur du logicien George Boole qui a, au 19ème siècle, proposé une vision algébrique et calculatoire de la logique).

L’ensemble des booléens est formé de deux éléments distincts que nous noterons V et F (parfois aussi notés 1 et 0).

Les booléens permettent d’interpréter une formule propositionnelle comme une valeur de vérité.

2.2.1  Modèle d’une formule propositionnelle

Pour interpréter une formule propositionnelle comme une valeur de vérité, il faut au préalable savoir comment on interprète les variables propositionnelles. En effet une variable propositionnelle est une inconnue donc peut très bien être remplacée par une proposition vraie ou une proposition fausse ou même par une formule qui comporte elle-même des variables propositionnelles et donc qui peut parfois prendre la valeur vraie et parfois la valeur faux.

Définition 1 (Interprétation)   Une interprétation est une fonction qui associe une valeur de vérité à chaque variable propositionnelle. C’est donc une fonction I Vp → B. On l’écrira sous la forme {p1b1,…,pnbn} avec pi Vp une variable propositionnelle et bi∈B la valeur booléenne V ou F correspondante.

Étant donnée une interprétation I, on peut calculer la valeur de vérité de n’importe quelle formule propositionnelle.

val(I,⊥)F 
val(I,⊤)V 
val(I,p)I(p)p  formule atomique 
val(I,¬ P)si val(I,P)=T alors F sinon V 
val(IP ∧ Q)si val(I,P)=V alors val(I,Qsinon F 
val(IP ∨ Q)si val(I,P)=V alors V sinon val(I,Q) 
val(IP ⇒ Q)si val(I,P)=V alors val(I,Qsinon V 
val(IP ⇔ Q)si val(I,P)=val(I,Qalors V sinon F 
Exemple 1   Soit la formule P définie comme ((xy) ⇒ x) ⇒ x et I l’interprétation {xF,yV}. On a val(I,xy)=V donc val(I,(xy) ⇒ x)=F et donc val(I,((xy) ⇒ x) ⇒ x)=V. Cette formule est en fait une tautologie (vraie pour toute interprétation).

La valeur d’une formule ne dépend que de la valeur de l’interprétation pour les variables qui apparaissent dans la formule. Si deux interprétations I1 et I2 coïncident (ont la même valeur) sur l’ensemble des variables propositionnelles d’une formule P alors val(I1,P)=val(I2,P).

Définition 2   Une formule P est valide si elle est vraie pour toute interprétation (on dit aussi que c’est une tautologie). Elle est satisfiable s’il existe une interprétation pour laquelle elle est vraie et elle est insatisfiable sinon, c’est-à-dire quand la formule est fausse quelle que soit l’interprétation.
On étend ces notions à un ensemble
E fini ou infini de formules:
Remarque.

Dire que deux formules P et Q sont valides est équivalent à dire que l’ensemble {P,Q} est valide. Par contre si deux formules sont satisfiables, cela ne veut pas dire que l’ensemble {P,Q} est satisfiable. Il suffit de prendre {xx} qui est insatisfiable car une interprétation I ne peut pas rendre vrai à la fois x et ¬ x alors que, pour chaque formule prise individuellement, on peut trouver une interprétation qui la rend vraie. Par contre si un ensemble de formules est satisfiable alors chaque formule individuellement est satisfiable. De manière duale si P et Q sont insatisfiables, il en est de même de l’ensemble {P,Q} mais le contraire n’est pas vrai, un ensemble de formules peut être insatisfiable alors que chaque formule individuellement est satisfiable.

Un ensemble de formules valide est a fortiori satisfiable. Comme la valeur d’une formule est vraie (resp. fausse) si et seulement si la valeur de sa négation est fausse (resp. vraie), on en déduit une correspondance entre validité et insatisfiabilité.

Proposition 1   La formule P est valide (resp. insatisfiable) si et seulement si la formule ¬ P est insatisfiable (resp. valide).
L’ensemble fini de formules
{A1,…,An} est valide (resp. satisfiable, resp. insatisfiable) si et seulement si la formule A1∧…∧ An est valide (resp. satisfiable, resp. insatisfiable)

Une formule propositionnelle fait apparaître seulement un nombre fini n de variables propositionnelle. Il y a 2n interprétations différentes pour ces variables propositionnelles, on peut donc connaître la validité d’une formule en calculant la valeur pour chacune de ces interprétations. Si on s’intéresse uniquement à la satisfiabilité, il suffit d’exhiber une interprétation pour laquelle la formule est vraie.

Définition 3 (Modèle d’une formule)   Un modèle d’une formule P est une interprétation I des variables de cette formule qui rend la formule vraie c’est-à-dire telle que val(I,P)=V.
On étend la notion de modèle à un ensemble de formules (fini ou infini)
E, I est un modèle si pour toute formule P E, on a val(I,P)=V.
Exemple 2   Soit la formule P définie comme ¬(xy) ⇒ ¬ y. L’interprétation {xV; yF} est un modèle, par contre {xF; yV} n’en est pas un.
Définition 4 (Conséquence logique )   On dira que P est une conséquence logique d’un ensemble de formules {A1,…,An} et on écrira A1,…,AnP si tout modèle de {A1,…,An} est aussi un modèle de P.
Proposition 2   Pour toutes formules A1,…,An et P, on a les propriétés suivantes:
Vérité et substitution.

Lorsque l’on fait une substitution dans une formule alors on restreint les interprétations possibles. Par exemple si on considère la formule x ∨ ¬ y on a 4 interprétations possibles pour les valeurs de x et de y et la formule est fausse pour l’interprétation xF, yV . Si on substitue x par zy, on obtient la formule (zy) ∨ ¬ y qui est une tautologie.

La validité et l’insatisfiabilité qui sont des propriétés de toutes les interprétations ne changent pas lorsque l’on effectue une substitution dans une formule, un ensemble de formules et ne change pas la notion de conséquence logique.

Les réciproques sont fausses, on peut avoir (cf l’exemple précédent) P[xQ] qui est valide sans que P le soit. La satisfiabilité simple n’est pas préservée, au contraire on a que si P[xQ] est satisfiable alors P est satisfiable mais le contraire est faux.

2.2.2  Équivalences booléennes

On utilise plusieurs connecteurs booléens mais il y a des équivalences entre ces connecteurs. On écrira PQ si PQ et QP ce qui revient aussi à dire que les valeurs de vérité de P et Q coïncident pour toute interprétation (i.e. I Vp →B, val(I,P)=val(I,Q)).

Lois algébriques.

L’ensemble des booléens avec les opérations de conjonction et de disjonction forme ce que l’on appelle une Algèbre de Boole.

Lois de de Morgan.

Les lois de de Morgan établissent le comportement de la négation par rapport aux autres connecteurs :

¬ ⊥ ≡ ⊤   ¬ ⊤ ≡ ⊥    ¬¬ P ≡ P    ¬(P∧ Q)≡ ¬ P ∨ ¬ Q     ¬(P∨ Q) ≡ ¬ P ∧ ¬ Q
Équivalence entre connecteurs.

Certains connecteurs peuvent se définir en fonction d’autres :

¬ P ≡ P ⇒ ⊥           P⇒ Q ≡ ¬ P ∨ Q          P⇔ Q ≡ (P ⇒ Q) ∧ (Q ⇒ P) ≡ (P ∧ Q) ∨ (¬ P ∧ ¬ Q)

2.3  Formes normales

Les équivalences mises en évidence ci-dessus montrent que la même propriété peut s’exprimer de plusieurs manières différentes. Cette redondance est intéressante pour l’expressivité (exprimer les notions le plus clairement possible en utilisant un vocabulaire riche) mais par contre peut être un frein au traitement informatique (comparaison, cas multiples à considérer).

On a par exemple déjà établi dans le paragraphe précédent que l’on pouvait se passer des connecteurs et en utilisant à la place les connecteurs ¬, et . On constate que dans le cas de l’équivalence, la formule transformée est deux fois plus grosse que la formule initiale, donc l’élimination du connecteur peut avoir un coût important.

Aussi on s’intéresse à établir qu’il existe des formes canoniques pour les formules propositionnelles.

2.3.1  Fonctions booléennes

De manière générale une formule P qui dépend de n variables propositionnelles p1,…,pn peut se voir comme une fonction booléenne à n arguments dans Bn→ B. C’est la fonction qui au n-uplet de booléens b1,…,bn associe la valeur boolénne val({pibi}i=1… n,P) correspondant à la valeur de vérité de la formule P dans l’interprétation qui associe la valeur b1 à la variable propositionnelle p1, la valeur b2 à la variable propositionnelle p2… On notera F(P) cette fonction.

Les notions de validité, satisfiabilité, insatisfiabilité d’une formule sont de fait des propriétés de la fonction booléenne associée : P est valide (resp. insatisfiable) si et seulement si F(P) est la fonction constante qui vaut T (resp. F). De même l’équivalence de deux formules correspond à l’égalité des fonctions booléennes associées, on a :

P≡ Q si et seulement si  F(P)= F(Q)

Une question naturelle est, étant donnée une fonction booléenne f quelconque à n arguments, peut-on trouver une formule propositionnelle P à n variables propositionnelles qui lui corresponde, c’est-à-dire telle que f= F(P).

La réponse est positive et même si on se restreint à des classes particulières de formules propositionnelles.

2.3.2  Forme normale de négation

Les lois de de Morgan rappelées dans la section 2.2.2 permettent de propager la négation vers les variables propositionnelles.

Définition 1 (Littéral)   On appelle littéral une formule qui est soit une formule atomique, soit la négation d’une formule atomique.
Proposition 1   Toute formule propositionnelle est équivalente à une formule propositionnelle qui ne comporte pas de connecteur ¬ sauf dans un littéral et n’utilise que les connecteurs ⊤,⊥,∨ et .

Une telle formule est dite en forme normale de négation.

Preuve: Pour résoudre ce problème, on construit deux fonctions de manière récursive : fnn (resp. neg) qui étant donnée une formule quelconque P, construit une formule en forme normale de négation équivalente à P (resp. équivalente à ¬ P).

fnn(P)PP  atomique
 fnn(¬ P)neg(P
 fnn(P∘ Q)fnn(P)∘ fnn(Q)∘ ∈ {∨,∧}
 fnn(P⇒ Q)neg(P)∨ fnn(Q)  
 fnn(P⇔ Q)= ( fnn(P)∧ fnn(Q))∨( neg(P)∧ neg(Q)) neg(⊤)= ⊥ 
neg(⊥)= ⊤ 
neg(x)= ¬ xx  variable propositionnelle
 neg(¬ P)fnn(P
neg(P ∧ Q)neg(P) ∨ neg(Q)
neg(P ∨ Q)neg(P) ∧ neg(Q)
neg(P ⇒ Q)fnn(P) ∧ neg(Q)
neg(P ⇔ Q)= ( fnn(P)∧ neg(Q))∨( neg(P)∧ fnn(Q))

On montre ensuite par récurrence sur la formule que fnn(P) et neg(P) sont en forme normale de négation et que de plus fnn(P)≡ P et neg(P)≡ ¬ P

Exemple 1   Soit la formule ((pq) ⇒ p) ⇒ p dans laquelle on élimine les implications, cette formule devient : ¬ (¬ (¬ pq) ∨ p) ∨ p. On peut ensuite repousser les négations en commençant par l’extérieur:
On obtient la formule : ((¬ pq) ∧ ¬ p)) ∨ p qui peut se simplifier en ¬ pp puis en .

2.3.3  Forme normale conjonctive

Définition 2 (Clause)   On appelle clause une formule propositionnelle qui n’utilise que des littéraux et la disjonction.

Comme la disjonction est associative et commutative, la clause peut toujours s’écrire de la forme l1l2∨… ∨ ln avec li un littéral et on peut réarranger les littéraux dans l’ordre que l’on veut (par exemple en ordonnant les variables propositionnelles, puis pour chaque variable en mettant d’abord les littéraux positifs puis les négatifs). Par ailleurs, on a PPP et P∨ ¬ P≡ ⊤.

On peut se ramener à une clause dans laquelle chaque variable propositionnelle apparaît au plus une fois sous forme positive ou négative.

Proposition 2   Une clause est équivalente à ou bien à une clause qui est une disjonction de variables propositionnelles (simples ou niées) dans laquelle chaque variable apparaît au plus une fois.

Preuve: Si une variable propositionnelle p apparaît deux fois sous forme positive ou deux fois sous forme négative, alors en utilisant PPP on peut retirer une des occurrences sans changer la valeur de la formule. Si une variable propositionnelle apparaît une fois sous forme positive et une fois sous forme négative alors, en utilisant p∨ ¬ p ≡ ⊤, on peut remplacer ces deux occurrences par la formule . Une clause qui contient est simplement équivalente à .

Une clause est donc caractérisée par un ensemble de variables propositionnelles, chacune associée à une polarité pour indiquer si elle apparaît en position positive ou négative.
Par convention, la clause associée à un ensemble vide de littéraux est interprétée comme la formule fausse .

Proposition 3   Soient L1 et L2 des ensembles de littéraux, si L1L2 alors la clause correspondant à L2 est une conséquence logique de la clause correspondant à L1.

Preuve: Si L1 est un ensemble vide alors la clause correspondante est et toute propriété est conséquence logique de . Sinon soit C1 (resp. C2, resp. C3) la clause correspondant à L1 (resp. L2, resp. L2L1). On a C2C1C3 et donc comme C1C3 est une conséquence logique de C1, on en déduit que C2 est une conséquence logique de C1.

Définition 3 (Forme normale conjonctive)   Une formule est dite en forme normale conjonctive si elle s’écrit comme une conjonction de clauses. Par convention, la conjonction d’un ensemble vide de formules est interprétée comme la formule vraie .
Proposition 4   Toute formule P admet une forme normale conjonctive, c’est-à-dire qu’il existe une formule Q équivalente à P et qui est en forme normale conjonctive.

Pour démontrer ce résultat, nous allons utiliser une autre propriété qui dit que toute fonction booléenne f à n arguments peut être associée a une formule Q en forme normale conjonctive telle que f= F(Q). En appliquant ce résultat à la fonction booléenne F(P) associée à P, on aura démontré le résultat de la proposition 4.

Proposition 5   Pour toute fonction booléenne f à n arguments, on peut trouver une formule Q en forme normale conjonctive telle que f= F(Q).

Preuve: On s’intéresse à l’ensemble Z des n-uplets pour lesquels la fonction f est fausse, c’est-à-dire

Z 
def
=
 
  {(b1,…,bn) | f(b1,…,bn)=F}

Dans la table de vérité, il suffit de s’intéresser aux lignes où la valeur de la formule est F. L’ensemble Z est fini. Si cet ensemble est vide alors f= F(⊤) qui est en forme normale conjonctive. On cherche une formule propositionnelle Q qui dépend des variables p1,…,pn correspondant à f. La variable propositionnelle pi correspond à la propriété “le i-ème argument de f est vrai”. La propriété Q doit être vraie lorsque la fonction est vraie et donc doit exprimer que les arguments ne sont pas dans Z. Pour un élément (b1,…,bn), la formule qui dit que les arguments ne correspondent pas à cette valeur est l1l2 ∨ … ∨ ln avec li=pi si bi=F et lipi si bi=V. Cette formule est une clause. Il suffit ensuite de prendre la conjonction des clauses pour chaque élément de Z.

Exemple 2   Soit la formule P =def  (pq) ⇒ (¬ pq), on commence par écrire la table de vérité :
 pq¬ p ∧ qp ⇒ q(p ⇒ q) ⇒ (¬ p ∧ q)
VVFVF  
VFFFV  
FVVVV 
FFFVF 
Les lignes qui nous intéressent sont la première et la dernière et on doit exprimer une formule qui dit exactement que l’on n’est pas dans un de ces deux cas.

La formule qui dit que l’on n’est pas dans le cas de la ligne 1 est ¬ p ∨ ¬ q et la formule qui dit que l’on n’est pas dans le cas de la ligne 4 est pq.

La forme normale conjonctive est donc p ∨ ¬ q) ∧ (pq).

2.3.4  Forme normale disjonctive

On définit de manière duale la notion de forme normale disjonctive.

Définition 4 (Forme normale disjonctive)  
Proposition 6   Pour toute formule propositionnelle P, il existe une formule Q équivalente en forme normale disjonctive.

Preuve: Comme précédemment, on peut construire la table de vérité de la formule P par rapport aux variables propositionnelles {p1,…,pn}. On s’intéresse à l’ensemble O des n-uplets (b1,…,bn), pour lesquels la table de vérité donne la valeur vrai. Pour chaque ligne on construit une conjonction élémentaire l1l2 ∧ … ∧ ln avec li=pi si bi=V et lipi si bi=F. Il suffit ensuite de prendre la disjonction de ces formules pour trouver une formule équivalente à P.

Exemple 3   En reprenant la formule P de l’exemple 2, on obtient la forme normale disjonctive :
(p∧ ¬ q) ∨ (¬ p ∧ q)

Si une formule est en forme normale disjonctive alors il est facile de trouver un modèle. On suppose que les branches de la disjonction sont en forme “simplifiée” c’est-à-dire qu’une variable propositionnelle apparaît dans un seul littéral. Il suffit de choisir une des branches de la disjonction. Pour chaque variable propositionnelle x qui apparaît dans un littéral l on prend dans le modèle xV si l=x et xF si lx. Il peut arriver qu’il n’y ait aucune composante en forme simplifiée: c’est le cas où la formule initiale est équivalente à et donc il n’y a pas de modèle.

Cependant, la mise en forme normale n’est pas forcément la meilleure manière de trouver un modèle. En effet, cette forme normale peut être exponentiellement plus grosse que la formule initiale. C’est le cas par exemple de la formule (a1b1) ∧…∧ (anbn) qui a 2n variables et 2n−1 connecteurs. La forme normale disjonctive s’écrit xi∈{ai,bi}(x1∧… ∧ xn). Il y a donc 2n disjonctions.

2.4  Systèmes déductifs

On s’intéresse maintenant à la possibilité de déduire de manière syntaxique qu’une formule P est une conséquence logique d’un ensemble de formules E, c’est-à-dire que la formule P sera vraie dans toute interprétation qui rend les formules de E vraies.

2.4.1  Préliminaires

On a vu au chapitre 1 un système de preuves particulier pour faire des déductions. Une relation A1,…,AnP est introduite pour représenter le relation être prouvable et des règles d’inférence permettent de construire une justification de la validité du jugement. En restreignant les règles de déduction aux connecteurs propositionnels et en considérant la règle de raisonnement classique par l’absurde, on a un système de preuve qui est correct et complet pour le calcul propositionnel. C’est-à-dire qu’il y a équivalence entre A1,…,AnP et l’existence d’une justification de A1,…,AnP

Règles d’inférence

Les règles d’inférence sont une manière de définir une relation R qui est très utile en informatique théorique.

Elles se présentent sous la forme de fraction :

P1… Pk
R(t1,…,tn)

Le dénominateur (aussi appelé la conclusion de la règle) est forcément un cas particulier de la relation que l’on cherche à définir. Le numérateur contient un nombre quelconque de conditions (que l’on appelera aussi les prémisses). Si ces conditions sont vérifiées alors cela établit R(t1,…,tn). S’il n’y a aucune condition k=0, cela veut dire que R(t1,…,tn) est toujours vrai.

Par exemple on peut définir le fait qu’un nombre entier est pair avec les règles d’inférences suivantes :

pair(0)
        
pair(x)
pair(x+2)

Dans la deuxième règle, x est une variable qui est implicitement quantifiée universellement, c’est-à-dire que la règle est valable si on remplace x par n’importe quel terme. Par exemple

pair(2) 
pair(4) 

mais aussi

pair(1) 
pair(3) 

.

Il y a plusieurs relations qui vérifient ces propriétés (par exemple l’ensemble des entiers ). Les règles d’inférence définissent une relation qui est la plus petite qui convient. Le fait qu’une telle relation existe et a les bonnes propriétés est un théorème qui nécessite des conditions supplémentaires sur Pi. Nous nous intéresserons au cas simple dans lequel chaque Pi est soit un cas particulier R(u1,…,uk) de la relation à définir, soit une condition qui ne parle pas de R.

Lorsque l’on introduit un système d’inférence pour définir une relation, alors on utilise ces mêmes règles d’inférence pour justifier que la relation est vérifiée.

pair(0) 
pair(2)
pair(4)

Le fait que la relation définie est la plus petite qui satisfait les règles d’inférence, nous permet également de dériver un schéma de preuve par induction puissant qui dit que si on se donne une autre relation S qui vérifie les mêmes propriétés que R alors pour tout x1,…,xk, si R(x1,…,xk) on a aussi S(x1,…,xk).

Dans le cas de la définition de pair, cela se traduit par le principe suivant :

Proposition 1 (Principe d’induction sur les entiers pairs.)   

Par exemple on peut utiliser ce principe pour prouver que si n vérifie pair alors il existe k tel que n=2k. Il suffit de vérifier les deux conditions du principe précédent avec pour propriété φ(n), l’énoncé “il existe k tel que n=2k”, c’est-à-dire :

  1. il existe k tel que 0=2k (il suffit de prendre k=0)
  2. soit n arbitraire et supposons qu’il existe k tel que n=2k, montrons qu’il existe k tel que n+2=2k. Il suffit de prendre k′=k+1.

L’exemple pair est particulièrement élémentaire et on peut trouver d’autre formulations équivalentes sans utiliser de règles d’inférence comme k, n=2k ou bien n mod 2=0.

Les règles d’inférence sont particulièrement utiles pour définir des relations plus générales qui ne sont pas des fonctions. Par exemple, si on suppose donnée une relation ami(x,y) qui représente le fait que x a déclaré que y est son ami dans un réseau social. Alors on peut simplement définir une relation reseau(x,y) qui représente le fait qu’il y a une chaîne d’amitié entre x et y.

Il suffit de traduire les conditions suivantes :

  1. Si x et y sont amis alors ils sont dans le même réseau.
  2. Si x et y sont dans le même réseau et y et z sont amis alors x et z sont dans le même réseau.
  3. Il n’y a pas d’autre manière d’être dans le même réseau : si quelqu’un est dans mon réseau, il est soit mon ami, soit l’ami de quelqu’un dans mon réseau

Ce qui se traduit par les règles d’inférence suivantes :

ami(x,y)
reseau(x,y)
     
reseau(x,y)   ami(y,z)
reseau(x,z)

Il peut y avoir plusieurs systèmes d’inférence différents qui définissent la même relation (au sens où on peut prouver reseau(x,y)⇔ reseau1(x,y)⇔ reseau2(x,y)) :

ami(x,y)
reseau1(x,y)
     
ami(x,y)   reseau1(y,z)
reseau1(x,z)

ou encore :

ami(x,y)
reseau2(x,y)
     
reseau2(x,y)   reseau2(y,z)
reseau2(x,z)

Multi-ensembles

Nous aurons besoin dans la suite de la notion de multi-ensemble. Soit un ensemble support E. Un multi-ensemble A sur E se comporte comme un sous-ensemble de E, mais dans lequel on autorise un élément à apparaître plus d’une fois.

En pratique, un multi-ensemble A peut se voir comme une fonction cA de E→ ℕ. Soit un élément x de E, si cA(x)=0 cela signifie que x n’appartient pas à A. Si cA(x)=k > 0 alors on dira que xA et de plus que X apparaît k fois ou encore que le nombre d’occurrences de x dans A est k.

Tout ensemble B peut se voir comme un multi-ensemble dans lequel chaque élément de B apparaît exactement une fois. C’est-à-dire que cB(x)=1 si xB et cB(x)=0 si xB.

Les opérations sur les ensembles s’étendent facilement aux multi-ensembles :

c(x)=0 
A ⋃ BcA⋃ B(x)=cA(x) + cB(x
A ∖ BcA∖ B(x)=cA(x) − cB(x)

On notera l’union de multi-ensembles finis par simple juxtaposition x1,…,xn,y1,…,yp.

Représentation.

Une manière (naïve) d’implanter des multi-ensembles finis est d’utiliser une structure de liste. On peut aussi représenter la fonction comme une structure applicative qui ne fait apparaître que les éléments qui sont effectivement dans le multi-ensemble avec pour chacun le nombre d’occurrences.

2.4.2  Calcul des séquents

Il existe de nombreux systèmes de preuve qui peuvent avoir des propriétés différentes comme de permettre des preuves courtes. Le système de déduction que nous avons présenté en chapitre 1 présente des justifications proches du raisonnement mathématique. Néanmoins, ce système ne se prête pas bien à la démonstration automatique. En effet, certaines règles, si elles sont utilisées de manière inappropriée peuvent conduire à des impasses. C’est le cas par exemple de l’introduction de la disjonction :

Γ ⊢ A 
Γ ⊢ A∨ B 

Si on sait montrer A alors a fortiori, on sait montrer AB mais si on est en train d’essayer de montrer AB se ramener à montrer A peut-être une erreur puisqu’il y a des cas dans lesquels AB est vrai sans que A le soit.

De la même manière, l’élimination de l’implication est problématique. Si AB ∈ Γ, la règle s’écrit :

Γ ⊢ A    Γ,B ⊢ C
Γ ⊢ C

Encore une fois si les prémisses de la règle sont vérifiées alors la conclusion l’est. Par contre nous n’avons aucune garantie que A soit vraie. Là-aussi le système ne nous empêche pas de prendre une mauvaise décision.

On dit que ces deux règles sont non réversibles. Si les prémisses sont vraies alors la conclusion est vraie mais il peut arriver que les prémisses soient fausses et que la conclusion soit néanmoins vraie.

Système G

Le système G répond aux problèmes précédents en introduisant une système de preuve qui retarde la prise de décision et donc ne risque pas de nous amener à un séquent non prouvable si ce que l’on cherche à montrer est vrai.

Pour obtenir ce résultat, on utilise un séquent plus complexe, dans lequel on a un ensemble d’hypothèses mais aussi un ensemble de conclusions A1,…,AnB1,…,Bp.

Le séquent est valide si et seulement si :
pour toute interprétation qui rend vraie toutes les formules A1,…,An, il existe une formule Bj qui est aussi vraie dans cette interprétation.
On notera alors A1,…,AnB1,…,Bp. On remarque que notre définition précédente de A1,…,AnB est un cas particulier de celle-ci lorsqu’il n’y a qu’une formule à droite.

Le séquent nous donne en partie gauche toutes les hypothèses à notre disposition que nous pouvons utiliser à notre guise et en partie droite les différentes options à notre disposition pour conclure la preuve puisqu’il suffit de justifier l’une des formules de droite pour avoir gagné.

Formule associée à un séquent.

On remarque que A1,…,AnB1,…,Bp est équivalent à dire que la formule A1∧…∧ AnB1 ∨ … ∨ Bp est valide avec la convention que si n=0 alors A1∧…∧ An est la formule et si p=0 alors B1 ∨ … ∨ Bp est la formule . Si n=1 alors A1∧…∧ An est défini comme la formule A1 et si p=1 alors B1 ∨ … ∨ Bp est la formule B1.

La formule A1∧…∧ AnB1 ∨ … ∨ Bp avec les conventions précédentes est appelée formule associée au séquent.

Règles du système G

Les règles permettent de décomposer les connecteurs soit dans la partie gauche du séquent, soit dans la partie droite. On utilise des lettres grecques Γ, Δ pour représenter des ensembles arbitraires (finis) de formules. On rappelle que l’ordre des formules n’intervient pas dans la définition d’unensemble. Les ensembles A,B,C et C,A,B sont égaux.

Un premier jeu de règles permet de conclure une preuve dans des cas triviaux :

(Jok)
⊥,Γ ⊢ Δ
      (Triv)
Γ ⊢ Δ,⊤
      (Hyp)
A,Γ ⊢ Δ,A

Nous donnons ensuite les règles pour chaque connecteur : on retrouve la règle Jok qui est la règle gauche de et la règle Triv qui est la règle droite de .

 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 
 
Exemple 1   On peut montrer ¬ (AB) ⊢ ¬ A ∨ ¬ B.
d 
¬ g 
d 
¬ d 
hyp  
 A ⊢ ¬ B,A
  ⊢ ¬ A,¬ B,A
       
¬ d 
hyp  
 B ⊢ ¬ A,B
  ⊢ ¬ A,¬ B,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. La profondeur de l’arbre est au maximum égale au nombre de symboles dans le séquent.

Une autre propriété importante est que toutes les règles sont réversibles c’est-à-dire qu’une interprétation rend vrai un séquent en conclusion d’une règle si et seulement si elle rend vraie les séquents qui apparaissent dans les prémisses.

Proposition 2   Les règles du système G sont correctes et réversibles.

Preuve: On regarde les règles une par une en utilisant les propriétés des connecteurs. On peut se ramener à la validité des formules assossiées. Si Γ=A1,…,An on note M la formule A1∧ … ∧ An et si Δ=B1,…,Bp on note P la formule B1 ∨ … ∨ Bp.

Si on s’intéresse à la règle gauche de l’implication. Les prémisses se traduisent par les formules MPA et BMP la conclusion se traduit par la formule (AB) ∧ MP On vérifie que les formules (MPA) ∧ (BMP) et (AB) ∧ MP sont équivalentes (par exemple à l’aide de tables de vérité).

Proposition 3   Le système G est correct et complet.

Preuve: En décomposant tous les connecteurs, on construit un arbre dont les feuilles sont uniquement composées de formules atomiques A1,…,AnB1,…,Bp.

Les règles sont correctes, donc si le séquent est prouvable alors toutes les feuilles sont des instances des règles “terminales” et la conclusion est aussi valide (par récurrence sur la structure de l’arbre de preuve).

Si le séquent n’est pas prouvable, alors il existe une feuille de l’arbre A1,…,AnB1,…,Bp qui n’est pas une règle triviale. Toute variable propositionnelle qui apparaît dans les Ai, n’apparaît pas dans Bj et donc on peut construire une interprétation qui rend vraie les formules de Ai et faux toutes les formules de Bj. Comme les règles sont réversibles, le nœud qui est le parent de cette feuille est également non valide. Et donc la racine de l’arbre qui est le séquent qui nous intéresse n’est pas valide non plus. On a montré qu’un séquent non prouvable n’est pas valide et donc (contraposée) tout séquent valide est prouvable.

2.4.3  Preuve par résolution

Le système de preuve précédent permet de montrer n’importe quelle formule qui est valide (et donc vraie dans n’importe quelle interprétation). On peut s’intéresser à un autre problème qui est de savoir si une formule est satisfiable ou non, c’est-à-dire s’il existe un modèle.

On va se ramener à un cas où les formules manipulées sont très simples à savoir ce sont uniquement des clauses (disjonction de littéraux).

On rappelle qu’un ensemble de formules est satisfiable s’il existe une interprétation qui rend toutes les formules vraies ou, ce qui est équivalent (dans le cas d’un ensemble fini) si la conjonction des formules est satisfiable.

Mise en forme clausale

On considère seulement le cas où l’ensemble initial de formules est fini mais les résultats présentés se généralisent au cas où E est infini.

Proposition 4 (Mise en forme clausale)   Soit E un ensemble fini de formules. Il existe un ensemble fini de clauses C tel que E est satisfiable si et seulement si C est satisfiable.

Preuve: Si E={A1,…,An} alors E est satisfiable, si et seulement si A1∧ … ∧ An est satisfiable. La formule A1∧ … ∧ An peut être mise en forme normale conjonctive. Elle est donc équivalente à une formule C1∧ … ∧ Cp dans laquelle chaque Ci est une clause. Si on prend C={C1,…,Cp} on a un ensemble de clauses qui est satisfiable si et seulement si l’ensemble initial E était satisfiable. □ La méthode de preuve précédente donne une mise en forme clausale qui correspond à une formule équivalente mais qui peut être exponentiellement plus grosse que la formule initiale.

Mise en forme clausale efficace.

Si on ne s’intéresse qu’à la satisfiabilité, on peut se permettre de transformer la formule et en particulier d’introduire de nouvelles variables pour éviter l’explosion combinatoire.

Le principe de la décomposition est le suivant. On part d’une formule P qui est en forme normale de négation et qui ne contient que des conjonctions et des disjonctions.

On construit un ensemble clause(P) de clauses tel que clause(P) est vraie pour une interprétation I alors P est aussi vraie pour cette interprétation et si P est vraie pour une interprétation I alors il existe une interprétation I qui coincide avec I sur les variables de P et pour laquelle clause(P) est vraie.

On procède par récurrence sur la structure de la formule.

Exemple 2   Soit la formule P définie comme (a1b1) ∨ (a2 ∧ ¬ b2) ∨ (¬ a3 ∧ (b3c)) ∨ a4 ∨ ¬ b4. On introduit les variables x1, x2 et x3 pour représenter respectivement (a1b1) (x1), (a2 ∧ ¬ b2) (x2), et a3 ∧ (b3c)) pour (x3). L’ensemble des clauses contient
{x1 ∨ x2 ∨ x3  ∨ a4 ∨ ¬ b4, ¬ x1 ∨ a1,  ¬ x1 ∨ b1, ¬ x2 ∨ a2, ¬ x2 ∨ ¬ b2, ¬ x3 ∨ a3, ¬ x3 ∨ b3 ∨ c }

Preuve: Pour montrer que la transformation est correcte, il suffit de montrer que P est vraie pour une interprétation I si et seulement si clause(P) est vraie pour une interprétation I qui coincide avec I sur les variables de P. Le seul cas intéressant est celui dans lequel on introduit une nouvelle variable. Il suffit de montrer que A ∨ (PQ) est vraie pour I si et seulement si {Ax, ¬ xP, ¬ xQ} est vrai pour une interprétation I+{xb} avec x une variable qui n’apparaît pas dans la formule initiale. Si A ∨ (PQ) est vraie pour une interprétation I, on prend pour x la valeur de PQ. Si P est vrai alors ¬ xP est vrai et si P est faux alors ¬ (PQ) est vrai et donc ¬ xP aussi, le même raisonnement s’applique à la clause ¬ xQ.

Dans l’autre sens, si {Ax, ¬ xP, ¬ xQ} est vraie pour une interprétation I. Si l’interprétation rend A vraie alors la formule A ∨ (PQ) est aussi vraie pour cette interprétation. Sinon l’interprétation I rend x vraie et donc comme ¬ xP et xQ sont vrais, on en déduit que P et Q sont vrais pour cette interprétation et donc A ∨ (PQ) est vraie pour cette interprétation.

Résolution

On rappelle qu’une clause est une disjonction de littéraux et peut donc se voir comme un ensemble de littéraux. Nous les noterons l1∨…∨ ln mais considérons les clauses ll et l comme identique. Le cas où cet ensemble est vide correspond à la proposition qui est toujours fausse. Si la clause contient la formule alors, la clause est toujours vraie, elle est équivalente à la clause x ∨ ¬ x. On peut donc toujours se ramener au cas où les littéraux sont des variables ou des négations de variables propositionnelles (et donc ne contiennent ni , ni .

On suppose donné un ensemble de clauses. On cherche à savoir si ces clauses sont satisfiables. Pour cela on va se donner un système de règles qui nous permet de dériver de nouvelles clauses telle que si l’ensemble initial est vrai pour une interprétation I, alors l’ensemble obtenu en ajoutant la nouvelle clause l’est aussi. 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 clause initial n’est pas satisfiable.

Définition 1 (Preuve par résolution)   Soit C et C deux clauses 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:

Exemple 3   On se donne l’ensemble E suivant p ∨ ¬ qr, ¬ r, p}. On peut faire les étapes de résolution suivantes :
(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
Si on ajoute maintenant la clause q à l’ensemble E précédent, on peut construire une réfutation :
(q) 
(r) 
(p) ¬ p ∨ ¬ q ∨ r          p
 ¬ q ∨ r
           ¬ r
 ¬ q
          q
 
On peut également partir de la formule A définie comme ¬ (p ∨ (qr)) ⇒ (¬ q ∨ ¬ r). 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
 
Proposition 5   Soit E un ensemble de clauses.

Preuve:

La technique de preuve par résolution est importante car elle est à la base des systèmes de programmation logique (le plus connu est le langage de programmation Prolog) qui permet de calculer à partir de programmes décrits de manière logique par des clauses.


Previous Up Next