Générateur de formules aléatoires

On perfectionne notre grammaire en indiquant des poids entre crochet pour chaque alternative, et aussi pour donner une proirité syntaxique à chaque connecteur. L'entête précise le symbole d'entrée, la liste des symboles non-terminaux, la liste des connecteurs avec leur priorité affichée entre crochet. Les connecteurs et les variables sont représentés par des caractères autres que { , } [ ] car ils sont utilisées pour rédiger la grammaire.



La programmation doit pouvoir se faire la plus naturellement possible. On programme un automate :

var X=[] 		// Liste des symboles non-terminaux.
Rb() // lit tous les éventuelles caractères blancs. let x=R("Entrée","Symbole","Connecteur") // lit "Entrée" ou "Symbole" ou "Connecteur"
// et retourne respectivement 0 ou 1 ou 2, sinon génère une erreur.
switch (x) case 0: Rb()
R("=") Rb() Rc(E) break; case 1: Rb Rb()
// lit tous les éventuelles caractères blancs. R("Symbole") // lit "Symbole" ou génère une erreur. Rb() R("=") Rb()
R("{") i=0 // index des symboles. X[i] désigne le (i+1)ième symbole
do { Rb() Rc(X[i]) // lit un caractère et le mémorise dans X[i] i++ Rb()
Rc(c) } while (c=",") if (c!="}") erreur();

 

6) Analogie et structuration

Dés que la structure booléenne de la logique est posée, on peut déjà y percevoir les embryons des grandes structures simples et fondamentales révélées par les mathématiques que sont les relations d'équivalence, les relations d'ordre, les treillis et les structures de corps.

6.1) Connecteurs s'appliquant à des ensembles

Les connecteurs `"∧","∨","↔","⊕"`, sont associatifs et commutatifs, autrement dit, ils peuvent s'appliquer à un ensemble de propositions. On définit donc des connecteurs s'appliquant à un ensemble fini quelconque de variables booléennes :

La conjonction `A` :
`A^"∧"` signifie que chaque variable booléenne appartenant à `A` est vrai.

La disjonction `A` :
`A^"∨"`
signifie qu'il existe au moins une variable booléenne appartenant à `A` qui est vrai.

La parité `A` :
`A^"↔"`
signifie qu'il y a une parité ou une imparité de vrai parmi l'ensemble `A` de variables booléennes selon que celui-ci est respectivement paire ou impaire.

L'imparité `A` :
`A^"⊕"`
signifie qu'il y a une imparité ou une parité de vrai parmi l'ensemble `A` de variables booléennes selon que celui-ci est respectivement paire ou impaire.

Autrement dit :

Cardinal 3
Cardinal 2
Singleton
Ensemble
vide
`{x,y,z}^"∧" ↔ (x"∧"y)"∧"z` `{x,y}^"∧" ↔(x"∧"y)` `{x}^"∧" ↔x` `{}^"∧" ↔`1
`{x,y,z}^"∨" ↔ (x"∨"y)"∨"z` `{x,y}^"∨" ↔(x"∨"y)` `{x}^"∨" ↔x` `{}^"∨" ↔`0
`{x,y,z}^"↔" ↔ (x"↔"y)"↔"z` `{x,y}^"↔" ↔(x"↔"y)` `{x}^"↔" ↔x` `{}^"↔"↔`1
`{x,y,z}^"⊕" ↔ (x"⊕"y)"⊕"z` `{x,y}^"⊕" ↔(x"⊕"y)` `{x}^"⊕" ↔"¬"x` `{}^"⊕" ↔`0

La conjonction est considérée comme un ensemble de conditions restrictives, donc l'absence de condition restrictive vaut le vrai. La disjonction est considérée à l'inverse comme un ensemble de solutions, donc l'absence de solution vaut le faux. Cette définition satisfait la loi de Morgan.

Puis il existe deux analogies fondamentales, l'une se rapportant aux classes d'équivalence, définissant l'opérateur d'égalité appliqué à un ensemble de variables booléennes, l'autre se rapportant aux relations d'ordre totale que forme les suites causales ou ordonnées d'implications successives, définissant l'opérateur d'implication appliqué à une suite de variables booléennes :

