L'algorithme de Wang pour le calcul des propositions


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équences
   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, 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", avec des variantes
et une extension au calcul des prédicats. Il s'agit ici du
"premier  programme" de Wang, système "P".

L'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équences


L'algorithme  de Wang résulte de l'application au calcul propositionnel d'une
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équences, de la forme

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

ou les pi, qj sont des propositions.  L'ensemble des pi forme l'antécédent de
la séquence, 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 etant 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é

Une séquence 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)

Une telle séquence 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 était une séquence 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
resultat  est VRAI sauf si l'une des formules de l'ensemble est fausse (resp.
FAUX sauf si l'une des formules est vraie).

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

Une séquence 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.

La séquence 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équences.

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

II - L'algorithme de Wang

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

Pour qu'une séquence 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 de la séquence
sont des variables  (propositions  atomiques).  
En effet, dans le cas contraite, l'ensemble des variables apparaissant dans la séquence
se divise en deux sous-enesmebles disjoints, celles qui apparaissent dans l'antécédent 
et celles qui apparaissent dans le conséquent.
En donnant à toutes les premières la valeur VRAI et aux secondes  la valeur FAUX,
on obtient un système de valeurs des variables qui rend fausse l'implication associée a la séquence.
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 : la séquence  " 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 à la séquence : (a ∧ b) > (c ∨ d) prend la valeur FAUX.

Appelons séquence atomique une séquence dont tous les éléments sont des
variables. Pour une telle séquence, nous pouvons décider immédiatement
de sa validité. Nous allons à présent voir comment ramener la validité de
toute séquence à celle d'un ensemble fini de séquences atomiques.

Definissons la "complexité" d'une séquence comme le nombre total de
connecteurs qui apparaissent dans ses éléments. Une séquence atomique est de
complexité nulle. Nous allons voir comment passer d'une séquence de
complexité positive à une séquence équivalente, ou a un couple de séquences
équivalent, de complexité strictement plus faible.

Nous  adpterons  pour ce faire l'approche de la logique connue sous le nom de
déduction naturelle : à chaque connecteur sont attachées 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 une séquence 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.  La séquence S s'écrit alors :

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

Observation :  La  séquence S est équivalente à la séquence S' obtenue en
"faisant passer p dans le conséquent" :

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

Par "équivalente", nous entendons que S est valide si et seulement si S' est valide.

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. Dans le
premier, la conclusion est immédiate, dans le second la validité de S
entraîne que l'une des qj est vraie, et la conclusion suit.

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  de  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É DE LA SÉQUENCE

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

            IL SUFFIT D'ÉTABLIR CELLE DE LA SÉQUENCE

                     "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'une séquence donnée à celle d'une séquence où aucune négation ne
figure plus dans l'antécédent.

On peut faire l'observation symétrique et voir qu'une  séquence où une
négation apparaît dans le conséquent est équivalente à la séquence obtenue 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É DE LA SÉQUENCE

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

           IL SUFFIT D'ÉTABLIR CELLE DE LA SÉQUENCE

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

           ET RÉCIPROQUEMENT.



L'usage systématique de ces deux règles permet donc de passer d'une séquence
donnée à une séquence équivalente (quant à sa validité) ne contenant plus
aucune formule de la forme (NON 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 à une séquence,
jointe à l'associativité de la disjonction, montre qu'une séquence S où une
disjonction apparaît dans le conséquent est équivalente à la séquence 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 une séquence 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.
Une séquence 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 : si c'est l'une, la validité de S entraîne
celle de S', si c'est l'autre, celle de S".  La réciproque est immédiate. 
On notera  que les deux séquences S' et S" ont chacune une complexité au plus
un de moins que S (la somme de leurs complexités vaut un de moins).

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

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

est valide si et seulement si les deux suivantes, 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É DE LA SÉQUENCE

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

          IL SUFFIT D'ÉTABLIR CELLE DE LA SÉQUENCE

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

          ET CELLE DE LA SÉQUENCE

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

          ET RÉCIPROQUEMENT.



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

          POUR DÉMONTRER LA VALIDITÉ DE LA SÉQUENCE

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

          IL SUFFIT D'ÉTABLIR CELLE DE LA SÉQUENCE

                  " 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É DE LA SÉQUENCE

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

          IL SUFFIT D'ÉTABLIR CELLE DE LA SÉQUENCE

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

          ET RÉCIPROQUEMENT.


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

          POUR DÉMONTRER LA VALIDITÉ DE LA SÉQUENCE

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

          IL SUFFIT D'ÉTABLIR CELLE DE LA SÉQUENCE

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

          ET CELLE DE LA SÉQUENCE

                  " 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", une séquence 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équences

                 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équences 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É DE LA SÉQUENCE

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

          IL SUFFIT D'ÉTABLIR CELLE DE LA SÉQUENCE

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

          ET CELLE DE LA SÉQUENCE

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

          ET RÉCIPROQUEMENT.



De même, une séquence 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É DE LA SÉQUENCE

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

          IL SUFFIT D'ÉTABLIR CELLE DE LA SÉQUENCE

          " 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équence avec un
antécédent non-vide : par exemple, la tautologie

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

se traduit "officiellement" par la séquence avec antécédent vide

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

mais, vu l'interprétation des séquences 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 la séquence 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 la séquence " -> (x ⊃ x) " qui via Imp-Cons donne
          " x -> x " qui est valide.

" x  ∨ ¬x "  (loi  du  tiers  exclu)  :  se traduit par " -> (x ∨ ¬x) ", par
          Disj-Cons on obtient " -> x , ¬x " et par Nég-Cons " x -> x " valide.

" x ⊃ (y ⊃ x) " (le premier des axiomes traditionnels) : de " -> (x ⊃ (y ⊃ x))"
          on tire par Imp-Cons " x -> (y ⊃ x) " et, 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 la rendre fausse, prendre x et y VRAIs et z FAUX).

Pour compléter notre exemple précédent, établissons la validité  de la
séquence S2 : comme plusieurs règles lui sont applicables, prenons comme
principe d'employer chaque fois que possible une règle qui donne une seule
séquence  équivalente, plutôt qu'un  couple  (règles  de  la  négation, Imp-Cons,
Disj-Cons et Conj-Ant).

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

