Valid XHTML     Valid CSS2    

Solveur 1

gilles.hunault "at" univ-angers.fr                    


     
          -e : exhaustive, toutes les solutions (désactivée par défaut)
          -h : écrit "help" :p
          -p : cherche des formule que avec des littéraux positifs (pas de not)
               (désactivée par défaut)
          -s n : recherche toute les formule de 1 à n par (5 par défaut)
          -t : effectue seulement le test de subsommation (désactivée par défaut)
          -u : seulement des clauses unitaires (pas de "ou") (désactivée par défaut)
          -v : mode verbeux, c'est à dire qu'on affiche l'instance
               (désactivée par défaut)
          -x : sortie format XML que j'avais développé...(désactivée par défaut)
     
     Donc la recherche peut se faire dans 4 espaces :
     
     les CNF (par défaut) ex (a|~b)&(~c)
     les CNF-U (-u) ex (a)&(~b)&(~c)
     les CNF-+ (-p) ex (a|b)&(c)
     et les CNF-U+ (-p -u) ex (a)&(b)&(c)

 

 

retour gH    Retour à la page principale de   (gH)