diff --git a/app/Prop/Main.hs b/app/Prop/Main.hs new file mode 100644 index 0000000..0502bb5 --- /dev/null +++ b/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 \ No newline at end of file diff --git a/app/Prop/Normalforms.hs b/app/Prop/Normalforms.hs new file mode 100644 index 0000000..9380596 --- /dev/null +++ b/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 \ No newline at end of file diff --git a/app/Prop/Resolution.hs b/app/Prop/Resolution.hs new file mode 100644 index 0000000..a1698d7 --- /dev/null +++ b/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 \ No newline at end of file diff --git a/app/Prop/Syntax.hs b/app/Prop/Syntax.hs new file mode 100644 index 0000000..48ea4c8 --- /dev/null +++ b/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 diff --git a/resolution.cabal b/resolution.cabal index b00543e..1403e65 100644 --- a/resolution.cabal +++ b/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