Nous appliquons donc Imp-Cons au dernier élément du conséquent, il vient

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

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

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

S"4 =               a, (¬a ∨ (b ⊃ c))   ->    ¬b, c

Par Nég-Cons il vient

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

De nouveau, nous devons bifurquer : seule Disj-Ant s'applique, pour donner

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

La première donne par Nég-Ant

S7 =                a, b, -> a, c                           qui est valide

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)

par Disj-Ant, bifurcation

S'13 =              ¬a   ->    (a ∧ ¬b) , (a ⊃ c)
S"13 =              (b ⊃ c)   ->    (a ∧ ¬b) , (a ⊃ c)

De S'13, par Neg-Ant

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

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.

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)

S'16 par Imp-Cons donne

S17 =                a -> a, c                              valide

S"16 par Neg-Cons (systématiquement de gauche à droite ...)

S18 =                b -> a, (a > c)

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équences (ou couples de séquences), 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équences. 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équences. 
Les théorèmes du système seront les séquences valides.

Nous prenons comme axiomes toutes les séquences 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).
L'application d'une règle se traduit donc 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 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(900, yfx, [imp]) .
:- op(800, yfx, [ou]) .
:- op(700, yfx, [et]) .
:- op(600, 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 atomes Prolog.
    Il faudra la raffiner pour traiter des objets plus complexes.
*/

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

concat([], X, X). 
concat([A|X], Y, [A|Z]) :- concat(X, Y, Z).

/* Les deux listes de formules Antec et Conseq seront ge're'es avec les formules
   non-triviales en te^te et les variables (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) :- concat(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),
    concat(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),
    concat(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),
    concat(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

*/