Implémentation d'un programme de logique mathématique en C

Implémentation d'un programme de logique mathématique en C - C - Programmation

Marsh Posté le 07-02-2007 à 15:34:43    

Hello all.

 

Je suis entrain d'essayer de faire un programme pour faire un truc de logique

 

mathématique en utilisant l'Algorithme de réfutation pour trouver si une déduction est

 

vraie ou fausse.  J'ai compris l'algorithme mais pour l'implémentation en langage C je

 

galère a mort.

 

les connecteur logique utiliser sont: et (& ), ou (|), non (i), -> (l'implication).

 

**** J'explique L'algorithme:
Cet algorithme suit les étapes suivantes:

 

(1)
J'ai une déduction, en cas générale c'est  
P1, P2, P3, ..., Pn  DEDUIT P
par exemple, si j'ai P1 P2 et P3 comme ceci:
P1:   B -> !A
P2:   !B -> (C et A)
P3:   !A ou !C
P:     !A
Note: sachant que l'expression (I -> J) veut dite !(I et !J)
alors ma déduction est :
(B -> !A), !B -> (C et A), !A ou !C   DEDUIT   !A
(L%u2019algorithme de réfutation va vérifier si cette déduction est vraie ou pas)

 

(2)
On transforme notre déduction en un ensemble sigma comme suite:
sigma = { P1, P2, P3, !P }       (par exemple)
en cas générale c'est:   sigma = { P1, P2, P3, ....., !P }

 

(3)
On applique un ensemble de règles sur l'ensemble sigma,
ces règles sont appeler des Closes, et sont les suivant:
1- si j'ai dans une certaine formule Pi l'expression {!!A}, alors ça deviens  {A}
2- si j'ai {A & B} j'obtiens  {A, B}
3- si j'ai {!(A et B)} j'obtiens deux chose: {!A} et également {!B}
4- si j'ai {A -> B} j'obtiens  {!A} {B}

 

Exemple:
Si j'ai un ensemble comme ça:
sigma = { !!A, C&A, (B -> !A), !(A&B) }   on appliquant les close une par une ça devien:

 

( on appliquant la 1ere close: )
sigma = { A, C&A, (B -> !A), !(A&B) }

 

( on appliquant la 2ere close: )
sigma = { A, C, A, (B -> !A), !(A&B) }

 

( on appliquant la 4ere close: )    on aura 2 ensemble:
sigma1 = { A, C, A, !B, !(A&B) }
sigma2 = { A, C, A, !A, !(A&B) }

 

( on a appliquant la 3ere close sur sigma1 : ) on auras 2 autre ensemble:
sigma3 = { A, C, A, !B, !A }
sigma4 = { A, C, A, !B, !B }

 

( on a appliquant la 3ere close sur sigma2 : ) on auras 2 autre ensemble:
sigma5 = { A, C, A, !A, !A }
sigma6 = { A, C, A, !A, !B }

 

On ne pas allez plus loin (simplifier) dans ces ensembles donc on s'arrête ici, et on appelle

 

ces ensemble des ensemble littéraux.

 

Remarquant qu'a partir de sigma j'ai eu 4 ensemble littéraux: sigma3, sigma4, sigma5,

 

sigma6
Voici un schémas:
                  sigma
                     /\
                   /    \
                 /        \
           sigma1     sigma2
          /\                     /\
        /    \                 /    \
      /        \             /        \
sigma3 sigma4   sigma5  sigma6

 

Les ensembles sigma3 sigma4   sigma5  sigma6 sont appelés des ensembles de littéraux,
-Si tout les ensemble de littéraux sont inconsistant (cf plus bas) alors ma déduction du

 

début est VRAIE
-Si tout les ensemble de littéraux sont satisfiable, alors ma déduction du début est

 

FAUSSE.

 

En dit qu'un ensemble est inconsistant SI cet ensemble contiens des élément qui ce

 

contredit, par exemple dans notre exemple précédant: l'ensemble sigma5 contiens

 

l'élément A et l'élément !A alors il est inconsistant, sigma6 et sigma3 aussi.
SINON il est satisfiable, par exemple comme sigma4.

 

off... :)

 


**** Implémentation en C:

 

Ah là je galère, je ne sais pas comment implémenter les tout ces ensemble dans un

 

exemple concret de programme !
J'ai donc utilisé des tableaux de chaîne de caractère tout simplement, mais formules sont

 

