diff --git a/app/Main.hs b/app/Main.hs index 4ecf82e..605f255 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -1,8 +1,8 @@ module Main where import FOLSyntax ( Formula(Conj, Neg, Impl), Term(..) ) -import Parser ( parseFormula ) -import Resolution ( CNF, doResolution ) +import Parser ( parseFormula, parseFormulaE ) +import Resolution ( CNF, doResolution, doResolutionIO, showCNF ) import Normalforms ( makeNNF, renameBinders, @@ -10,6 +10,7 @@ import Normalforms makeSkolem, makeCNF, makeClauseSet ) +import Control.Monad (void) {- To prove a formula we: @@ -20,6 +21,11 @@ To prove a formula we: proveFormula :: Formula -> Either () CNF proveFormula form = doResolution . makeClauseSet . makeCNF . makeSkolem . makePNF . renameBinders . makeNNF $ Neg form +proveFormulaIO :: Formula -> IO () +proveFormulaIO form = do + let clauseSet = makeClauseSet . makeCNF . makeSkolem . makePNF . renameBinders . makeNNF $ Neg form + void $ doResolutionIO clauseSet + -- unification examples terma1 :: Term terma1 = Fun "f" [Var "x", Fun "g" [Var "y"]] @@ -67,8 +73,8 @@ formula6 = Impl (Conj psi1 psi2) psi3 psi2 = parseFormula "forall x. P(x) -> forall y. Q(y) -> !L(x, y)" psi3 = parseFormula "forall x. D(x) -> !Q(x)" -main :: IO () -main = do +testing :: IO () +testing = do putStrLn $ "Now making NNF of formula: " ++ show formula1 print $ makeNNF formula1 putStrLn $ "Now making PNF of formula: " ++ show formula2 @@ -90,4 +96,56 @@ main = do putStrLn $ "Now Proving formula by resolution: " ++ show formula6 case proveFormula (Neg formula6) of Left _ -> putStrLn "Success!" - Right _ -> return () \ No newline at end of file + Right _ -> return () + +main :: IO () +main = do + showIntroText + go + where + go = do + putStrLn "\nYou can now enter a formula that should be proven or enter the name of a predefined formula to proof them." + putStrLn "Type 'help' to see the information again." + -- TODO use haskeline... + line <- getLine + case line of + "script" -> fullProof formula3 + "doctors" -> fullProof formula6 + "drugs" -> fullProof formula5 + "help" -> showIntroText + str -> case parseFormulaE str of + Left err -> putStrLn err + Right formula -> fullProof formula + go + fullProof f = do + putStr "\n\n\n" + putStrLn $ "1. Negation of formula:\n" ++ show (Neg f) + let f' = makeNNF (Neg f) + putStrLn $ "2. Negation normalform:\n" ++ show f' + let f'' = makePNF $ renameBinders f' + putStrLn $ "3. Prenex normalform (with renamed binders):\n" ++ show f'' + let f''' = makeSkolem f'' + putStrLn $ "4. Skolemization:\n" ++ show f''' + let g = makeClauseSet . makeCNF $ f''' + putStrLn $ "5. Clause set:\n" ++ showCNF g + putStrLn "6. Do resolution:\n" + _ <- doResolutionIO g + putStrLn "7. Negation of formula is unsatisfiable, so the formula is valid!" + showIntroText = do + putStrLn "This is a simple program implementing a resolution algorithm on first order logic (FOL)." + putStrLn "Caution: resoluton on FOL is only a semi-decider, if you try to prove an unprovable formula the algorithm will diverge!" + putStrLn "\nProcedure:" + putStrLn "To proof a formula the program takes the following steps:" + putStrLn "1. Negate the formula" + putStrLn "2. Transform it to negation normalform" + putStrLn "3. Transform it to prenex normalform" + putStrLn "4. Skolemize formula" + putStrLn "5. Transform it to a clause set" + putStrLn "6. Exhaustively use the reduction rule, until the empty clause is found." + putStrLn "7. If an empty clause was found the negation of the formula is unsatisfiable, making the the formula valid!" + putStrLn "\nPrelude:" + putStrLn "There are some predefined formulas that can be called for a proof:" + putStrLn $ "script = " ++ show formula3 ++ " [a small resolution example taken from lecture notes]" + -- putStrLn $ "exercises = " ++ show formula4 ++ " [another small resolution example taken from exercises]" TODO this is already negated... + putStrLn $ "doctors = " ++ show formula6 ++ " [a little more complex example from exercises]" + putStrLn $ "drugs = " ++ show formula5 ++ " [most complex example from exercises]" diff --git a/app/Normalforms.hs b/app/Normalforms.hs index 87db682..a57761d 100644 --- a/app/Normalforms.hs +++ b/app/Normalforms.hs @@ -3,7 +3,7 @@ module Normalforms where import FOLSyntax ( Formula(..), Term(..), formulaVars, termSubst, findFresh ) import qualified Data.Set as Set -import Resolution ( CNF, renameFormula ) +import Resolution ( CNF, renameFormula, Clause (..) ) import Data.List ( find ) import Data.Maybe ( fromJust ) @@ -137,8 +137,8 @@ makeCNF form = let form' = cnfStep form in -- create the list of clauses from a formula makeClauseSet :: Formula -> CNF makeClauseSet (Conj f1 f2) = makeClauseSet f1 `Set.union` makeClauseSet f2 -makeClauseSet (Disj f1 f2) = Set.singleton $ collectDisjs f1 `Set.union` collectDisjs 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 $ Set.singleton f +makeClauseSet f = Set.singleton . Clause $ Set.singleton f diff --git a/app/Parser.hs b/app/Parser.hs index 15503d2..6c9a843 100644 --- a/app/Parser.hs +++ b/app/Parser.hs @@ -1,4 +1,4 @@ -module Parser (parseFormula) where +module Parser (parseFormula, parseFormulaE) where import Lexer ( comma, @@ -14,6 +14,7 @@ import Text.Parsec.String (Parser) import Data.Functor ( ($>) ) import Prelude hiding (pred, all) +import Data.Either.Extra (mapLeft) term :: Parser Term @@ -87,5 +88,8 @@ fromRight :: Either a b -> b fromRight (Left _) = error "fromRight called on left value!" fromRight (Right b) = b +parseFormulaE :: String -> Either String Formula +parseFormulaE str = mapLeft show (parse (contents formula) "stdin" str) + parseFormula :: String -> Formula parseFormula = fromRight . parse (contents formula) "stdin" \ No newline at end of file diff --git a/app/Resolution.hs b/app/Resolution.hs index f221a90..5e51e09 100644 --- a/app/Resolution.hs +++ b/app/Resolution.hs @@ -1,4 +1,5 @@ {-# LANGUAGE TupleSections #-} +{-# LANGUAGE InstanceSigs #-} module Resolution where import Data.Set (Set) import qualified Data.Set as Set @@ -10,31 +11,37 @@ import FOLSyntax termSubst, findFresh ) import Data.Maybe ( mapMaybe ) -import Data.List +import Data.List ( intercalate, intersect, permutations ) import Control.Monad (zipWithM) type CNF = Set Clause -type Clause = Set Literal +newtype Clause = Clause (Set Literal) type Literal = Formula type Unifier = [(Term, Term)] +instance Show Clause where + show :: Clause -> String + show = showClause +instance Eq Clause where + (==) :: Clause -> Clause -> Bool + (==) = alphaEq +instance Ord Clause where + (<=) :: Clause -> Clause -> Bool + (Clause c1) <= (Clause c2) = Clause c1 == Clause c2 || c1 <= c2 + +showCNF :: CNF -> String +showCNF set = "[" ++ intercalate ", " (map show $ Set.toList set) ++ "]" -- 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 +-- 4. check if any clause pair was unifiable, with a unificator that maps variables only to variables alphaEq :: Clause -> Clause -> Bool -alphaEq c1 c2 = any (uncurry unifyLiteralList) permutationPairs +alphaEq (Clause c1) (Clause c2) = Set.size c1 == Set.size 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 Unifier unify [] = Just [] @@ -58,11 +65,14 @@ unify ((t, s) : rest) = do unifyLiteralList :: [Literal] -> [Literal] -> Bool unifyLiteralList ls1 ls2 = case zipWithM unifyLiterals ls1 ls2 of Nothing -> False - Just mgus -> all checkSimpleMgu mgus + Just mgus -> all checkSimpleMgu mgus && checkValidMgu (concat mgus) where + checkValidMgu mgu = case unify mgu of + Nothing -> False + _ -> True checkSimpleMgu :: Unifier -> Bool checkSimpleMgu [] = True - checkSimpleMgu ((Var _, Var _) : _) = True + checkSimpleMgu ((Var _, Var _) : rest) = checkSimpleMgu rest checkSimpleMgu _ = False unifyLiterals :: Literal -> Literal -> Maybe Unifier unifyLiterals (Neg f) (Neg g) = unifyLiterals f g @@ -100,7 +110,7 @@ makeVariablesDisjunct c1 c2 = (c1', c2') (_, c2') = makeClauseDisjunct used c2 -- takes a list of variable names and ensures that the clause does not contain these variables (by renaming), then returns all variables used in the clause + used before makeClauseDisjunct :: [String] -> Clause -> ([String], Clause) -makeClauseDisjunct used clause = (concatMap formulaVars newClause ++ newUsed, newClause) +makeClauseDisjunct used (Clause clause) = (concatMap formulaVars newClause ++ newUsed, Clause newClause) where criticalVars = used `intersect` concatMap formulaVars clause (newUsed, newClause) = foldr foldFun (used, clause) criticalVars @@ -127,10 +137,10 @@ 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 = newClauses +resolveClauses (Clause c1) (Clause c2) = newClauses where -- first make variables in both clauses disjunct - (c1', c2') = makeVariablesDisjunct c1 c2 + (Clause c1', Clause c2') = makeVariablesDisjunct (Clause c1) (Clause c2) zippedLiterals = [(lit1, lit2) | lit1 <- Set.toList c1', lit2 <- Set.toList c2'] newClauses = Set.fromList $ mapMaybe (\(l1, l2) -> do -- first calculate mgu @@ -138,12 +148,16 @@ resolveClauses c1 c2 = newClauses -- 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'' `Set.union` c2'' + return . Clause $ c1'' `Set.union` c2'' ) zippedLiterals + +cnfMember :: Set Literal -> Set Clause -> Bool +cnfMember set cnf = Set.member set $ Set.map (\(Clause c) -> c) cnf + -- 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 +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] @@ -153,7 +167,7 @@ resolveStep clauses = if Set.empty `Set.member` clauses then Left () else Right 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 + inRight clause clauses' = clause `cnfMember` Set.map snd clauses' -- 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 @@ -179,11 +193,12 @@ doResolutionIO cnf = do let setE = resolveStepVerbose set case setE of Left _ -> do - putStrLn "Resolved to empty clause, so formula is proven!" + putStrLn "Resolved to empty clause!" return $ Left () Right set' -> do putStrLn $ "Resolution iteration " ++ show n ++ ":\n" printResolvents (Set.toList $ set' `Set.difference` set) + putStrLn $ "Clauses after iteration:\n" ++ concatMap (\c -> showClause c ++ "\n") (Set.map snd set') putStrLn "" resolutionHelper set' (n + 1) @@ -194,4 +209,4 @@ printResolvents (([c1, c2], c) : rest) = do printResolvents _ = return () showClause :: Clause -> String -showClause c = "[" ++ intercalate ", " (map show (Set.toList c)) ++ "]" \ No newline at end of file +showClause (Clause c) = "[" ++ intercalate ", " (map show (Set.toList c)) ++ "]" \ No newline at end of file