La classe `A` :
`A^"="`
signifie qu'il y a une équivalence entre chaque variable booléenne de l'ensemble `A`.

La suite causale (suite croissante) `S` :
`S^"→"`
signifie qu'il y a une implication toujours dans le même sens entre chaque variable booléenne successive de la suite `S`.

Autrement dit :

Cardinal 3
Cardinal 2
Singleton
Ensemble
vide
`{x,y,z}^"=" ↔ (x"↔"y")∧("y"↔"z")` `{x,y}^"=" ↔(x"↔"y)` `{x}^"=" ↔`1 `{}^"=" ↔`1
`(x,y,z)^"→" ↔ (x"→"y")∧("y"→"z")` `(x,y)^"→" ↔(x"→"y)` `(x)^"→" ↔`1 `()^"→" ↔`1

Un ensemble de variable égale, est faux seulement s'il existe deux variables distincts dans cet ensemble. Donc appliqué à une seule ou aucune variable booléenne c'est toujours vrai.

Une suite causale est vrai lorsque la suite de booléens est croissante, et elle est fausse s'il existe une variable fausse qui arrive après une variable vrai. Donc appliqué à une seule ou aucune variable booléenne elle vaut toujours vrai.

La notion de suite croissante qui désigne un ensemble totalement ordonnée de variables booléennes, se généralise en la notion d'ordre partiel sur un ensemble de variables booléennes.

6.2) Les deux corps symétriques des booléens

Puis il existe deux corps symétrtiques des booléens que l'on présente sous forme de quintuplet avec comme argument dans l'ordre ; le nom de la structure qui porte sur le même ensemble sous-jacent qui est l'ensemble des booléens `{0,1}`, l'addition, l'élément neutre de l'addition, la multiplication, l'élément neutre de la multiplication :

`sf"Corps"(B, "⊕",0,"∧",1)`

`sf"Corps"(barB, "↔",1,"∨",0)`

La structure de corps résoud les équations en logique propositionnelle. Considérons 4 variables booléennes `x,y,z,t`. Chaque polynôme correspond à une propositions logiquement différentiable pour au moins une valeur booléenne de `x,y,z,t`. Donc pour savoir si deux propositions sont équivalentes, on les développe en polynôme sous forme normale pour savoir s'il s'agit du même polynôme. Cela donne l'algorithme de résolution par développement de polynômes.

6.3) Le treillis des booléens

Puis il existe un treillis des booléens caractérisé par la distributivité de `"∧"` sur `"∨"` et de `"∧"` sur `"∨"`.

`x"∧"(y"∨"z) ↔ (x"∧"y)"∨"(x"∧"z)`
`x"∨"(y"∧"z) ↔ (x"∨"y)"∨"(x"∨"z)`

Chaque proposition peut se décomposer en une conjonction de clauses ou symétriquement en une disjonction d'état :

`x"→"y ↔ x"∨¬"y`
`x"↔"y ↔ (x"∨¬"y)"∧"(y"∨¬"x)`
`x"↔"y ↔ (x"∧"y)"∨"(¬x"∧¬"y)`
`x"⊕"y ↔ ("¬"x"∧"y)"∨"("¬"y"∧"x)`
`x"⊕"y ↔ (x"∨"y)"∧"("¬"x"∨¬"y)`

Un littéral est une variable booléenne ou sa négation. Grace à la loi de Morgan, il est possible de supprimer la négation dans le corps des formules et de la garder que au niveau de la variable booléenne.

`"¬"(x"∧"y) ↔ "¬"x"∨¬"y`
`"¬"(x"∨"y) ↔ "¬"x"∧¬"y`
`"¬"(x"→"y) ↔ x"∧¬"y`
`"¬"(x"↔"y) ↔ x"⊕"y`
`"¬"(x"⊕"y) ↔ x"↔"y`

Cela donne l'algorithme de résolution par développement en une conjonction de clauses, ou en une disjonction d'états.

7) Algorithmes de résolution du calcul proportionnel