en fait des chaînes de caractère.
Bon je met ce que j'ai déjà réussi a faire, mais ce n'ai rien:

 
Code :
  1. #include <stdio.h>
  2. #include <string.h>
  3. #include <stdlib.h>
  5. /*Je supose que le nbr de formules dans notre deduction est 3 formules*/
  6. #define N 4
  8. void read_string(char*, int);
  9. void Deduction(char P[][]);
  10. void ApliquerLesCloses(char *sigma[]);
  12. /*************************************************/
  14. /*  Representation de connecteur logique:
  15.       -    represente    ->
  16.       =    represente    <->
  17.       &    represente    et
  18.       |    represente    ou
  19.       !    represente    non
  20. */
  22. int main(void)
  23. {
  24.     /* on a N formules de longeur 20 maximum */
  25.     char P[N][20] = {"B-!A", "!B-C&A", "!A|!C", "!A"};
  26.     char *sigma[N];
  27.     int i;
  29.     //Deduction(P);
  31.     /* construire l'ensemble sigma = {P1, P2, P3, !P} a partire
  32.        des formulent */
  33.     for(i=0; i<N; i++)
  34.         sigma[i] = P[i];
  36.     ApliquerLesCloses(sigma);
  38.     return EXIT_SUCCESS;
  39. }
  41. /***********************************************/
  43. /* fonction securiser qui permet de saisir un chaine de caractere */
  44. void read_string(char *buffer, int size_of_buffer)
  45. {
  46.     /*on saisi notre chaine avec un simple fgets sur stdin*/
  47.     fgets(buffer, size_of_buffer, stdin);
  49.     /*on essaye de trouver le caractere '\n'*/
  50.     char *p = NULL;
  51.     p = strchr(buffer,'\n');
  53.     /*si on trouve le '\n', On le remplace par le caractere null (0 ou '\0')*/
  54.     if (p != NULL)
  55.         *p = 0;
  57.     /* sinon (s'il reste des caractere dans le tompon) on va jusqu'a
  58.        la fin de stdin */
  59.     else
  60.     {
  61.         int c;
  62.         while ((c = fgetc(stdin)) != '\n' && c != EOF);
  63.     }
  65. }
  67. /*************************************************/
  68. /* Cette fonction permet de saisir les formules de la deduction */
  69. void Deduction(char P[N][20])
  70. {
  71.     int i;
  73.     printf("La deduction est de la forme:   P0, P1, P2 deduit P\n"
  74.            "Donnez les formules P0 P1 P2 et P\n\n" );
  76.     for(i=0; i<N; i++)
  77.     {
  78.         printf("P%d: ",i);
  79.         read_string(P[i], sizeof(P[i]));
  80.     }
  82.     printf("Donc voici la deduction a demantrer:\n" );
  84.     for(i=0; i<N; i++)
  85.     {
  86.         if(i != N-1)
  87.             printf("(%s), ", P[i]);
  88.         else
  89.             printf("(%s)",P[i]);
  90.     }
  92. }
  94. /***************************************************/
  95. /* Apliquer les closes sur les formules de l'ensemple sigma */
  96. void ApliquerLesCloses(char* sigma[])
  97. {
  98.     int ip, i, j, len;
  99.     char *chaine;
  101.     /* on prend chaque chaine */
  102.     for(ip=0; ip<N; ip++)
  103.     {
  104.         chaine = sigma[ip];
  105.         len = strlen(chaine);
  107.         /* parcourire toute cette chaine */
  108.         for(i=0; i<len-1; i++)
  109.         {
  111.             /* s'il y a 2 non (!!) qui ce suivent, on les elimine (C'est la 1ere Close :p)*/
  112.             if( chaine[i] == '!' && chaine[i+1] == '!' )
  113.                 /*on deplace le reste de la chaine de 2élement vers l'ariere*/
  114.                 for(j=i+2; j<=len+1; j++)
  115.                     chaine[j-2] = chaine[j];
  117.             /*s'il y a (A&B) ça devien A, B*/
  118.             /* .... alors là pour le reste, je galére a mort .... */
  119.             /*Surtout pour la création d'un autre ensemble , etc...*/
  120.         }
  121.     }
  122. }
 

I know that the topic is too long but thank you for your help.

 



Message édité par bad___day le 22-02-2007 à 11:30:21
Reply

Marsh Posté le 07-02-2007 à 15:34:43   

Reply

Marsh Posté le 10-02-2007 à 15:21:12    

up

Reply

Marsh Posté le 10-02-2007 à 15:55:42    

faut voir avec les cracks de la programmation fonctionnelle
 
nraynal ?

Reply

Marsh Posté le 10-02-2007 à 22:42:32    

