L'algorithme de Wang pour le calcul des propositions

Nouvelle version, mai 2011

Jean-François Perrot


Note historique

Motivation : un système formel  traditionnel pour le calcul des propositions
et son inadéquation au calcul automatique
  1. Le système 
  2. Exemples de preuves dans ce système 

Notations
I- Séquents
   a) Description
   b) Validité
   c) Antécédents et conséquents vides

II - Algorithme de Wang
   a) Critères de validité, séquences atomiques, complexité
   b) Réduction de la complexité, cas de la négation
   c) Réduction de la complexité, disjonction, conjonction et implication
   d) Exemples

III - Système formel
   a) Langage, axiomes, règles de déduction
   b) Exemples d'arbres de preuve
   c) Stratégie de recherche, programme
 
IV- Réalisation en Prolog


Note historique :

Hao Wang est un logicien américain.
L'algorithme en question a été publié en 1960 dans  l'IBM Journal of Research and Development,
[Volume 4, Number 1, Page 2] article intitulé "Toward Mechanical Mathematics".
Dans cet article, notre algorithme apparaît comme "premier  programme", alias système "P".
L'article contient aussi des variantes et une extension au calcul des prédicats.

Cet article a été écrit en 1958, et les expériences furent effectuées sur IBM 704 -
machine à lampes, 32 k mots de 36 bits, celle-là même qui vit naître LISP à la même époque.
Le programme a été écrit en assembleur (Fortran existait à l'époque, mais il ne s'était pas encore imposé)
et l'auteur estime que "there is very little in the program that is not straightforward".

Il observe que les preuves engendrées sont "essentiellement des arbres", et annonce que
la machine a démontré 220 théorèmes du calcul des propositions (tautologies) en 3 minutes.
Il en tire argument pour la supériorité d'une approche algorithmique par rapport à une approche heuristique
comme celle du "Logic  Theorist" de Newell, Shaw et Simon (à partir de 1956 sur la machine
JOHNNIAC de la Rand Corporation) : un débat qui dure encore ...

Cet algorithme a été popularisé par J. McCarthy, comme exemple-fanion d'application de LISP.
Il figure dans le manuel de la première version de LISP (LISP 1, sur IBM 704 justement, le manuel est daté de Mars 1960), et il a été repris dans le célèbre LISP 1.5 Programmer's Manual publié en 1962 par MIT Press,
un des maîtres-livres de l'Informatique.

Motivation : un système formel traditionnel pour le calcul des propositions
et son inadéquation au calcul automatique

Traditionnel signifie que le calcul des propositions est pris dans sa formulation  à la Hilbert et non à la Gentzen (voyez Wikipédia-fr ).
L'approche de Gentzen (par la déduction naturelle) est précisément une réponse à la difficulté que nous allons mettre en évidence. L'algorithme de Wang s'inscrit dans cette dernière perspective.
Nous donnerons plus loin une formulation de l'algorithme comme un système formel qui nous ramènera 
aux préoccupations évoquées ici.

Rappel sur les notations :

Nous  adoptons ici le système de connecteurs usuel (disjonction, conjonction, négation et implication matérielle).
Par ordre de priorité décroissante :

           "¬" pour la négation ,
           "∨" pour la disjonction (OU),
           "∧" pour la conjonction (ET),
           "⊃" pour l'implication.

Exemple : (a ∨ b) ∧ ¬a ⊃ b  = (((a OU b) ET (NON a)) IMP b)

I - Séquents

L'algorithme  de Wang résulte de l'application au calcul propositionnel de la méthode connue sous le nom de déduction naturelle.

a) Description

Pour démontrer qu'une formule donnée du calcul des propositions est une tautologie,
on travaille non pas sur des propositions isolées, mais sur des séquents, de la forme

                       " p1, p2,...,pm -> q1, q2,...,qn "

ou les pi, qj sont des propositions.
[ Le mot séquent est un néologisme emprunté à l'anglais.
  Je l'adopte ici, plutôt que séquence, car ce dernier terme est très employé en informatique pour désigner toute autre chose.]

L'ensemble des pi forme l'antécédent du séquent, celui des qj s'appelle son conséquent.

Par exemple, avec m = 1 et n = 2 :

          (¬a ∨ (b ⊃ c))   ->    (a ∧ ¬b) , (a ⊃ c)

antécédent = {(¬a ∨ (b ⊃ c))}  conséquent = {(a ∧ ¬b) , (a ⊃ c)}.

L'antécédent  et  le  conséquent étant des ensembles de propositions, l'ordre des  pi et  des  qj est sans signification.  Également, une même proposition n'est comptée qu'une seule fois : les pi et les qj sont tous distincts.

Notons que l'un ou l'autre ou les deux peuvent être vides.

b) Validité