Voici 4 méthodes pour déterminer si une proposition est une tautologie, une antilogie, ou est indécidable :

  1. Par la table de vérité.
  2. Par le développement en une conjonction de clauses, ou en une disjonction d'états.
  3. Dans le corps `sf"Corps"(B, "⊕",0,"∧",1)` ou bien dans le corps symétrique `sf"Corps"(barB, "↔",1,"∨",0)` par développement de polynômes.
  4. Dans le langage de connecteur `{"¬", "⇒"}` par le système axiomatique de Hilbert.
  5. Dans le langage de connecteur `{"¬", "et", "ou"}` par la résolution de la conjonction de clauses, ou bien symétriquement par la résolution de la disjonction d'états.

7.1) La table de vérité

Cette méthode consiste à procéder à tous les testes possibles en attribuant aux variables booléennes `x_1,x_2,x_3,..., x_n ` à tour de rôle leur valeur possibles `0` ou `1`, soit `2^n` différentes valeurs booléennes possibles. S'il y a au moins un résultat égal à `1` alors la proposition est satisfaisable. S'il y a au moins un résultat égal à `0` alors la proposition est de négation satisfaisable. Et s'il a au moins un résultat égal à `0` et au moins un résultat égal à `1` alors la proposition est indécidable. Si les résultats sont toujours égaux à `0` alors la proposition est une antilogie. Si les résultats sont toujours égaux à `1` alors la proposition est une tautologie.

7.2) Algorithme de résolution par développement de polynômes.

On transcrit la proposition sous forme d'un polynôme dans un des corps booléens symétriques `sf"Corps"(B, "⊕",0,"∧",1)` ou bien `sf"Corps"(barB, "↔",1,"∨",0)`, qui sont des corps de caractéristique 2 que l'on renomme en `sf"Corps"(K,"+",0,"×",1)`.

La proposition se transcrit en un unique polynôme, une forme normale développée en enlevant les puissances doubles `x^2 = x` et en enlevant les monômes doubles `2x = x"+"x = 0`, puisque nous sommes dans un corps de caractèristique 2. La proposition est tautologique si elle est égale au polynôme `1`, elle est antilogique si elle est égale au polynôme `0`, et elle est indécidable si elle est égale à un polynôme autre que `0` ou `1`.

7.3) Le système axiomatique de Hilbert

Cette théorie utilise les connecteurs logiques `{¬, "⇒"}` qui sont suffisants pour engendrer tous les connecteurs logiques. Et elle utilise des inconnnus que l'on note `a,b,c,...` et qui jouent ici non pas le rôle de variable booléenne mais un rôle uniquement symbolique puisque la résolution s'opère uniquement de façon syntaxique. Les connecteurs n'opèrent pas de calcul booléen, ils ne sont que symboliques.

Puis on utilise des variables supplémentaires dites libres `A,B,C,...` et le connecteur de déduction `⊢` pour écrire les règles de déduction.

On accumule dans un sac toutes les propositions que l'on démontre. Les règles de déduction prennent des propositions présentes dans le sac et opère un calcul pour produire le cas échéant une nouvelle proposition que l'on rajoute dans le sac. Et il y a 4 règles de déductions  :

`(A, A"⇒"B)⊢ B`
`⊢ A "⇒" (B "⇒" A)`
`⊢ (A "⇒" (B "⇒" C)) "⇒" ((A "⇒" B) "⇒" (A "⇒" C))`
`⊢ ("¬"A "⇒" "¬"B) "⇒" (B "⇒" A)`

La première règle s'appelle le modus ponens. Elle prend en entrée deux propositions présentes dans le sac, et si l'unification avec l'entête réussit, elle produit une nouvelle proposition que l'on rajoute dans le sac. Les 3 autres règles ont une liste vide comme entête et engendrent des propositions où `A,B,C` parcourent toutes les propositions du langage.

Ce moteur produit exactement l'ensemble de toutes les propositions tautologiques. Pour détecter les propositions indécidables, il faut un autre algorithme.

Si on commence l'algorithme avec un sac contenant une proposition initiale `P`, on produit alors exactement l'ensemble de toutes les déductions possibles de `P`.

7.4) Algorithme de résolution par développement en une conjonction de clauses, ou en une disjonction d'états.

On appelle littéral, une variable booléenne préfixé ou non par le connecteur de négation. Les littéraux sont `x`,`"¬"x`,`y`,`"¬"y`,`z`,`"¬"z`.... On appelle proposition une composition de connecteurs et de variables booléennes. On appel clause une disjonction de littéraux. On appel état une conjonction de littéraux.

