From 876a9c9c6395eff7e3eeed991d326b69ac9fb321 Mon Sep 17 00:00:00 2001 From: reijix Date: Thu, 8 Jun 2023 11:30:41 +0200 Subject: [PATCH] Added some printing for resolution and implemented alphaEq on clauses --- app/Main.hs | 2 +- app/Resolution.hs | 104 +++++++++++++++++++++++++++++++++++++++------- 2 files changed, 90 insertions(+), 16 deletions(-) diff --git a/app/Main.hs b/app/Main.hs index f9258fb..4ecf82e 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -88,6 +88,6 @@ main = do Left _ -> putStrLn "Success!" Right _ -> return () putStrLn $ "Now Proving formula by resolution: " ++ show formula6 - case proveFormula formula6 of + case proveFormula (Neg formula6) of Left _ -> putStrLn "Success!" Right _ -> return () \ No newline at end of file diff --git a/app/Resolution.hs b/app/Resolution.hs index 9389581..f221a90 100644 --- a/app/Resolution.hs +++ b/app/Resolution.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE TupleSections #-} module Resolution where import Data.Set (Set) import qualified Data.Set as Set @@ -8,16 +9,34 @@ import FOLSyntax termFreeVars, termSubst, findFresh ) -import Data.List.Extra ( intersect ) import Data.Maybe ( mapMaybe ) +import Data.List +import Control.Monad (zipWithM) type CNF = Set Clause type Clause = Set Literal type Literal = Formula type Unifier = [(Term, Term)] + +-- alpha equality on clauses, a clause [S(x), P(y)] is equal to [S(y), P(x)] +-- 1. get all permutations of both clauses +-- 2. build the crossproduct of permutations of c1 and c2 +-- 3. unify each clause pair +-- 4. collect mgus where variables are only mapped to variables (meaning they are alpha eq) +-- 5. check if any such mgu exists +alphaEq :: Clause -> Clause -> Bool +alphaEq c1 c2 = any (uncurry unifyLiteralList) permutationPairs + where + permutationPairs = [(c1', c2') | c1' <- permutations $ Set.toList c1, c2' <- permutations $ Set.toList c2] + +set1 :: Clause +set1 = Set.fromList [Pred "S" [Var "x"], Pred "P" [Var "y"]] +set2 :: Clause +set2 = Set.fromList [Pred "P" [Var "z"], Pred "S" [Var "y"]] + -- unification algorithm of martelli montanari -unify :: [(Term, Term)] -> Maybe [(Term, Term)] +unify :: [(Term, Term)] -> Maybe Unifier unify [] = Just [] -- (delete) unify ((Var x, Var y) : rest) | x == y = unify rest @@ -36,6 +55,20 @@ unify ((t, s) : rest) = do rest' <- unify rest return $ (t, s) : rest' +unifyLiteralList :: [Literal] -> [Literal] -> Bool +unifyLiteralList ls1 ls2 = case zipWithM unifyLiterals ls1 ls2 of + Nothing -> False + Just mgus -> all checkSimpleMgu mgus + where + checkSimpleMgu :: Unifier -> Bool + checkSimpleMgu [] = True + checkSimpleMgu ((Var _, Var _) : _) = True + checkSimpleMgu _ = False + unifyLiterals :: Literal -> Literal -> Maybe Unifier + unifyLiterals (Neg f) (Neg g) = unifyLiterals f g + unifyLiterals (Pred p ts1) (Pred s ts2) | p == s && length ts1 == length ts2 = unify $ zip ts1 ts2 + unifyLiterals _ _ = Nothing + -- unifies predicates, e.g. P(x,y) == P(f(a), z) unifyPredicates :: Literal -> Literal -> Maybe Unifier unifyPredicates (Pred p1 ts1) (Neg (Pred p2 ts2)) | p1 == p2 && length p1 == length p2 = unify $ zip ts1 ts2 @@ -44,14 +77,6 @@ unifyPredicates _ _ = Nothing 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 `Set.member` clauses then Left () else Right $ clauses `Set.union` newClauses - where - -- rename all variables - zippedClauses = [(c1, c2) | c1 <- Set.toList clauses, c2 <- Set.toList clauses, c1 /= c2] - newClauses = setConcat $ map (uncurry resolveClauses) zippedClauses - -- applies an mgu to a given formula, asserts that the formula contains no quantifiers applyMgu :: Formula -> [(Term, Term)] -> Formula applyMgu (Pred p ts) mgu = Pred p $ map (`applyMguTerm` mgu) ts @@ -67,7 +92,7 @@ applyMguTerm (Var x) ((Var y, t) : rest) = if x == y then t else applyMguTerm (V applyMguTerm (Fun f ts) mgu = Fun f $ map (`applyMguTerm` mgu) ts applyMguTerm t _ = t --- takes two clauses and makes the variables these clauses disjunct +-- takes two clauses and makes the variables of these clauses disjunct makeVariablesDisjunct :: Clause -> Clause -> (Clause, Clause) makeVariablesDisjunct c1 c2 = (c1', c2') where @@ -102,22 +127,71 @@ renameFormula f' _ _ = 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 c1 c2 = Set.fromList newClauses +resolveClauses c1 c2 = newClauses where -- first make variables in both clauses disjunct (c1', c2') = makeVariablesDisjunct c1 c2 zippedLiterals = [(lit1, lit2) | lit1 <- Set.toList c1', lit2 <- Set.toList c2'] - newClauses = concat $ mapMaybe (\(l1, l2) -> do + newClauses = Set.fromList $ mapMaybe (\(l1, l2) -> do -- first calculate mgu mgu <- unifyPredicates l1 l2 -- now apply mgu to clauses without l1 and l2 let c1'' = Set.map (`applyMgu` mgu) (c1' `Set.difference` Set.singleton l1) let c2'' = Set.map (`applyMgu` mgu) (c2' `Set.difference` Set.singleton l2) - return [c1'', c2''] + return $ c1'' `Set.union` c2'' ) zippedLiterals +-- a single resolution step as described in gloin +resolveStep :: CNF -> Either () CNF +resolveStep clauses = if Set.empty `Set.member` 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 + +resolveStepVerbose :: Set ([Clause], Clause) -> Either (Set ([Clause], Clause)) (Set ([Clause], Clause)) +resolveStepVerbose clauses = if Set.empty `inRight` clauses then Left clauses else Right $ clauses `Set.union` newClauses + where + inRight clause set = clause `Set.member` Set.map snd set + -- cross product of clauses + zippedClauses = [(c1, c2) | c1 <- Set.toList (Set.map snd clauses), c2 <- Set.toList (Set.map snd clauses), c1 /= c2] + -- after resolveStep add every clause that can be gained through resolution to clauseSet + newClauses = setConcat' $ map (\(c1, c2) -> ([c1, c2], resolveClauses c1 c2)) zippedClauses + +setConcat' :: [([Clause], Set Clause)] -> Set ([Clause], Clause) +setConcat' [] = Set.empty +setConcat' ((cs, clauses) : rest) = Set.map (cs,) clauses `Set.union` setConcat' rest + -- do resolution until we have proven unfulfillability of formula set doResolution :: CNF -> Either () CNF doResolution f = do f' <- resolveStep f - doResolution f' \ No newline at end of file + doResolution f' + +doResolutionIO :: CNF -> IO (Either () (Set ([Clause], Clause))) +doResolutionIO cnf = do + let preparedCNF = Set.map ([], ) cnf + resolutionHelper preparedCNF 1 + where + resolutionHelper :: Set ([Clause], Clause) -> Int -> IO (Either () (Set ([Clause], Clause))) + resolutionHelper set n = do + let setE = resolveStepVerbose set + case setE of + Left _ -> do + putStrLn "Resolved to empty clause, so formula is proven!" + return $ Left () + Right set' -> do + putStrLn $ "Resolution iteration " ++ show n ++ ":\n" + printResolvents (Set.toList $ set' `Set.difference` set) + putStrLn "" + resolutionHelper set' (n + 1) + +printResolvents :: [([Clause], Clause)] -> IO () +printResolvents (([c1, c2], c) : rest) = do + putStrLn $ "Resolving " ++ showClause c1 ++ " and " ++ showClause c2 ++ "\n-> " ++ showClause c + printResolvents rest +printResolvents _ = return () + +showClause :: Clause -> String +showClause c = "[" ++ intercalate ", " (map show (Set.toList c)) ++ "]" \ No newline at end of file