Un séquent s'interprète comme une implication matérielle

                    "(p1 ET p2 ET...ET pm)  =>  (q1 OU q2 OU...OU qn)".

Dans notre exemple :

                    (¬a ∨ (b ⊃ c))  ⊃  (a ∧ ¬b) ∨ (a ⊃ c)

Un tel séquent est valide si l'implication en question est vraie quelque soit le système  de valeurs des variables,
c'est-a-dire si l'implication en question, vue comme une proposition unique, est une tautologie. 
Nous voici ramenés à la case "départ" ...  mais en apparence seulement.

Notre exemple se trouve être un séquent valide !

c) Antécédents et conséquents vides

Rappelons que la conjonction (resp. la disjonction) d'un ensemble vide de propositions vaut VRAI (resp.  FAUX).
En effet, on généralise la conjonction (resp. la disjonction) binaire à des ensembles quelconques
en posant que le résultat  est VRAI sauf si l'une des formules de l'ensemble est fausse
(resp. FAUX sauf si l'une des formules est vraie).

Un séquent valide dont le conséquent est vide exprime donc que
les éléments de son antécédent sont des propositions contradictoires.

Un séquent valide dont l'antécédent est vide exprime donc que
les éléments de son conséquent sont des propositions "complémentaires", dont la disjonction est tautologique.

Le séquent dont l'antécédent et le conséquent sont vides n'est pas valide.
On peut la prendre pour représenter le FAUX dans le langage des séquents.

Une  proposition quelconque p est donc une tautologie ssi le séquent " -> p" est valide.
On ramène donc la preuve d'une tautologie à démontrer la validité d'un séquent.

II - L'algorithme de Wang

a) Critère de validité, séquences atomiques, complexité :

Pour qu'un séquent soit valide, il suffit qu'une même formule apparaisse dans ses deux membres (antécédent et conséquent). 
[C'est une conséquence immédiate du fait  que  (p  ∧  X)  >  (p  ∨  Y) pour toute proposition p,
X et Y étant des formules quelconques].

Cette condition est aussi nécessaire lorsque tous les éléments du séquent sont des variables  (propositions  atomiques),
c'est-à-dire que
En effet, dans ce cas il suffit de donner
pour obtenir un système de valeurs des variables qui rend fausse l'implication associée au séquent.
On notera que ce raisonnement reste valable si l'antécédent ou le conséquent, ou les deux,
sont vides (cf.  I-c)].

Exemple : le séquent  " a, b -> c, d " où a, b, c, d sont des variables, n'est  pas valide
car si on prend a et b VRAIs et c et d FAUX, la proposition implicative associée au séquent :
(a ∧ b) ⊃ (c ∨ d) prend la valeur FAUX.

Appelons séquent atomique un séquent dont tous les éléments sont des variables.
Pour un tel séquent, nous pouvons décider de sa validité par une simple inspection.
Nous allons à présent voir comment
ramener la validité de tout séquent à celle d'un ensemble fini de séquents atomiques.
Definissons la "complexité" d'un séquent comme le nombre total de connecteurs qui apparaissent dans ses éléments.
Un séquent atomique est de complexité nulle.
Nous allons voir comment passer d'un séquence de complexité positive à un séquenct équivalent,
ou à un couple de séquents équivalent, de complexité strictement plus faible.

En itérant le processus à partir d'un séquent donné s, on arrive à une ensemble fini A de séquents atomiques,
équivalent à s en ce sens que s est valide si, et seulement si, tous les séquents de A sont valides.
En fait cette équivalence est plus forte : le séquent s et l'ensemble A sont "logiquement équivalents",
en ce sens qu'ils sont tous deux vrais pour les mêmes systèmes de valeurs des variables qui subsistent dns A.
selon le vocabulaire traditionnel, l'ensemble A représente la forme conjonctive réduite du séquent s.

Pour ce faire, conformément au principe de la déduction naturelle, nous allons attacher à chaque connecteur
des règles (deux par connecteur), qui expriment en quelque sorte sa signification.

b) Réduction de la complexité des formules : le cas de la négation

Soit S un séquent où apparaît une négation parmi les éléments de l'antécédent :
comme l'ordre des éléments est indifférent, nous pouvons appeler p1 cet élément, et poser p1 = ¬p. 
Le séquent S s'écrit alors :

                   S =  ¬p, p2,...,pm -> q1, q2,...,qn