On transcrit la proposition en utilisant que les connecteurs `"et"`, `"ou"` et des littéraux. Puis on développe en une disjonction d'états pour prouver la satisfaisabilité, ou en une conjonction de clauses pour prouver la satisfaisabilité de la négation.

7.4.1) Pour prouver l'antilogie d'une conjonction de clauses

Uns fois la proposition développée en une conjonction de clauses ce qui assure au moins la satisfaisabilité de sa négation, on applique l'algorithme suivant. Les règles de déduction du calcul propositionnel sont plus simples dans un langage logique n'utilisant qu'une conjonctions de clauses de littéraux. Une clause est un couple d'ensembles finis de variables booléennes `(A,B)`, le premier ensemble regroupe les variables affirmées dans la clause, et le second ensemble regroupe les variables négativées dans la clause. Par exemple :

`A={x,x,z}`
`B={u,v}`
`(A,B) = ({x,y,z},{u,v}) = x "ou" y "ou" z "ou" "¬"u "ou" "¬"v`

On choisit une proposition `P` de départ que l'on décompose en une conjonction de clauses. On regroupe ces clauses de départ dans un sac. Chaque clause contenue dans le sac apporte une contrainte. Le sac correspond à une conjonction. Puis on accumule dans le sac, toutes les clauses que l'on démontre, et on supprime celles qui sont redondantes, jusqu'à déduire le "faux" (la clause vide) auquel cas la proposition est une antilogie, (ou jusqu'à obtenir un sac vide si toutes les clauses sont tautologiques à la suite d'une hypothèse extérieure, auquel cas la proposition est une tautologie). L'algorithme est défini en 5 règles :

  1. Lorsque dans le sac il y a une clause `(A,B)` telle que `A"∩"B≠{}` alors elle est tautologique et doit être enlevée, car elle n'apporte aucune contrainte supplémentaire.
  2. Lorsque dans le sac il y a deux clauses `(A,B), (C,D)` incluses l'une dans l'autre `(A,B) "⊆" (C,D)` c'est à dire `A"⊆"C" et "B"⊆"D`, la plus grande doit être enlevée, car elle n'apporte aucune information.
     
  3. Lorsque dans le sac il y a deux clauses `(A,B), (C,D)` qui s'opposent pour une seule variable c'est à dire lorsque `(A"∩"D)uu(B"∩"C)` est un singleton, on peut déduire la clause union dans laquelle on enlève la seule variable `x` appartenant à `(A"∩"D)uu(B"∩"C)`, et on ajoute cette nouvelle clause `((A"∪"C)"\"{x},(B"∪"D)"\"{x})` dans le sac. Par exemple les deux clauses `({a,b,c},{d,e})` et `({b,c},{a,d})` produisent la clause union dans laquelle on enlève la variable `a` c'est à dire `({b,c},{d,e})`.
     
  4. Toute conjonction contenant une clause vide `({},{})` désigne l'antilogie. Ainsi, si le sac contient la clause vide, on conclut "faux".
     
  5. La conjonction vide `{}` désigne la tautologie. Ainsi lorsque le sac devient vide, on conclut "vrai". (Cela peut arriver par une intervention extérieur, si on prend une hypothèse qui rend tautologique toutes les clauses dans le sac.)

Le moteur s'arrête si la conjonction contient la clause vide et auquel cas la proposition `P` est une antilogie, (ou si la conjonction devient vide et auquel cas la proposition `P` est une tautologie).

7.4.2) Pour prouver la tautologie

Par négation nous obtenons le mécanisme symétrique. Une fois la proposition développée en une disjonction d'états ce qui assure au moins sa satisfaisabilité, on applique l'algorithme suivant. Les règles de déduction du calcul propositionnel sont plus simples dans un langage logique n'utilisant qu'une disjonction d'états de littéraux. Un état est un couple d'ensembles finis de variables booléennes `(A,B)`, le premier ensemble regroupe les variables affirmées dans l'état, et le second ensemble regroupe les variables négativées dans l'état. Par exemple :

`A={a,b,c]`
`B={d,e}`
`(A,B) =({a,b,c},{d,e}) = a "et" b "et" c "et" "¬"d "et" "¬"e`

