vérification propositionnelle Formule Un autre Implique (en Haskell)

Question

Supposons que nous ayons

data Exp = Prop String -- a proposition 
     | And Exp Exp -- a conjunction of propositions 
     | Or Exp Exp -- a disjunction of propositions 

Alors est-il un moyen de voir si l'on implique l'expression imbriquée un autre? C'est, je suis à la recherche de quelque chose comme ce qui suit:

implies :: Exp -> Exp -> Bool 
implies = {- returns true if and only if the first expression 
       implies the second expression     -} 

implies 
    (And (Prop "Apple") (Prop "Banana")) 
    (Or (Prop "Apple") (Prop "Banana")) 
-- => True, since "Apple and Banana" implies "Apple or Banana" 

implies 
    (Or (Prop "Apple") (Prop "Banana")) 
    (And (Prop "Apple") (Prop "Banana")) 
-- => False, since "Apple or Banana" does not imply "Apple and Banana" 

est-il un moyen de mettre en œuvre, ou est-il une bibliothèque qui implémente cela? Si cela fait une différence: j'ai seulement besoin de And et de Or (c'est-à-dire que je n'ai pas besoin d'implication matérielle).

Answer 1

Normalement vous utiliseriez un solveur SAT (comme indiqué dans l'autre réponse) mais pour votre exemple spécifique, vous pourriez également exploiter le fait que les formules propositionnelles sur un ensemble de littéraux U peuvent être représentées par des sous-ensembles U. Ces "sous-ensembles représentatifs" sont les modèles d'une formule.

Dans votre exemple, U = { Apple, Banana }. L'expression (Apple AND Banana) est représentée uniquement par un sous-ensemble unique de U, à savoir par { Apple, Banana }. (Apple OR Banana) d'autre part a trois modèles: { Apple }, { Banana } et { Apple, Banana }.

Si une proposition p est dans models(f) alors p est vrai, sinon il est faux. Les modèles pour une formule f AND g sont les sous-ensembles de U qui sont des modèles de f et de g. Un modèle f OR g est un ensemble qui est un modèle de f ou un modèle de g.

Dans Haskell cela ressemble (si l'on ajoute import qualified Data.Set as S en haut):

-- The powerset of `U = {Apple, Banana}` 
u = [S.empty, S.singleton "Apple", S.singleton "Banana", S.fromList ["Apple", "Banana"]] 

isModelOf :: S.Set String -> Exp -> Bool 
isModelOf s = any ((==) s) . models 

models :: Exp -> [S.Set String] 
models e = case e of 
    Prop s -> filter (s `S.member`) u 
    And l r -> filter (flip isModelOf r) $ models l 
    Or l r -> models l ++ models r 

Enfin, une formule f implique une formule g si tous les modèles de f est aussi un modèle de g:

implies :: Exp -> Exp -> Bool 
implies f g = all isGModel fModels where 
    fModels = models f 
    gModels = models g 
    isGModel s = any ((==) s) gModels 

Veuillez noter que cette approche est très inefficace et n'échelle pas au-delà d'un petit nombre de littéraux (parce que les modèles sont calculés en énumérant des sous-ensembles de tous les littéraux). Mais il peut être éducatif de penser au problème en termes d'ensembles.

Answer 2

Ceci touche à l'un des problèmes clés en informatique. Pour une expression des AND et des OR des variables booléennes, pouvons-nous déterminer si l'expression est satisfiable? Ou l'expression est-elle toujours fausse?

Un algorithme simple consiste à construire une preuve par contradiction puis à appliquer itérativement resolution.

Par exemple, le premier problème est équivalent à prouver invalide APPLE && BANANA && NOT (APPLE || BANANA). Eh bien, cette expression est équivalente à APPLE && BANANA && NOT APPLE && NOT BANANA et cette expression est invalide, donc nous pouvons conclure que l'implication est vraie.

De même le deuxième problème est équivalent à prouver invalide (APPLE || BANANA) && NOT (APPLE && BANANA). Cela se divise en quatre expressions: APPLE && NOT APPLE, APPLE && NOT BANANA, BANANA && NOT APPLE, BANANA & NOT BANANA. La première et la dernière sous-expressions peuvent être invalidées, mais les autres ne le peuvent pas. L'algorithme de résolution se rend compte qu'il est bloqué et donc l'implication ne tient pas.

Les algorithmes comme celui-ci qui aborde la question de savoir si les formules sont valides relèvent de SAT solvers. Le problème de satisfiability booléen est plus général que le problème que vous rencontrez, et les paquets pour l'attaquer (tels que incremental-sat-solver on Hackage et funsat on Hackage) emploient un algorithme plus sophistiqué qu'indiqué ici, mais vous devriez trouver possible de traduire votre expression à un problème de satisfiability . Généralement, il vous sera demandé de créer une expression qui n'est pas différente de votre type de données abstrait, en utilisant des variables et des AND et des OR. Les deux paquets cracheront un type de données de résultat indiquant que l'expression est insatisfiable ou qu'elle est satisfiable et voici ce que toutes les variables devraient être. Vos propositions peuvent être mises en œuvre en tant que variables dont vous connaissez déjà les valeurs de vérité.