Observation :  Le  séquent S est équivalent au séquent S' obtenu en "faisant passer p dans le conséquent" :

                     S' =   p2,...,pm -> p, q1, q2,...,qn

Par "équivalent", nous entendons que S est valide si et seulement si S' est valide, et plus précisément que
S est vrai pour un certain système de valeurs des variables ssi S' est vrai pour le système en question

En  effet, dire que S est valide signifie que :
  toutes les fois que les propositions  pi  (i =  1,..., m) sont simultanément toutes vraies,
   l'une au moins des qj (j = 1,..., n) est vraie,
donc que toutes les fois que les pi  (i =  2,..., m) sont toutes vraies
et que p est fausse, alors l'une au moins des qj est vraie.

De même, dire que S' est valide signifie que :
  toutes les fois que les propositions   pi  (i =  2,...,m) sont simultanément toutes vraies,
l'une au moins des qj (j = 1,...,n) est vraie.

Supposons S valide et montrons que S' l'est aussi, à savoir que
si toutes les pi  (i =  2,...,m) sont vraies, l'une au moins de p et des qj (j = 1,...,n) est vraie.

Deux cas se présentent, selon que p est vraie ou fausse.
Réciproquement,  la validité de S' entraîne celle de S, car si toutes les pi  (i =  2  ...   m)
sont vraies et que p est fausse, alors S' nous assure que l'une des qj est vraie, c'est tout ce que demande S !

Notre observation est ainsi établie.
Son intérêt est évidemment qu'elle permet  de  passer  du séquent  S à S' dont la complexité est exactement un de moins.
Nous la reformulons donc comme une règle d'action :

 
Règle Neg-Ant : (Négation dans l'antécédent)

            POUR DÉMONTRER LA VALIDITÉ DU SÉQUENT

                   " ¬p, p2,...,pm -> q1, q2,...,qn "

            IL SUFFIT D'ÉTABLIR CELLE DU SÉQUENT

                     "p2,...,pm -> p, q1, q2,...,qn"

            ET RÉCIPROQUEMENT.

L'application répétée de cette règle permet de ramener la preuve de la validité d'un séquent donné
à celle d'un séquen où aucune négation ne figure plus dans l'antécédent.

On peut faire l'observation symétrique et voir qu'un  séquent où une négation apparaît dans le conséquent
est équivalent au séquent obtenu en faisant passer la formule niée dans l'antécédent,
avec un gain de complexité de 1, d'ou la seconde règle relative a la négation :


 Règle Neg-Cons : (Négation dans le conséquent)

            POUR DÉMONTRER LA VALIDITÉ DU SÉQUENT

                   "p1, p2,...,pm -> ¬q, q2,...,qn"

           IL SUFFIT D'ÉTABLIR CELLE DU SÉQUENT

                   "q, p1, p2,...,pm -> q2,...,qn"

           ET RÉCIPROQUEMENT.



L'usage systématique de ces deux règles permet donc de passer d'un séquent donné à un séquent équivalent
(vrai pour les mêmes systèmes de valeurs des variables)
ne contenant plus aucune formule de la forme (¬ f).

Les  autres  connecteurs vont à présent recevoir un  traitement analogue.

c)  Réduction  de  la  complexité  des formules : disjonction, conjonction et implication