On choisit une proposition `P` de départ que l'on décompose en une disjonction d'états. On regroupe ces états de départ dans un sac. Chaque état contenu dans le sac apporte une solution. Le sac correspond à une grande disjonction. Il ne fait que réduire une solution plus générale.

Puis on accumule dans le sac, toutes les états possibles que l'on démontre avec ce jeu de règles symétriques, et on supprime ceux qui sont redondants, jusqu'à déduire le "vrai" (l'état vide) auquel cas la proposition est une tautologie, (ou jusqu'à obtenir un sac vide si tous les états sont antilogiques à la suite d'une hypothèse extérieur, auquel cas la proposition est une antilogie). L'algorithme est défini en 5 règles :

  1. Lorsque dans le sac il y a un état `(A,B)` tel que `A"∩"B≠{}` alors il est antilogique et doit être enlevée, car il ne se réalise jamais.
  2. Lorsque dans le sac il y a deux états `(A,B), (C,D) ` inclus l'un dans l'autre `(A,B) "⊆" (C,D)` c'est à dire `A"⊆"C" et "B"⊆"D`, le plus grand doit être enlevé, car il ne se réalise que si le plus petit se réalise, et donc ne libère aucune contrainte, n'apporte aucune nouvelle alternative.
     
  3. Lorsque dans le sac il y a deux états `(A,B), (C,D)` qui s'opposent pour une seule variable c'est à dire lorsque `(A"∩"D)uu(B"∩"C)` est un singleton, on peut déduire une nouvelle alternative qu'est l'état union dans laquelle on enlève la seule variable `x` appartenant à `(A"∩"D)uu(B"∩"C)`, et on ajoute cette nouvelle solution `((A"∪"C)"\"{x},(B"∪"D)"\"{x})` dans le sac. Par exemple les deux états `({a,b,c},{d,e})` et `({b,c},{a,d})` produisent l'état union dans laquelle on enlève la variable `a` c'est à dire `({b,c},{d,e})`.
     
  4. Toute disjonction contenant un état vide `({},{})` désigne la tautologie. Ainsi si le sac contient l'état vide, on conclut "vrai".
     
  5. La disjonction vide `{}` désigne l'antilogie. Ainsi si le sac devient vide, on conclut "faux". (Cela peut arriver par une intervention extérieur, si on prend une hypothèse qui rend antilogique toutes les clauses dans le sac.)

Le moteur s'arrête si la disjonction contient l'état vide et auquel cas la proposition `P` est une tautologie, (ou si la disjonction devient vide et auquel cas la proposition `P` est une antilogie).

7.5) Le système de déduction naturelle

Pour pouvoir étendre ce système de déduction à des langages logiques plus riches tel le langage logique du premier ordre, on va opter pour une cinquième méthode dite "naturelle" qui introduit et élimine chaque connecteur logique par une règle de déduction spécifique.

Mais celle-ci se définit dans le cadre d'une conjonction de propositions formant un ensemble de propositions sur lequel on applique des règles de transformations. Pour ne pas être tributaire de cet arbitraire, il faut considérer les autres ensembles de propositions évoqués au chapitre 6, à savoir, les conjonctions, les disjonctions, les parités, les imparités, les classes, et les suites croissantes et peut-être même d'une façon plus générale, les ensembles de variables booléennes munie d'un ordre partiel. Sans avancer davantage dans cette voie de travail, on peut parallèlement à cela proposer une approche beaucoup plus pragmatique et empirique, susceptible de produire immédiatement des applications, et qui stimulera davantage nos lecteurs car moins ingrate.

8) Résolution de la satisfaisabilité par la méthode de Newton