Plutôt que de donner tout de suite du code C, il pourrait être intéressant de nous expliquer déjà ton principe de lecture/analyse des clauses et comment tu penses les représenter en mémoire.
Il faudrait peut-être écrire une sorte de grammaire des clauses, formaliser les règles de déduction en termes de réécriture, fouille du côté de l'implémentation des Prolog.

Reply

Marsh Posté le 11-02-2007 à 02:34:45    

Le langage C est une obligation pour toi dans ce cas?

Message cité 1 fois

---------------
Les bureaucrates: "S'ils tombaient d'un immeuble, il leur faudrait une semaine pour s'ecraser." "All I ever wanted All I ever needed Is here in my arms Words are very unnecessary They can only do harm               Enjoy the silence"
Reply

Marsh Posté le 11-02-2007 à 10:22:43    

le langage C n'est effectivement pas la panacée pour faire ce genre de choses, mais sinon si c'est obligatoire il va falloir déja voir à représenter tes expressions d'une manière traitable, par exemple en utilisant un truc du genre (je sens que ce bout de code va provoquer les fureurs de certains :whistle:) :

 
Code :
  1. enum expression_type {
  2.   EXPRESSION_VARIABLE,
  3.   EXPRESSION_UNARY_OPERATOR,
  4.   EXPRESSION_BINARY_OPERATOR
  5. };
  6.  
  7. enum unary_operator {
  8.   UNARY_OPERATOR_NOT
  9. };
  10.  
  11. enum binary_operator {
  12.   BINARY_OPERATOR_AND,
  13.   BINARY_OPERATOR_OR,
  14.   BINARY_OPERATOR_IMPLY
  15. };
  16.  
  17. struct expression {
  18.   enum expression_type type;
  19.   union {
  20.     char variable;
  21.     struct {
  22.       enum unary_operator name;
  23.       struct expression* rhs;
  24.     } unary_operator;
  25.     struct {
  26.       enum binary_operator name;
  27.       struct expression* rhs;
  28.       struct expression* lhs;
  29.     } binary_operator;
  30.   } value;
  31. };
  32.  
  33. struct expression_set {
  34.   struct expression head;
  35.   struct expression_set* tail;
  36. };
 

Tu fais quelques fonctions pour créer des struct expression pour commencer, histoire de pas te palucher des mallocs à travers tout ton code,
des trucs du genre :

Code :
  1. struct expression* a = expression_new_variable("a" );
  2. struct expression* b = expression_new_variable("b" );
  3. struct expression* not_a = expression_new_unary_operator(UNARY_OPERATOR_NOT, a);
  4. struct expression* b_and_not_a = expression_new_binary_operator(BINARY_OPERATOR_AND, b, not_a);
 

Tu définis sur la struct expression_set (un expression_set c'est un ensemble d'expression, cad un sigma) les opérations habituelles de liste chainée (add, prev, next) et une fonction duplicate (tu va en avoir besoin pour crée tes plusieurs sigma quand ça "bifurque"...) et ensuite il te faudra aussi une liste chainée d'expression_set pour stocker tout tes sigma et les parcourir (enfin tu peut utiliser ce que tu veut comme conteneur, et si t'es flemmard ou que t'en a une de déja faite, tu utilise une liste chainée générique à base de void*... )

 

ensuite tu fais des fonction genre expression_set_is_consistant() pour faire tes test à la fin et une fonction expression_set_is_simple() pour savoir si une expression est "minimale" au sens de la forme A ou !A.

 

il te faut des fonctions de transformation d'arbre (les struct expression forment un arbre ...) qui utilisent tes 4 règles de transformation pour remplacer un expression_set par d'autres expression_set "simplifiés", çe sera le coeur de ton algo et pas forcément le plus facile... tant que expression_set_is_simple() renvoie vrai, tu ré-applique (en gros hein). quand toutes les expression_set sont simples, tu regarde si toutes tes expression_set sont consistantes avec la fonction idoine, selon le résultat tu as ta réponse, TADAM \o/

 

Bon le bonus c'est par contre qu'on début il te faudra peut-être transformer une expressions sous la forme humaine en chaîne de caractère en une structure d'arbre, fait ton flemmard, utilise le bulldozer, flex/bison :D (facile si tu maitrise les regexp cela dit)

 


Message édité par 0x90 le 11-02-2007 à 10:23:24

---------------
Me: Django Localization, Yogo Puzzle, Chrome Grapher, C++ Signals, Brainf*ck.
Reply

Marsh Posté le 11-02-2007 à 11:03:24    

L'interet d'ecrire ce genre de truc en C m'echappe...
Et effectivement, au vu du code que bad_day a donne, ca m'a l'air bien mal parti.