La définition même de la proposition implicative associée à un séquent, jointe à l'associativité de la disjonction,
montre qu'un séquent S où une disjonction apparaît dans le conséquent est équivalent au séquent S'
de complexité un de moins, obtenue en "supprimant les parenthèses" :

                    S =   p1, ... , pm -> (q' ∨ q"), q2, ... , qn
équivaut à
                    S' =   p1, ... , pm -> q', q", q2, ... , qn


De même pour un séquent où une conjonction apparaît dans l'antécédent :

                    S =   (p' ∧ p"), p2, ... , pm -> q1, q2, ... , qn
équivaut à
                    S' =   p', p", p2, ... , pm -> q1, q2, ... , qn

Lorsqu'une  disjonction apparaît dans l'antécédent, les choses se compliquent un peu.
Un séquent de ce type

                    S =   (p' ∨ p"), p2, ... , pm -> q1, q2, ... , qn

est valide si et seulement si les deux séquences suivantes le sont :

                    S' =   p', p2, ... , pm -> q1, q2, ... , qn
                    S" =   p", p2, ... , pm -> q1, q2, ... , qn

En effet, la disjonction (p' ∨  p") est  vraie si l'une ou l'autre des propositions  p' et p" est vraie :
La réciproque est immédiate. 

On notera  que les deux séquents S' et S" ont chacun une complexité au plus un de moins que S
(la somme de leurs complexités vaut un de moins).

De même pour un séquent où une conjonction apparaît dans le conséquent :
le séquent

                    S =   p1, ... , pm -> (q' ∧ q"), q2, ... , qn

est valide si et seulement si les deux suivants, de complexité inférieure, le sont

                    S' =   p1, ... , pm -> q', q2, ... , qn
                    S" =   p1, ... , pm -> q", q2, ... , qn

Vérification immédiate.

Comme pour la négation, nous reformulons ces observations comme des règles associées aux connecteurs.

Voici les règles de la disjonction :


Regle Disj-Ant : (Disjonction dans l'antécédent)

          POUR DÉMONTRER LA VALIDITÉ DU SÉQUENT

                  " (p' ∨ p"), p2, ... , pm -> q1, q2, ... , qn "

          IL SUFFIT D'ÉTABLIR CELLE DU SÉQUENT

                  " p', p2, ... , pm -> q1, q2, ... , qn "

          ET CELLE DU SÉQUENT

                  " p", p2, ... , pm -> q1, q2,...,qn "

          ET RÉCIPROQUEMENT.



Règle Disj-Cons : (Disjonction dans le conséquent)

          POUR DÉMONTRER LA VALIDITÉ DU SÉQUENT

                  " p1, p2, ... , pm -> (q' ∨ q"), q2, ... , qn "

          IL SUFFIT D'ÉTABLIR CELLE DU SÉQUENT

                  " p1, p2, ... , pm -> q', q", q2, ... , qn "

          ET RÉCIPROQUEMENT.




Voici les règles de la conjonction :



Règle Conj-Ant : (Conjonction dans l'antécédent)

          POUR DÉMONTRER LA VALIDITÉ DU SÉQUENT

                  " (p' ∧ p"), p2, ... , pm -> q1, q2, ... , qn "

          IL SUFFIT D'ÉTABLIR CELLE DU SÉQUENT

                  " p', p", p2, ... , pm -> q1, q2, ... , qn "

          ET RÉCIPROQUEMENT.


Règle Conj-Cons : (Conjonction dans le conséquent)

          POUR DÉMONTRER LA VALIDITÉ DU SÉQUENT

                  " p1, p2, ... , pm -> (q' ∧ q"), q2, ... , qn "

          IL SUFFIT D'ÉTABLIR CELLE DU SÉQUENT

                  " p1, p2, ... , pm -> q', q2, ... , qn"

          ET CELLE DU SÉQUENT

                  " p1, p2, ... , pm -> q", q2, ... , qn "

          ET RÉCIPROQUEMENT.


Application au connecteur d'implication matérielle :


Comme  par définition on a "X ⊃ Y <==> ¬X ∨ Y", un séquent qui présente une implication  dans  l'antécédent 
peut  se  traiter en lui appliquant la règle Disj-Ant :
on réécrit

                  S = (p' ⊃ p"), p2, ... , pm -> q1, q2, ... , qn
comme

                 S = (¬p' ∨ p"), p2, ... , pm -> q1, q2, ... , qn

qui donne les deux séquents

                 S' = ¬p', p2, ... , pm -> q1, q2, ... , qn
                 S" =  p", p2, ... , pm -> q1, q2, ... , qn

puis en appliquant la règle  Nég-Ant  à  S' on obtient

                 S'' = p2, ... , pm -> p', q1, q2, ... , qn

d'où finalement un couple de deux séquents de complexité strictement inférieure à celle de S :

                 S'' = p2, ... , pm -> p', q1, q2, ... , qn
                 S" =  p", p2, ... , pm -> q1, q2, ... , qn

Nous formulons donc la règle dérivée :


Règle Imp-Ant : (Implication dans l'antécédent)

          POUR DÉMONTRER LA VALIDITÉ DU SÉQUENT

                  " (p' ⊃ p"), p2, ... , pm -> p', q1, q2, ... , qn"

          IL SUFFIT D'ÉTABLIR CELLE DU SÉQUENT

         " p2, ... , pm -> p', q1, q2, ... , qn "

          ET CELLE DU SÉQUENT

                  " p", p2, ... , pm -> q1, q2, ... , qn "

          ET RÉCIPROQUEMENT.



De même, un séquent présentant une implication dans le conséquent se traite par Disj-Cons suivie de Nég-Cons,
d'où la règle dérivée :


Règle Imp-Cons : (Implication dans le conséquent)

          POUR DÉMONTRER LA VALIDITÉ DU SÉQUENT

                  " p1, p2, ... , pm -> (q' ⊃ q"), q2, ... , qn "

          IL SUFFIT D'ÉTABLIR CELLE DU SÉQUENT

          " q',  p1, p2, ... , pm ->  q", q2, ... , qn "

          ET RÉCIPROQUEMENT.


On observera que la règle Imp-Cons justifie la tendance naturelle à traduire une proposition implicative directement
sous la forme d'une séquent, avec un antécédent non-vide :
par exemple, la tautologie

                    (¬a ∨ (b ⊃ c)) > (a ∧ ¬b ∨ (a ⊃ c))

se traduit "officiellement" par le séquent avec antécédent vide

(S0)                ->  (¬a ∨ (b ⊃ c) > a ∧ ¬b ∨ (a ⊃ c))

mais, vu l'interprétation des séquents comme des implications, on est tenté de la traduire directement par la séquence équivalente

(S1)                (¬a ∨ (b ⊃ c))   ->    ((a ∧ ¬b) ∨ (a ⊃ c))

qui  résulte de S0 par la règle Imp-Cons, et même, en allant plus loin dans l'interprétation,
par un séquent avec deux éléments dans le conséquent

(S2)                (¬a ∨ (b ⊃ c))   ->    (a ∧ ¬b) , (a ⊃ c)

qui resulte de S1 par la règle Disj-Cons.

d) Exemples

Un certain nombre de tautologies simples sont effectivement  traitées "instantanément" par notre méthode :

" x ⊃ x " : se traduit par le séquent " -> (x ⊃ x) " qui via Imp-Cons donne " x -> x " qui est valide.

" x  ∨ ¬x "  (loi  du  tiers  exclu)  :  se traduit par " -> (x ∨ ¬x) ",
  1. par Disj-Cons on obtient " -> x , ¬x "
  2. et par Nég-Cons " x -> x " valide.
" x ⊃ (y ⊃ x) " (le premier des axiomes traditionnels) : de " -> (x ⊃ (y ⊃ x))" on tire
  1. par Imp-Cons " x -> (y ⊃ x) " et,
  2. de nouveau par Imp-Cons " x, y -> x " qui est valide.

En  revanche,  " x  ⊃ (y ⊃ z) " donne par le même calcul "x, y -> z" qui est invalide
(pour le rendre faux, prendre x et y VRAIs et z FAUX).

Pour compléter notre exemple précédent, établissons la validité  du séquent S2 :

(¬a ∨ (b ⊃ c))   ->    (a ∧ ¬b) , (a ⊃ c)

comme plusieurs règles lui sont applicables, prenons comme principe d'employer chaque fois que possible
une règle qui donne un seul séquent  équivalent, plutôt qu'un  couple,
donc de onner la priorité aux règles  de  la  négation, Imp-Cons, Disj-Cons et Conj-Ant.

S2 =                (¬a ∨ (b ⊃ c))   ->    (a ∧ ¬b) , (a ⊃ c)

  1. Nous appliquons donc Imp-Cons au dernier élément du conséquent, il vient
    S3 =                a, (¬a ∨ (b     ⊃ c))   ->    (a ∧ ¬b) , c

  2. Nous n'échappons pas à un couple  ...   Appliquons Conj-Cons et traitons successivement

  3. S'4 =               a, (¬a ∨ (b ⊃ c))   ->    a, c          qui est valide,
    et

  4. S"4 =               a, (¬a ∨ (b ⊃ c))   ->    ¬b, c
    Par Nég-Cons il vient

  5. S5 =                a, b, (¬a ∨ (b ⊃ c))   ->  c
    De nouveau, nous devons bifurquer : seule Disj-Ant s'applique, pour donner

  6. S'6 =               a, b, ¬a -> c          et
    S"6 =               a, b, (b     ⊃ c) -> c

  7. La première donne par Nég-Ant
    S7 =                a, b, -> a, c                               qui est valide

  8. La seconde bifurque encore, donnant par Imp-Ant
    S'8 =               a, b -> b, c                                qui est valide
    S"8 =               a, b, c -> c                            qui est valide.

La preuve de la validité de S2, donc de S0, et donc que la formule initiale

                    (¬a ∨ (b ⊃ c)) > (a ∧ ¬b ∨ (a ⊃ c))

est bien une tautologie, est ainsi achevée.


Naturellement, d'autres preuves sont possibles, en appliquant les règles dans un ordre différent.
Par  exemple, si on adopte une stratégie "de gauche à droite", en cherchant dans l'antécédent d'abord, puis dans le conséquent,
on obtient:

S2 =                (¬a ∨ (b ⊃ c))   ->    (a ∧ ¬b) , (a ⊃ c)

  1. par Disj-Ant, bifurcation
    S'13 =              ¬a   ->    (a     ∧ ¬b) , (a ⊃ c)
    S"13 =              (b     ⊃ c)   ->    (a ∧ ¬b) , (a ⊃ c)

  2. De S'13, par Neg-Ant
    S14 =                -> a, (a     ∧ ¬b) , (a ⊃ c)

  3. Ici "le bon choix" est manifestement Imp-Cons, qui donne
    S15 =               a -> a, (a     ∧ ¬b), c                     qui est valide, ce qui règle le cas de S'13.

  4. Si "bêtement" nous prenons d'abord Conj-Cons, nous bifurquons à nouveau
    S'16 =               -> a, (a     ⊃ c)      compte-tenu de ce que "a, a = a"
    S"16 =               -> a, ¬b, (a     ⊃ c)

  5. S'16 par Imp-Cons donne
    S17 =                a -> a, c                                  valide

  6. S"16 par Neg-Cons (systématiquement de gauche à droite ...)
    S18 =                b -> a, (a > c)

  7. et enfin par Imp-Cons
    S19 =               a, b -> c                                   valide

Comme on voit, le résultat final (ici, la validité de S'13) ne change pas, mais bien la longueur de la preuve.
Le programme ici proposé, évidemment, suit une stratégie figée de gauche à droite, avec le genre d'inefficacité que
nous  venons de voir. Mais il est plus vite  écrit  qu'un  programme plus "astucieux".

La preuve de S"13 (avec variantes) est laissée en exercice.

III - Système formel

Bien que les observations que nous avons faites précédemment aient énoncé des équivalences entre séquents (ou couples de séquents),
il est clair que les règles que nous en avons tirées s'utilisent dans un seul sens, celui qui fait décroître la complexité des séquents.
En outre, leur mise en œuvre a fait clairement apparaître une structure de preuve arborescente. 
Il est donc naturel de les  reformuler comme des règles de déduction dans le cadre d'un système formel.

a) Langage, axiomes, règles de déduction

Le langage de notre système est formé des séquents. 
Les théorèmes du système seront les séquents valides.

Nous prenons comme axiomes tous les séquents dont l'antécédent et le conséquent ont une intersection non vide.

Les règles de déduction sont au nombre de 8 (2 par connecteur), simples recopies des 8 règles édictées ci-dessus
dans le format où la conclusion est en-dessous du trait et les prémisses au-dessus
(alors qu'auparavant nous disions "Pour <conclusion> il suffit <prémisses>).


                     p2, ..., pm -> p, q1, q2,..., qn
Neg-Ant :           ----------------------------------
                    ¬p, p2, ..., pm -> q1, q2,..., qn


                     q,  p1, p2,..., pm -> q2,..., qn
Neg-Cons :           --------------------------------
                     p1, p2,..., pm-> ¬q, q2,..., qn


            p', p2, ... , pm -> q1, q2,...,qn  ,  p", p2,..., pm -> q1, q2,...,qn
Disj-Ant :     ------------------------------------------------------------------
                          (p' ∨ p"), p2, ... , pm -> q1, q2,...,qn


                     p1, p2,..., pm -> q', q", q2,...,qn
Disj-Cons :            -------------------------------------
                     p1, p2,..., pm -> (q' ∨ q"), q2,...,qn


                     p', p", p2,..., pm -> q1, q2,...,qn
Conj-Ant :             -------------------------------------
                     (p' ∧ p"), p2,..., pm -> q1, q2,...,qn


             p1, p2,..., pm -> q', q2,...,qn  ,  p1, p2,..., pm -> q", q2,...,qn
Conj-Cons :   -----------------------------------------------------------------
                         p1, p2, ... , pm -> (q' ∧ q"), q2,...,qn


             p2,..., pm -> p', q1, q2,...,qn ,  p", p2, ..., pm -> q1, q2,...,qn
Imp-Ant :     -----------------------------------------------------------------
                         (p' ⊃ p"), p2, ... , pm -> q1, q2,...,qn


                     q', p1, p2,..., pm ->  q", q2,...,qn
Imp-Cons :           --------------------------------------
                     p1, p2,..., pm -> (q' ⊃ q"), q2,...,qn

b) Exemples d'arbres de preuve

Loi du tiers exclu :
                                                    Axiome
                                                   --------
                                                    x -> x
                                        Neg-Cons  -----------
                                                   -> x, ¬x
                                        Disj-Cons ------------
                                                   -> (x ∨ ¬x)


Première preuve de S2  :

                                  Axiome          Axiome        Axiome
                               -------------    ----------    ----------
                               a,b, -> a,c      a,b -> b,c ,  a,b,c -> c
                               -----------  I-A ------------------------
                               a,b,¬a -> c       ,       a,b,(b⊃c) -> c
                           D-A ----------------------------------------
                    Axiome                       a,b,(¬a∨(b⊃c)) -> c
              -------------------     Neg-Cons -----------------------
              a,(¬a∨(b⊃c)) -> a,c     ,          a,(¬a∨(b⊃c)) -> ¬b,c
    Conj-Cons --------------------------------------------------------
                             a,(¬a∨(b⊃c)) -> (a∧¬b),c
                 Imp-Cons  -----------------------------
                            (¬a∨(b⊃c)) -> (a∧¬b),(a⊃c)



c) Stratégie de recherche de l'arbre de preuve, programme

Nos règles de production ont la bonne volonté d'utiliser des prémisses qui se déduisent de la conclusion
(au contraire d'une règle comme modus ponens).
Nous pouvons donc utiliser la stratégie de preuve "en marche arrière" (backward chaining), et traduire
l'application d'une règle par un ou deux appels récursifs de la procédure de démonstration.

En outre, les prémisses ont des complexités strictement inférieures à celles des  conclusions,
de sorte que toute application de règle "constitue un progrès vers une solution".
Il n'y a pas de risque de boucle, ni même d'échec et d'obligation de revenir en arrière (back-track).

La seule subtilité est que certains choix sont plus habiles que d'autres, et conduisent plus vite à une solution.

Le programme le plus simple suit une stratégie figée de gauche à droite, en cherchant d'abord dans l'antécédent puis dans le conséquent,
et en appliquant la règle associée au connecteur principal de la première formule non-atomique qu'il trouve.


Exercice :

Modifier le programme pour lui faire employer une stratégie plus raffinée, comme celle que nous avons prise pour la première preuve de S2. Pour ne pas perdre de temps en tests inutiles, on gèrera 10 ensembles au lieu de 4, en distinguant
les formules atomiques, les  négations, les disjonctions, les conjonctions et les implications.
Y a-t-il une stratégie optimale ?


Réalisation en Prolog

/*  L'algorithme de Wang  en SWI-Prolog  */

/*  Dans ce programme, on repre'sente la se'quence courante comme
    un couple de listes de termes Antec et Conseq .
    Ces termes seront e'crits avec la syntaxe concre`te habituelle,
    les connecteurs binaires en position infixe'e a` trois niveaux de priorite's.
    Pour e'viter les conflits avec la syntaxe des listes Prolog, qui utilise le symbole "|",
    on revient ici aux noms français des connecteurs,
    et on introduit donc les conventions ne'cessaires a` l'usage du lecteur Prolog comme suit  :
*/

:- op(950, yfx, [imp]) .
:- op(925, yfx, [ou]) .
:- op(900, yfx, [et]) .
:- op(850, fx, [non]) .

/*  Il sera utile de ve'rifier si Antec et Conseq ont ou non une formule en commun.
    La solution ici retenue s'applique a` des formule atomiques repre'sente'es par des termes Prolog
    dont le foncteur n'est pas un connecteur.
*/

% inter(L, M) :- append(X, [A|Y], L), append(U, [A|V], M).

 inter(L, M) :- intersection(L, M, [X|Y]).


/* Les deux listes de formules Antec et Conseq seront ge're'es avec les formules
   non-triviales en te^te et les autres (formules atomiques) en queue ;
   de'finissons donc comment une nouvelle formule doit s'ajouter a` une liste.
*/

consp(X imp Y). consp(X ou Y). consp(X et Y). consp(non X).

ajouter(F, L, [F|L]) :- consp(F), !.
ajouter(F, L, M) :- append(L, [F], M).

/* Enonçons a` pre'sent les re`gles gouvernant la validite' d'une se'quence.
   Le pre'dicat valide sera charge' en outre de ramener la liste des e'ventuels contre-exemples
   pour les propositions  qui ne sont pas des tautologies.
   On rappelle que cette liste peut e^tre vue comme une repre'sentation de la proposition
   en forme  conjonctive re'duite.
*/

valide(Antec, Conseq, []) :- inter(Antec, Conseq), !.

/* Les re`gles visant la ne'gation.*/
valide( [non X | R], Conseq, Contrex) :- ! ,
    ajouter(X, Conseq, Ncsq), valide(R, Ncsq, Contrex).

valide(Antec , [non X | R], Contrex) :- !,
    ajouter(X, Antec, Ntc), valide(Ntc, R, Contrex).

/* Les re`gles re'gissant la disjonction.*/

 valide( [X ou Y | R], Conseq, Contrex) :- !,
     ajouter(X, R, Ntc1), valide(Ntc1, Conseq, Contrex1),
     ajouter(Y, R, Ntc2), valide(Ntc2, Conseq, Contrex2),
     append(Contrex1, Contrex2, Contrex).

 valide(Antec, [X ou Y | R], Contrex) :- !,
     ajouter(X, R, Ncsq1), ajouter(Y, Ncsq1, Ncsq2),
     valide(Antec, Ncsq2, Contrex).

/* Les re`gles sur la conjonction.*/

 valide([X et Y | R], Conseq, Contrex) :- !,
     ajouter(X, R, Ntc1), ajouter(Y, Ntc1, Ntc2),
     valide(Ntc2, Conseq, Contrex).

 valide(Antec, [X et Y | R], Contrex) :- !,
     ajouter(X, R, Ncsq1), valide(Antec, Ncsq1, Contrex1),
     ajouter(Y, R, Ncsq2), valide(Antec, Ncsq2, Contrex2),
     append(Contrex1, Contrex2, Contrex).


/* Enfin, les re`gles sur l'implication.*/

 valide([X imp Y | R], Conseq, Contrex) :- !,
     ajouter(Y, R, Ntc), valide(Ntc, Conseq, Contrex1),
     ajouter(X, Conseq, Ncsq), valide(R , Ncsq, Contrex2),
     append(Contrex1, Contrex2, Contrex).


 valide(Antec, [X imp Y | R], Contrex) :- !,
     ajouter(X, Antec, Ntc), ajouter(Y, R, Ncsq),
     valide(Ntc, Ncsq, Contrex).

 /* Et si aucune des situations pre'ce'dentes ne se pre'sente, c'est que toutes les
formules sont atomiques, et comme Antec et Conseq ont une intersection vide,
il s'ensuit que la se'quence n'est pas valide.*/

valide(Antec, Conseq, [[Antec, Conseq]]) :- !,
    write('Pas une tautologie'),  nl.    

/* Ceci acheve la de'finition du pre'dicat "valide" ; voici un pre'dicat "top-level" pour le mettre en œuvre commode'ment.*/

wang(Formule, Cx) :- valide([], [Formule], Cx),
                                write('OK'), nl.

/* Quelques exemples de tautologies (fabriquer des non-tautologies, c'est plus facile!) . */

w1 :- wang(a ou non a, []).

w2 :- wang(a imp (b imp a), []).

w3 :- wang((a ou b) et non a imp b, []).

w4 :- wang((a imp b) imp (non b imp non a), []).

w5 :- wang((a imp b) et a imp b, []).

w6 :- wang(non a ou (b imp c) imp a et non b ou (a imp c), []).

myst :- wang((pp imp qq) et
           (qq imp rr) et
           (rr imp ss) et
           (tt imp non ss) imp (pp imp non tt), []).

big :- wang(
        (x et y et u) ou (non x et non y et u) ou
        (non x et y et non u) ou (x et non y et non u)
        ou
        (non x et y et v) ou (x et non y et v) ou
        (x et y et non v) ou (non x et non y et non v)
        ou
        (non z et t et v) ou (z et non t et v) ou
        (z et t et non v) ou (non z et non t et non v)
        ou
        (non z et t et u) ou (z et non t et u) ou
        (z et t et non u) ou (non z et non t et non u)
        , []).

/*
-----------------------------------------------------------------
| ?- myst.
OK

yes
| ?- wang(d ou c imp a et non b ou c, X).
Pas une tautologie
Pas une tautologie
OK

X = [[[d],[c,a]], [[d,b],[c]]]
yes

*/

Application à la réduction des conditions de vérification

qr

a >= 0 et b > 0 imp a = b*0+a et a >= 0

a = b*q+r et r >= 0 et r >= b imp a = b*(q+1)+(r-b) et r-b >= 0

a = b*q+r et r >= 0 et non(r >= b) imp a = b*q+r et r >= 0 et r < b

transp. arith.
x=a et y=b imp (x+y)-((x+y)-y)=b et (x+y)-y=a