Pour rechercher la satisfaisabilité d'une proposition à l'aide de réseaux de neurones, on définie une logique continue où les valeurs logiques appartiennent à un intervalle réel `]0,1[` et où les connecteurs logique sont des fonctions analytiques. L'exigence de continuité nous oblige à prendre un domaine ouvert, ce qui peut paraître surprenant. Dans cette optique, le vrai absolu noté `1` et le faux absolu noté `0` sont hors domaine et n'apparaissent donc jamais. Les propositions peuvent être quasiment vrais ou quasiment fausses mais jamais complétement. Cela ne gène pas la recherche car la méthode de Newton procède par approximation en suivant les plus grandes pentes. (Et de même dans un réseau de neurone où l'apprentissage procède par approximation en suivant les plus grandes pentes dans la rétropropagation des erreurs.)

Le calcul que fait un neurone est une sigmoïde générique de `]0,1[` vers `]0,1[` et qui possède une raideur initialement fixée à `4pi`. (On peut aussi la fixer à `3pi` ou moins encore s'il y a beaucoup de niveaux de profondeur).

`f(x) = 1/(1+e^(4pi(-x+1/2)))`

Si on répète cette transormation, on obtient une quasi-sigmoïde 2 à 3 fois plus raide. Le connecteur de négation correspond à une telle sigmoïde mais envoyant `0` sur `1` et envoyant `1` sur `0`, ce que l'on obtient en remplaçant dans la sigmoïde `f` la variable `x` par `1"-"x`.

`("¬"x) = 1/(1+e^(4pi(x-1/2)))`

Le connecteur de conjonction `x "et" y` s'obtient en remplaçant dans la sigmoïde `f` la variable `x` par `xy`.

`(x "et" y) = 1/(1+e^(4pi(-xy + 1/2)))`

Le connecteur de disjonction `x "ou" y` s'obtient en remplaçant dans la sigmoïde `f` la variable `x` par `x"+"y"-"xy`.

`(x "ou" y) = 1/(1+e^(4pi(xy-x-y + 1/2)))`

Le connecteur d'implication `x"⇒"y` qui est égal à `"¬"x "ou" y` s'obtient en remplaçant dans la sigmoïde `f` la variable `x` par `1"-"x"+"y"-"(1"-"x)y` `=` `1"-"x"+"xy`

`(x"⇒"y) = 1/(1+e^(4pi(-xy+x-1/2)))`

Le connecteur d'équivalence `x"⇔"y` qui est égal à `(x"⇒"y) "et" (y"⇒"x)` s'obtient en remplaçant dans la sigmoïde `f` la variable `x` par `(1"-"x"+"xy)(1"-"y"+"xy)` `=` `1"-"x"-"y"+"xy"+"xy"-"x^2y"-"xy^2"+"x^2y^2`. On remplace `x^2` par `x` et `y^2` par `y`. Cela ne change pas la valeur résultat dans les cas `0` ou `1`. On obtient alors la formule `1"-"x"-"y"+"2xy` qui est du même degrés que celle des autres connecteurs binaires.

`x"⇔"y = 1/(1+e^(4pi(-2xy+x+y-1/2)))`

Le connecteur ou exclusif `x"⊕"y` qui est égal à `"¬"(x"⇔"y)` s'obtient en remplaçant dans la sigmoïde `f` la variable `x` par `1"-"(1"-"x"-"y"+"2xy)` `=` `x"+"y"-"2xy`

`(x"⊕"y) = 1/(1+e^(4pi(2xy-x-y+1/2)))`

Etant donnée une formule `P(x_1,x_2,x_3...,x_n) = P(vec x)` celle-ci peut ainsi se traduire en une fonction continue de `"]"0,1"["^n` vers `]0,1[` comme composée des sigmoïdes qui la composent. Et il est alors possible de rechercher les extremums de cette fonction analytique par la méthode de Newton vectorielle. C'est une recherche des racines de la dérivée. Avec l'itération suivante :

 

---- 23 avril 2024 ----

 

 

`vec x :=vec x - P’’^-1"×"P’`

`P’ = ( ((del P)/dx_1), ((del P)/dx_2),(...))`

`P’’ = ( ((del^2P)/dx_1^2, (del^2P)/(dx_1dx_2), ... ),((del^2 P)/(dx_1dx_2),(del^2 P)/dx_2^2,...), (...,...,...))`

 

 

 

 

 

 

 

 

 

9) La topologie de la logique du premier ordre

Si vous avez fait un peu de topologie vous aurez remarqué que des notions de topologies apparaissent dés qu'il est nécessaire de réunir ou de procéder à une intersection d'une infinités d'ensembles. Et c'est précisément le cas dans la logique du premier ordre pour interpréter les premières formules `AAxP(x)` et `EExP(x)`.

 

---- 23 avril 2024 ----