Dans ce chapitre, nous allons aborder la logique et les formules sur le plan syntaxique, c’est-à-dire que nous chercherons à établir des propriétés logiques des formules (validité, satisfiabilité) par des transformations sans passer par la notion de modèle. Nous étudierons tout d’abord des mises en formes canoniques de formules logiques et en particulier la mise en forme clausale. Nous introduirons également la représentation des formules propositionnelles comme des diagrammes de décision binaires. Finalement nous introduirons des systèmes de déduction pour les formules et en particulier le calcul des séquents.
Dans le chapitre 2 nous avons introduit la forme normale de négation d’une formule. Une formule en forme normale de négation ne contient pas de connecteur ⇒ (ou ⇔) et les seuls négations portent sur des symboles de prédicat. Grace aux lois de de Morgan, il est possible de propager les symboles de négation jusqu’aux symboles de prédicat et donc toute formule est équivalente à une formule en forme normale de négation. De plus cette transformation ne change pas la taille de la formule.
Dans la suite, on parlera d’instance de prédicat pour parler d’une formule de la forme R(t1,…,tn) avec R un symbole de prédicat. Une formule atomique est soit une instance de prédicat soit de la forme ⊤ ou ⊥. Dans le cas propositionnel, les instances de prédicat sont juste les variables propositionnelles.
Preuve: Pour définir un algorithme qui calcule la forme normale de négation d’une formule, on construit deux fonctions de manière récursive : fnn qui étant donnée une formule quelconque P, construit une formule en forme normale de négation équivalente à P et neg qui étant donnée une formule quelconque P, construit une formule en forme normale de négation équivalente à ¬ P.
|
On montre ensuite par récurrence structurelle sur la formule P que fnn(P) et neg(P) sont en forme normale de négation et que de plus fnn(P)≡ P et neg(P)≡ ¬ P □
Un litteral tout seul est une clause dans laquelle il n’y a pas de disjonction. Si on veut faire apparaître une disjonction, on peut toujours rééecrire le littéral l en l∨ ⊥.
Les clauses peuvent se simplifier. La disjonction est associative et commutative, on a également P∨ P≡ P, P∨ ¬ P≡ ⊤, P∨ ⊤ ≡ ⊤, P∨ ⊥ ≡ P. Une clause peut donc soit être de la forme ⊥ ou ⊤, soit s’écrire l1∨ l2∨… ∨ ln avec li un littéral autre que ⊥ ou ⊤. On peut représenter une clause comme un ensemble de litteraux tous distincts. La clause qui correspond à la formule atomique ⊥ est appelée clause vide elle correspond par convention à un ensemble vide de littéraux. Si une clause contient une instance de prédicat et sa négation alors elle est de la forme p∨¬ p∨ Q et se simplifie en ⊤.
On peut donc se ramener à une clause dans laquelle chaque instance de prédicat R(t1,…,tn) apparaît au plus une fois sous forme positive ou négative (¬ R(t1,…,tn)).
Preuve: Si une instance de prédicat p apparaît deux fois sous forme positive ou deux fois sous forme négative, alors en utilisant p∨ p≡ p on peut retirer une des occurrences sans changer la valeur de la formule. Si une instance de prédicat p 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 à ⊤ (on dira que la clause est triviale). Si une clause est de la forme P∨⊥ on peut la simplifier en la clause P. □
Une clause est donc caractérisée par un ensemble d’instances de prédicats, chacun associé à un signe pour
indiquer s’il apparait en position positive ou négative. On peut représenter une clause not triviale comme un ensemble d’instance de prédicats associés à des booléens (true si l’instance apparait positivement et false si elle apparait négativement).
Par exemple la clause p∨¬ q peut se représenter par l’ensemble {(p,true);(q,false)}.
Par convention, la clause associée à un ensemble
vide de littéraux est interprétée comme la formule fausse
⊥. En effet une disjonction de formules est vraie lorsque l’une des formules qui forme la disjonction est vraie. S’il n’y a pas de formule, alors la propriété est fausse.
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. L2 ∖ L1). On a C2 ≡ C1 ∨ C3 et donc comme C1 ∨ C3 est une conséquence logique de C1, on en déduit que C2 est une conséquence logique de C1. □
La conjonction de formules est vraie lorsque toutes les formules qui forment la conjonction sont vraies. S’il n’y a pas de formule, alors la propriété est vraie.
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.
Preuve: On s’intéresse à l’ensemble Z des n-uplets pour lesquels la fonction f est fausse, c’est-à-dire
Z |
| {(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 l1 ∨ l2 ∨ … ∨ ln avec li=pi si bi=F et li=¬ pi si bi=V. Cette formule est une clause. Il suffit ensuite de prendre la conjonction des clauses pour chaque élément de Z. □
|
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 p ∨ q.
La forme normale conjonctive est donc (¬ p ∨ ¬ q) ∧ (p ∨ q).
Construire la table de vérité d’une formule est trop complexe en général et donc on va plutôt utiliser des méthodes syntaxiques. La formule (a ∧ b) ∨ c n’est pas en forme normale conjonctive car il y a une disjonction qui porte sur une formule qui n’est pas un littéral. La règle de distributivité permet d’inverser les conjonctions et les disjonctions.
|
On en déduit un algorithme de mise en forme normale conjonctive. Pour cela, on construit une fonction fnc(P) qui calcule un ensemble de clauses équivalent à P et on utilise de manière auxiliaire une fonction fnc-neg(P) qui construit un ensemble de clauses équivalent à ¬ P. On aura besoin d’une autre fonction auxiliaire sh, qui prend en argument deux ensembles de clauses E et E′ et construit un nouvel ensemble de clauses avec toutes les combinaisons possibles C∨ C′ avec C∈ E et C′∈ E′, c’est-à-dire que sh(E,E′)={C∨ C′|C∈ E, C′∈ E′}. Si E contient n clauses et Si E′ contient p clauses alors sh(E,E′) peut contenir jusqu’à n× p clauses (il pourrait y en avoir moins si certaines clauses se simplifient).
|
|
On définit de manière duale la notion de 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 l1 ∧ l2 ∧ … ∧ ln avec li=pi si bi=V et li=¬ pi si bi=F. Il suffit ensuite de prendre la disjonction de ces formules pour trouver une formule équivalente à P. □
(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 x↦ V si l=x et x↦ F si l=¬ x. 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 (a1∨ b1) ∧…∧ (an ∨ bn) 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.
Lorsqu’une formule propositionnelle est en forme normale conjonctive, il est facile de voir si elle est valide. En effet si l’ensemble des clauses n’est pas vide, on en choisit une qui est de la forme l1∨… ∨ ln que l’on rend fausse en choisissant une interprétation dans laquelle chacun des li est faux ce qui est possible car ils portent tous sur des variables propositionnelles différentes. Si une des clauses de la forme normale conjonctive est fausse alors il en est de même de la formule.
La forme normale conjonctive de la formule (a1 ∧ b1) ∨ … ∨ (an ∧ bn) s’écrit ∧ci∈{ai,bi}c1∨… ∨ cn qui contient 2n clauses. Cette complexité est intrinsèque car liée à la complexité de décider si une formule propositionnelle est valide.
La forme normale conjonctive est équivalente à la formule initiale. Pour la démonstration automatique, cette équivalence n’est pas forcément nécessaire. Si on ne s’intéresse qu’à la satisfiabilité, on peut se permettre de transformer la formule P en une formule Q, telle que P et Q ne sont pas équivalentes, mais seulement equisatisfiable. C’est-à-dire que P est satisfiable si et seulement si Q. Cela nous permet d’introduire de nouvelles variables propositionnelles dans Q pour éviter l’explosion combinatoire.
Dire que P et Q sont équivalents c’est dire que pour toute interprétation I, on a I⊨ P si et seulement si I⊨ Q alors que dire que P et Q sont equisatisfiables c’est dire qu’il existe une interprétation I telle que I⊨ P si et seulement si il existe une interprétation J telle que J⊨ Q. Deux formules équivalentes sont equisatisfiables mais le contraire n’est pas vrai.
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 de clauses, clause(P), tel que : si 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 J 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.
clause(P)= |
|
{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 J.
On suppose donnée une interprétation I telle que I⊨ P. On construit une interprétation J qui coincide avec I sur les variables de P et telle que J⊨ clause(P). Le seul cas intéressant est celui dans lequel on introduit une nouvelle variable propositionnelle. Il suffit de montrer que si I⊨ A ∨ (R ∧ Q) et que x est une variable propositionnel qui n’apparaît pas dans A ∨ (R ∧ Q) alors il existe une interprétation J telle que J⊨ A ∨ x, ¬ x ∨ R, ¬ x ∨ Q.
On suppose que I⊨ A ∨ (R ∧ Q), on construit une interprétation J qui coincide avec I pour tous les symboles dans I et on choisit pour interpréter la variable x, la valeur de R∧ Q dans I. Si I⊨ R alors J⊨ R (car I et J coincident sur les symboles qui apparaissent dans R) et a fortiori J ⊨¬ x ∨ R. Si R est faux dans I alors I⊨ ¬ (R∧ Q) et donc x vaut F dans J et donc J⊨¬ x ∨ R. Le même raisonnement s’applique à la clause ¬ x ∨ Q.
Dans l’autre sens, si une interprétation J rend vraie les trois formules {A ∨ x, ¬ x ∨ R, ¬ x ∨ Q}, on va montrer que J⊨ A ∨ (R ∧ Q). Si J⊨ A alors J⊨ A ∨ (R ∧ Q). Sinon comme J⊨ A ∨ x, on en déduit J⊨ x et donc comme J⊨ ¬ x ∨ R et J⊨ ¬ x ∨ Q, on en déduit que J⊨ R et J⊨ Q et donc J⊨ A ∨ (R∧ Q). □
Les transformations précédentes, traitent de la partie propositionnelle des formules (sans quantificateur), nous allons dans cette section montrer comment peut se traiter la partie avec quantificateurs.
Dans la section 2.3.2 nous avons établit des propriétés d’équivalence qui permettent de ramener les quantificateurs en tête de formule. Si x n’est pas libre dans la formule A alors :
|
Attention la remontée des quantificateurs au travers d’une négation change le quantificateur (loi de de Morgan) de même lorsqu’il est dans la partie gauche d’une implication. La remontée des quantificateurs doit se faire après avoir mis la formule en frme normale de négation.
Q x1, …, Q xn, A |
Preuve:
On commence par mettre la formule P en forme normale de négation puis on utilise les équivalences rappelées ci-dessus pour remonter les quantificateurs en veillant à renommer si nécessaire les variables liées pour ne pas créer de phénomène de capture. Par exemple si on a une formule de la forme A ∨ ∃ x,G(x) et que x est libre dans A (en plus d’être liée dans ∃ x,G(x) alors on commence par renommée la variable liée (ce qui ne change pas le sens de la formule) en choisissant une variable z qui n’est pas libre dans A ni dans ∃ x,G(x), on a alors A ∨ ∃ x,G(x)≡ A ∨ ∃ z,G(z)≡ ∃ z,A ∨ G(z)
□
La forme prénexe n’est pas unique. L’ordre des quantificateurs en particulier peut varier en fonction de l’ordre dans lequel on choisit de les faire remonter.
On a vu qu’intervertir un quantificateur exitentiel et un quantificateur universel en général ne préservait pas l’équivalence entre les formules. Nous allons montrer ici que si on ne s’intéresse qu’à la satisfiabilité, alors on peut se ramener à une formule prénexe qui n’aura que des quantificateurs universels.
La skolemisation est une opération (introduite par le logicien norvégien Thoraf Albert Skolem au 20ème siècle) qui permet de se débarrasser des quantifications existentielles en enrichissant les signatures et en préservant la satisfiabilité des formules.
L’idée de base est que si on s’intéresse à la formule ∀ x,∃ y,P(x,y) cette formule est vérifiée si pour tout élément d du domaine, on peut trouver un élément e du domaine tel que I,{x↦ d,y↦ e}⊨ P(x,y) est vraie. En général, la valeur e retenue pour y dépend de la valeur d choisie pour x. On peut exprimer e en fonction de d et donc le problème ∀ x,∃ y,P(x,y) est analogue au problème ∀ x,P(x,f(x)) dans lequel f est un nouveau symbole de fonction.
De manière plus précise on peut prouver ∀ x,P(x,f(x))⊨ ∀ x,∃ y,P(x,y) et si la formule ∀ x,∃ y,P(x,y) est satisfiable alors on peut à partir d’un modèle de cette formule, trouver un modèle de la formule ∀ x,P(x,f(x)) en choisissant la bonne interprétation pour la fonction f.
Pour que cette opération soit licite il suffit que les variables x1,…,xn ne soient pas liées dans B ce qui peut toujours être garanti quite à effectuer des renommages de variables liées dans B.
Preuve: La première propriété est une conséquence de B[y← f(x1,…,xn)]⊨ ∃ y,B et du fait que A est en forme normale de négation. En effet on vérifie aisément les propriété de stabilité de la conséquance logique : si Q⊨ R alors pour n’importe quelle formule P on a
Q∧ P⊨ R∧ P Q∨ P⊨ R∨ P ∀ x,Q⊨ ∀ x, R ∃ x,Q⊨ ∃ x, R |
Pour la seconde propriété on suppose construit un modèle I de la formule A. La formule B a comme variables libres les variables x1… xn, y. On regarde dans le modèle l’ensemble des n+1-uplets (d1,…,dn,e) tels que I,{x1↦ d1,…,xn↦ dn,y↦ e}⊨ B. On peut à partir de cette relation construire une fonction fJ ∈ Dn→ D telle que I,{x1↦ d1,…,xn↦ dn,y↦ fJ(d1,…,dn)}⊨ B s’il existe e tel que I,{x1↦ d1,…,xn↦ dn,y↦ e}⊨ B et fJ(d1,…,dn)=d avec d une valeur arbitraire de D si pour tout e, I,{x1↦ d1,…,xn↦ dn,y↦ e}⊭B. On peut alors construire une interprétation J sur le même domaine D que I, qui étend l’interprétation I avec l’interprétation du symbole de fonction f comme la fonction fJ.
Cette interprétation rend vraie la formule (∃ y,B) ⇔ B[y← f(x1,…,xn)] pour tout environnement {x1↦ d1,…,xn↦ dn}. Elle rend donc aussi vraie la formule ∀ x1… xn,((∃ y,B) ⇔ B[y← f(x1,…,xn)]). Par ailleurs cette interprétation rend vraie la formule A car J est une extension de I qui est un modèle de A. Comme par ailleurs on peut montrer ∀ x1 … xn,((∃ y,B) ⇔ B[y← f(x1,…,xn)]) ⊨ A⇔ A′ car A′ est obtenue à partir de A en remplaçant ∃ y,B par B[y← f(x1,…,xn)], on en déduit que J est un modèle de A′. □
On peut itérer l’opération précédente pour éliminer tous les quantificateurs existentiels d’une formule. Chaque élimination de quantificateur introduit un nouveau symbole de fonction.
Si on applique ces transformations à une formule A en forme normale de négation, on obtient une formule B sans quantificateur existentiel telle que
Cette opération peut nous permettre de montrer la validité d’une formule. En effet la validité d’une formule A est équivalent à l’insatisfiabilité de la formule ¬ A qui se ramène donc à l’insatisfiabilité de la forme skolémisée de ¬ A. Comme la forme skolémisée est une formule universelle, le théorème de Herbrand nous permet de ramener la satisfiabilité à l’existence d’un modèle construit sur le domaine de Herbrand.
Si on se donne un ensemble de formules A1,…,An on peut traiter la skolémisation de manière indépendante pour chaque formule. On obtient pour chaque Ai une formule Bi sans quantificateurs telle que ∀(Bi)⊨ Ai. On en déduit aisément que :