Message édité par el muchacho le 11-02-2007 à 11:05:00
Reply

Marsh Posté le 11-02-2007 à 11:34:06    

Tu connais COQ ?
 
sinon, en ML ca se fait genre 10x plus mieux vite [:pingouino]

Reply

Marsh Posté le 11-02-2007 à 12:44:01    

thermocline a écrit :

Le langage C est une obligation pour toi dans ce cas?


Non pas vraiment  :D  , mais c'est que c'est le langage que je maîtrise le mieux.
 

Citation :

sinon, en ML ca se fait genre 10x plus mieux vite


Oué, je croie que Caml (ou Ocaml) est plus adapter pour ce genre de programme. d'ailleurs y a un ami qui a essayer de m'aider en le faisant en oCaml: http://bluestorm.info/tmp/logic2.ml.html , mais ça ne marche pas tout a fait il a codé ça vite fait pour avoir une idée et il faudrait le modifier ptet un peu pour que ça donne le bon résultat... et ce n'ai pas envidant pour moi de bien comprendre ce qu'il a fait ( puisque je ne maîtrise que le C  :sweat: )
Alors si tu tu fait du caml Joel F, tu pourrai m'aider a continuer ce code ?
 
Sinon j'ai fait un peut de code mal parti Juste pour tester.., pour la création d'ensemble etc..:
 

Code :
  1. #include <stdio.h>
  2. #include <string.h>
  3. #include <stdlib.h>
  5. /*  Representation de connecteurs logique:
  7.       -              represente    ->         exemple     A-B
  8.       =              represente    <->        exemple     A=B
  9.       . ou (rien)    represente    et         exemple     AB
  10.       +              represente    ou         exemple     A+B
  11.       !              represente    non        exemple     !A
  12. */
  15. typedef struct sigma SIGMA;
  16. /* structure: */
  17. struct sigma
  18. {
  19.     int id; /* id de l'ensemble courant */
  20.     char* properties; /* propriétées de l'ensemble */
  22.     SIGMA *father;
  23.     SIGMA *son_1;
  24.     SIGMA *son_2;
  25. };
  27. /* Les prototypes: */
  28. SIGMA* CreerEnsemble(int, char*, SIGMA* , SIGMA*, SIGMA*);
  29. void SupprimerEnsemble(SIGMA*);
  30. int SeparerProprietes(char*, char[][]);
  31. void Close1(char*);
  32. int Litteral(SIGMA*); //===> teste si l'ensemble est litereale ou pas.
  34. /**********************************************************************/
  36. int main(void)
  37. {
  38.     SIGMA *sgm, *sgm1, *sgm2;// *sgm3, *sgm4, *sgm5, *sgm6;
  40.     sgm = CreerEnsemble(0, "(A.!!C)+B,(A.!!C)+!B,(A+C).B", NULL, sgm1, sgm2);
  42.     Close1(sgm->properties);
  43.     //int litteral = Litteral(sgm);
  45.     SupprimerEnsemble(sgm);
  47.     return EXIT_SUCCESS;
  48. }
  50. /**********************************************************************/
  52. SIGMA* CreerEnsemble(int i, char* P, SIGMA* pere, SIGMA* fils1, SIGMA* fils2)
  53. {
  54.     SIGMA* ensemble = malloc(sizeof *ensemble);
  56.     if ( ensemble == NULL ) //l'allocation a echoué
  57.         return NULL;
  59.     ensemble->id = i;
  60.     ensemble->properties = P;
  61.     ensemble->father = pere;
  62.     ensemble->son_1 = fils1;
  63.     ensemble->son_2 = fils2;
  65.     return ensemble;
  66. }
  68. /**********************************************************************/
  70. void SupprimerEnsemble(SIGMA* ensemble)
  71. {
  72.     /* si un champ a été alloué dynamiquement, le libérer */
  73.     free(ensemble), ensemble = NULL;
  74. }
  76. /**********************************************************************/
  78. void Close1(char *P)
  79. {
  80.     char propr[20][10];  // chaque ligne pointe vers une proprietee
  81.     int len, i, j, h, nbrProprietes;
  83.     nbrProprietes = SeparerProprietes(P, propr);
  85.     printf("\n\nTeste de la Close1:\n" );
  87.     /* on prend chaque chaine (propriete) */
  88.     for(i=0; i<nbrProprietes; i++)
  89.     {
  90.         len = strlen(propr[i]);
  91.         /* parcourire toute cette chaine */
  92.         for(j=0; j<=len-3; j++)
  93.         {
  94.             /* s'il y a 2 non (!!) qui ce suivent, on les elimine */
  95.             if( propr[i][j] == '!' && propr[i][j+1] == '!' )
  96.                 /*on deplace le reste de la chaine de 2élement vers l'ariere*/
  97.                 for(h=j+2; h<=len; h++)
  98.                     propr[i][h-2] = propr[i][h];
  99.         }
  101.         printf("%s\n", propr[i]);
  102.     }
  104. }
  106. /**********************************************************************/
  108. /* Cette fonction va separer chaque proprieté de l'ensemble de proprietés
  109.    et metre ces proprietes dans une matrice */
  110. int SeparerProprietes(char *P, char chaine[][10])
  111. {
  112.     int ip, i=0, j=0, lenP =strlen(P);
  114.     for(ip=0; ip <= lenP; ip++)
  115.         if(P[ip] != ',')
  116.         {
  117.             chaine[i][j] = P[ip];
  118.         j++;
  119.         }
  120.         else
  121.         {
  122.             chaine[i][j] = '\0';
  123.             i++; // on passe a la ligne suivante.
  124.             j = 0;  // on ce place à la 1ere colone de la ligne.
  125.         }
  127.     printf("Les proprietées sont:\n" );
  128.     for(ip=0; ip <= i; ip++)
  129.         printf("%d>   %s\n", ip+1, chaine[ip]);
  131.     return (i+1);  // Le nombre de proprietes
  132. }
  136. int Litteral(SIGMA* ensemble)
  137. {
  138.     char* P = ensemble->properties;
  139.     int i, lenP = strlen(P);
  140.     for(i=0; i<lenP; i++)
  141.         if(P[i] == '+' || P[i] == '.' || P[i] == '-')
  142.             return 0;
  144.     return 1;
  145. }


 
 
