Définir un type proposition avec Vrai, Faux, conjonction, disjonction, négation, implication, équivalence et variable.
Définir un type environnement associant à des variables des valeurs true ou false. Définir dans la même foulée une fonction retrouvant à partir d'une variable et d'un environnement sa valeur associée.
Écrire la fonction evaluer prenant une proposition et un environnement et calculant la valeur de vérité de la proposition vis-à-vis des valeurs conférées aux variables par l'environnement.
Définir une fonction extrayant les variables d'une proposition. Tâchez que votre solution ne consomme que l'exact nombre de :: nécessaires bref, qu'elle soit linéaire en le nombre de variables extraites. Attention aux variables qui apparaissent plusieurs fois, elles ne doivent être comptées qu'une unique fois.
Pour vérifier une formule ayant p, q, ... comme variables, il suffit de la vérifier pour toutes les combinaisons de valeurs que peuvent prendre p, q, .... Définissez donc une fonction prenant une proposition et vérifiant si elle est une tautologie. On pourra éprouver sa solution sur:
let p = Variable("p") and q = Variable("q") and r = Variable("r");; p : proposition = Variable "p" q : proposition = Variable "q" r : proposition = Variable "r" verifier_tautologie p;; - : bool = false verifier_tautologie (Or(p, Not(p)));; - : bool = true verifier_tautologie (Imply(p, p));; - : bool = true verifier_tautologie (Equivalent(p, Not(Not(p))));; - : bool = true (* Loi de Morgan *) verifier_tautologie (Imply (Not(And(p,q)), Or(Not(p),Not(q))));; - : bool = true (* Plus complexe *) verifier_tautologie (Imply (Imply(Imply(Variable("p"), Variable("q")),Variable("r")), Imply(Variable("p"), Imply(Variable("q"),Variable("r")))) );; - : bool = true verifier_tautologie (Imply (Imply(Variable("p"), Imply(Variable("q"),Variable("r"))), Imply(Imply(Variable("p"), Variable("q")),Variable("r")) ));; - : bool = false
L'implication et l'équivalence peuvent être considérées comme non primitives. Définir une fonction les convertissant en leur équivalent plus simple.
Lorsqu'une proposition n'est pas une tautologie, produire une réfutation c'est-à-dire l'environnement tel que la proposition soit fausse. Dans le cas d'une tautologie, la fonction retournera l'environnement vide. On utilisera avec fruit des exceptions.
refuter p;; - : liaison list = [\camlbslash{}{variable = Variable "p"; valeur = false\camlbslash{}}] refuter (simplifier (Imply (Imply(Variable("p"), Imply(Variable("q"),Variable("r"))), Imply(Imply(Variable("p"), Variable("q")),Variable("r")) )) );; - : liaison list = [\camlbslash{}{variable = Variable "r"; valeur = false\camlbslash{}}; \camlbslash{}{variable = Variable "q"; valeur = true\camlbslash{}}; \camlbslash{}{variable = Variable "p"; valeur = false\camlbslash{}}]