Implemented resolution on propositional logic

app/Prop/Main.hs

@@ -0,0 +1,29 @@
+module Prop.Main where
+
+import Prop.Resolution ( makeClauseSet, doResolution )
+import Prop.Normalforms ( makeNNF, makeCNF )
+import Prop.Syntax ( Formula(Atom, Conj, Disj, Neg) )
+
+fullResolution :: Formula -> String
+fullResolution f = doResolution . makeClauseSet . makeCNF $ makeNNF f
+
+-- atoms
+a :: Formula
+a = Atom "A"
+b :: Formula
+b = Atom "B"
+c :: Formula
+c = Atom "C"
+d :: Formula
+d = Atom "D"
+
+formula1 :: Formula
+formula1 = Neg $ Conj (Disj a (Neg a)) (Neg c)
+
+formula2 :: Formula
+formula2 = Conj (Disj d $ Disj b $ Neg c) $ Conj (Disj d c) $ Conj (Disj (Neg d) b) $ Conj (Disj (Neg c) $ Disj b $ Neg a) $ Conj (Disj c $ Disj b $ Neg a) $ Conj (Disj (Neg b) (Neg a)) (Disj (Neg b) a)
+
+main :: IO ()
+main = do
+    putStrLn $ fullResolution formula1
+    putStrLn $ fullResolution formula2

app/Prop/Normalforms.hs

@@ -0,0 +1,29 @@
+module Prop.Normalforms where
+
+import Prop.Syntax
+
+-- negation normalform
+makeNNF :: Formula -> Formula
+makeNNF form = if form == f' then form else makeNNF f'
+    where
+        f' = nnfStep form
+        nnfStep (Conj f1 f2) = Conj (nnfStep f1) (nnfStep f2)
+        nnfStep (Disj f1 f2) = Disj (nnfStep f1) (nnfStep f2)
+        nnfStep (Impl f1 f2) = Disj (Neg f1) f2
+        nnfStep (Neg (Conj f1 f2)) = Disj (Neg f1) (Neg f2)
+        nnfStep (Neg (Disj f1 f2)) = Conj (Neg f1) (Neg f2)
+        nnfStep (Neg (Impl f1 f2)) = Conj f1 (Neg f2)
+        nnfStep (Neg (Neg f)) = f
+        nnfStep (Neg T) = F
+        nnfStep (Neg F) = T
+        nnfStep f = f
+
+-- conjunctive normalform
+makeCNF :: Formula -> Formula
+makeCNF form = let form' = cnfStep form in
+            if form == form' then form else makeCNF form'
+    where
+        cnfStep (Conj phi psi) = Conj (cnfStep phi) (cnfStep psi)
+        cnfStep (Disj (Conj phi psi) xi) = Conj (Disj phi xi) (Disj psi xi)
+        cnfStep (Disj xi (Conj phi psi)) = Conj (Disj xi phi) (Disj xi psi)
+        cnfStep f = f

app/Prop/Resolution.hs

@@ -0,0 +1,66 @@
+module Prop.Resolution where
+
+import Data.Set (Set)
+import qualified Data.Set as Set
+import Prop.Syntax ( Formula(..) )
+import Data.Maybe ( mapMaybe )
+import Debug.Trace
+import Data.List ( intercalate )
+
+
+type CNF = Set Clause
+newtype Clause = Clause (Set Literal) deriving (Eq, Ord)
+type Literal = Formula
+
+instance Show Clause where
+    show = showClause
+
+showClause :: Clause -> String
+showClause (Clause c) = "[" ++ intercalate ", " (map show (Set.toList c)) ++ "]"
+
+showCNF :: CNF -> String
+showCNF set = "[" ++ intercalate ", " (map show $ Set.toList set) ++ "]"
+
+-- create the list of clauses from a formula in CNF
+makeClauseSet :: Formula -> CNF
+makeClauseSet (Conj f1 f2) = makeClauseSet f1 `Set.union` makeClauseSet f2
+makeClauseSet (Disj f1 f2) = Set.singleton . Clause $ collectDisjs f1 `Set.union` collectDisjs f2
+    where
+        collectDisjs (Disj f1' f2') = collectDisjs f1' `Set.union` collectDisjs f2'
+        collectDisjs f' = Set.singleton f'
+makeClauseSet f = Set.singleton . Clause $ Set.singleton f
+
+-- takes two clauses and tries to unify every literal in a crossproduct, returns the set of all clauses resulting from this resolution step
+resolveClauses :: Clause -> Clause -> Set Clause
+resolveClauses (Clause c1) (Clause c2) = newClauses
+    where
+        -- zip the literals of both clauses
+        zippedLiterals = [(lit1, lit2) | lit1 <- Set.toList c1, lit2 <- Set.toList c2]
+        newClauses = Set.fromList $ mapMaybe (\(l1, l2) -> do
+                                            if Neg l1 == l2
+                                                then do
+                                                    let c1' = c1 `Set.difference` Set.singleton l1
+                                                    let c2' = c2 `Set.difference` Set.singleton l2
+                                                    return . Clause $ c1' `Set.union` c2'
+                                                else Nothing
+                            ) zippedLiterals
+
+cnfMember :: Set Literal -> Set Clause -> Bool
+cnfMember set cnf = Set.member set $ Set.map (\(Clause c) -> c) cnf
+setConcat :: Ord a => [Set a] -> Set a
+setConcat = foldr Set.union Set.empty
+
+-- a single resolution step as described in gloin
+resolveStep :: CNF -> Either () CNF
+resolveStep clauses = if Set.empty `cnfMember` clauses then Left () else Right $ clauses `Set.union` newClauses
+    where
+        -- cross product of clauses
+        zippedClauses = [(c1, c2) | c1 <- Set.toList clauses, c2 <- Set.toList clauses, c1 /= c2]
+        -- after resolveStep add every clause that can be gained through resolution to clauseSet
+        newClauses = setConcat $ map (uncurry resolveClauses) zippedClauses
+
+doResolution :: CNF -> String
+doResolution cnf | trace ("resolutionStep:\n" ++ showCNF cnf) True = case resolveStep cnf of
+    Left _ -> "no"
+    Right cnf' -> if cnf == cnf' then "yes" else doResolution cnf'
+doResolution _ = undefined

app/Prop/Syntax.hs

@@ -0,0 +1,21 @@
+module Prop.Syntax where
+
+data Formula
+    = Neg Formula
+    | Conj Formula Formula
+    | Disj Formula Formula
+    | Impl Formula Formula
+    | T
+    | F
+    | Atom String
+    deriving (Eq, Ord)
+
+
+instance Show Formula where
+    show (Neg f) = "!(" ++ show f ++ ")"
+    show (Conj f1 f2) = "(" ++ show f1 ++ " /\\ " ++ show f2 ++ ")"
+    show (Disj f1 f2) = "(" ++ show f1 ++ " \\/ " ++ show f2 ++ ")"
+    show (Impl f1 f2) = "(" ++ show f1 ++ " -> " ++ show f2 ++ ")"
+    show T = "true"
+    show F = "false"
+    show (Atom a) = a

resolution.cabal

@@ -71,7 +71,7 @@ executable resolution
     -- Directories containing source files.
     hs-source-dirs:   app
 
-    other-modules:    Lexer, Parser, FOLSyntax, Resolution, Normalforms
+    other-modules:    Lexer, Parser, FOLSyntax, Resolution, Normalforms, Prop.Syntax, Prop.Normalforms, Prop.Resolution, Prop.Main
 
     -- Base language which the package is written in.
     default-language: Haskell2010