ça sera sympa si vous pourriez m'aider.
 
 :)


Message édité par bad___day le 12-02-2007 à 15:30:17
Reply

Marsh Posté le 11-02-2007 à 21:11:36    

Si tu n'est pas obligé d'utiliser le C, alors j'ai vu un prouveur en Prolog qui fait ça en 40 lignes de code.

Reply

Marsh Posté le 11-02-2007 à 21:11:36   

Reply

Marsh Posté le 11-02-2007 à 21:12:39    

Prolog, COQ, ISAR ...

Reply

Marsh Posté le 11-02-2007 à 21:22:53    

Je ne peux que te conseiller de regarder du côté de Prolog, en tant que programmeur, ça ouvre l'esprit.

Message cité 1 fois
Reply

Marsh Posté le 12-02-2007 à 15:35:17    

Trap D a écrit :

Je ne peux que te conseiller de regarder du côté de Prolog, en tant que programmeur, ça ouvre l'esprit.


Mais je ne connais pas ce langage  :( , et je croi pas que j'aurais le temps d'aprendre un langage juste pour realiser cet exercice.
Donc je croie que je préférerai le faire en C.
P.S. J'ai un peut édité le code du dernier topic...
 
 

Reply

Marsh Posté le 15-02-2007 à 20:24:13    

Si tu es tjrs sur cet exercice, tu fais comme tu veux, mais on ne pourra pas t'aider, l'algo est trop complexe pour être codé en C simplement, ça prendrait plus de temps que la plupart d'entre nous sont prêts à y consacrer. Tu ferais mieux d'apprendre ocaml et de reprendre le code de ton copain (qui a l'air de bien torcher, au passage) et de te faire aider par lui.

Message cité 1 fois
Message édité par el muchacho le 15-02-2007 à 20:26:42
Reply

Marsh Posté le 15-02-2007 à 22:09:10    

el muchacho a écrit :

Si tu es tjrs sur cet exercice, tu fais comme tu veux, mais on ne pourra pas t'aider, l'algo est trop complexe pour être codé en C simplement, ça prendrait plus de temps que la plupart d'entre nous sont prêts à y consacrer. Tu ferais mieux d'apprendre ocaml et de reprendre le code de ton copain (qui a l'air de bien torcher, au passage) et de te faire aider par lui.

 

Euh, j'ai dja donné une bonne partie quand même...

Message cité 1 fois
Message édité par 0x90 le 15-02-2007 à 22:17:59

---------------
Me: Django Localization, Yogo Puzzle, Chrome Grapher, C++ Signals, Brainf*ck.
Reply

Marsh Posté le 22-02-2007 à 11:29:38    

0x90 a écrit :

Euh, j'ai dja donné une bonne partie quand même...


et je n'arrive pas à l'utiliser :(
 

Reply

Sujets relatifs:

Leave a Replay

Make sure you enter the(*)required information where indicate.HTML code is not allowed