diff --git a/app/FOLSyntax.hs b/app/FOLSyntax.hs new file mode 100644 index 0000000..111f69a --- /dev/null +++ b/app/FOLSyntax.hs @@ -0,0 +1,32 @@ +module FOLSyntax where + +data Term = Var String | Fun String [Term] deriving (Eq, Ord) +data Formula + = Pred String [Term] + | Neg Formula + | Conj Formula Formula + | Disj Formula Formula + | Impl Formula Formula + | All String Formula + | Exists String Formula + | T + | F + deriving (Eq, Ord) + + +instance Show Term where + show (Var x) = x + show (Fun f []) = f + show (Fun f (x : xs)) = f ++ "(" ++ show x ++ foldr ((++) . (", "++) . show) ")" xs + +instance Show Formula where + show (Pred p []) = p + show (Pred p (x : xs)) = p ++ "(" ++ show x ++ foldr ((++) . (", "++) . show) ")" xs + 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 (All x f) = "(forall " ++ x ++ ". " ++ show f ++ ")" + show (Exists x f) = "(exists " ++ x ++ ". " ++ show f ++ ")" + show T = "true" + show F = "false" \ No newline at end of file diff --git a/app/Lexer.hs b/app/Lexer.hs new file mode 100644 index 0000000..2184d43 --- /dev/null +++ b/app/Lexer.hs @@ -0,0 +1,48 @@ +{-# LANGUAGE ImportQualifiedPost #-} + +module Lexer where + +import Text.Parsec.Char (alphaNum, letter, oneOf) +import Text.Parsec.Language (emptyDef) +import Text.Parsec.String (Parser) +import Text.Parsec.Token qualified as Tok + +lexer :: Tok.TokenParser () +lexer = Tok.makeTokenParser style + where + ops = ["/\\", "\\/", "->", "!"] + names = ["forall", "exists"] + style = + emptyDef + { Tok.commentLine = "" + , Tok.reservedOpNames = ops + , Tok.reservedNames = names + , Tok.opStart = oneOf "\\/-" + , Tok.opLetter = oneOf "\\/>" + , Tok.identStart = letter + , Tok.identLetter = alphaNum + } + +parens :: Parser a -> Parser a +parens = Tok.parens lexer + +dot :: Parser String +dot = Tok.dot lexer + +comma :: Parser String +comma = Tok.comma lexer + +semi :: Parser String +semi = Tok.semi lexer + +identifier :: Parser String +identifier = Tok.identifier lexer + +reserved :: String -> Parser () +reserved = Tok.reserved lexer + +reservedOp :: String -> Parser () +reservedOp = Tok.reservedOp lexer + +whiteSpace :: Parser () +whiteSpace = Tok.whiteSpace lexer \ No newline at end of file diff --git a/app/Main.hs b/app/Main.hs index f13f5e2..b1aa46f 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -2,42 +2,13 @@ module Main where import Data.List import Data.Maybe -import Debug.Trace +import qualified Data.Set as Set +import FOLSyntax +import Parser -{- -First we define first order predicate logic --} - -data Term = Var String | Fun String [Term] deriving (Eq) -data Formula - = Pred String [Term] - | Neg Formula - | Conj Formula Formula - | Disj Formula Formula - | Impl Formula Formula - | All String Formula - | Exists String Formula - | T - | F - deriving (Eq) - - -instance Show Term where - show (Var x) = x - show (Fun f []) = f - show (Fun f (x : xs)) = f ++ "(" ++ show x ++ foldr ((++) . (", "++) . show) ")" xs - -instance Show Formula where - show (Pred p []) = p - show (Pred p (x : xs)) = p ++ "(" ++ show x ++ foldr ((++) . (", "++) . show) ")" xs - 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 (All x f) = "forall " ++ x ++ ". " ++ show f - show (Exists x f) = "exists " ++ x ++ ". " ++ show f - show T = "true" - show F = "false" +fromRight :: Either a b -> b +fromRight (Left _) = error "fromRight called on left value!" +fromRight (Right b) = b -- free variables of a term termFreeVars :: Term -> [String] @@ -162,19 +133,19 @@ renameBinders f = fst $ go f [] -- prenex normalform -- TODO make it so that forall has higher priority to be moved left (makes skolem functions smaller) makePNF :: Formula -> Formula -makePNF form = go $ renameBinders . makeNNF $ form +makePNF form = go form where go f = let f' = pnfStep f in if f == f' then f else go f' -- swapping rules - pnfStep (Conj phi (All x psi)) = All x (Conj phi psi) - pnfStep (Disj phi (All x psi)) = All x (Disj phi psi) - pnfStep (Conj (All x psi) phi) = All x (Conj psi phi) - pnfStep (Disj (All x psi) phi) = All x (Disj psi phi) pnfStep (Conj phi (Exists x psi)) = Exists x (Conj phi psi) pnfStep (Disj phi (Exists x psi)) = Exists x (Disj phi psi) pnfStep (Conj (Exists x psi) phi) = Exists x (Conj psi phi) pnfStep (Disj (Exists x psi) phi) = Exists x (Disj psi phi) + pnfStep (Conj phi (All x psi)) = All x (Conj phi psi) + pnfStep (Disj phi (All x psi)) = All x (Disj phi psi) + pnfStep (Conj (All x psi) phi) = All x (Conj psi phi) + pnfStep (Disj (All x psi) phi) = All x (Disj psi phi) {- pnfStep (Conj phi (Exists x psi)) = Exists x (Conj phi psi) pnfStep (Conj phi (All x psi)) = All x (Conj phi psi) @@ -214,7 +185,7 @@ usedFunctions _ = [] -- skolem form of a formula makeSkolem :: Formula -> Formula -makeSkolem form = go (makePNF form) [] [] +makeSkolem form = go form [] [] where substTermInFormula :: Formula -> String -> Term -> Formula substTermInFormula (Pred p ts) x s = Pred p $ map (\t -> termSubst t x s) ts @@ -232,21 +203,21 @@ makeSkolem form = go (makePNF form) [] [] -- conjunctive normalform, removes all quantors, so its ready for resolution makeCNF :: Formula -> Formula -makeCNF form = go $ makeSkolem form +makeCNF form = go form where go f = let f' = cnfStep f in if f == f' then f else go f' - cnfStep (Conj phi psi) = Conj (makeCNF phi) (makeCNF psi) - cnfStep (Disj (Conj phi psi) xi) = Conj (makeCNF $ Disj phi xi) (makeCNF $ Disj psi xi) - cnfStep (Disj xi (Conj phi psi)) = Conj (makeCNF $ Disj xi phi) (makeCNF $ Disj xi psi) - cnfStep (All _ f) = makeCNF f - cnfStep (Exists _ f) = makeCNF f + 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 (All _ f) = cnfStep f + cnfStep (Exists _ f) = cnfStep f cnfStep f = f -- create the list of clauses from a formula -- TODO not working correctly for `makeCNFList formula5` makeCNFList :: Formula -> [[Formula]] -makeCNFList form = go $ makeCNF form +makeCNFList form = go form where go (Conj f1 f2) = go f1 ++ go f2 go (Disj f1 f2) = [collectDisjs f1 ++ collectDisjs f2] @@ -280,22 +251,36 @@ 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 --- a single resolution step as described in gloin -rifStep :: [[Formula]] -> Either () [[Formula]] -rifStep clauses | trace (show clauses) True = if [] `elem` clauses then Left () else Right newClauses +-- replace every fresh variable in a formula with a new name, this is only correct in our resolution context!! +makeVariablesDisjunct :: [[Formula]] -> [[Formula]] +makeVariablesDisjunct form = snd $ foldr (\clause (used', clauses') -> let (used'', clause') = makeClauseDisjunct used' clause in (used'', clause' : clauses')) ([], []) form +makeClauseDisjunct :: [String] -> [Formula] -> ([String], [Formula]) +makeClauseDisjunct used clause = (concatMap formulaVars newClause ++ newUsed, newClause) where + criticalVars = used `intersect` concatMap formulaVars clause + (newUsed, newClause) = foldr foldFun (used, clause) criticalVars + where + foldFun oldVar (used', clause') = (v' : used', map (\f -> renameFormula f oldVar v') clause') + where + v' = findFresh used' + +-- a single resolution step as described in gloin +-- TODO before each step, rename every clause so that variable names are disjunct! +rifStep :: [[Formula]] -> Either () [[Formula]] +rifStep clauses = if [] `elem` clauses then Left () else Right newClauses + where + -- rename all variables + clauses' = makeVariablesDisjunct clauses resolveClauses :: [Formula] -> [Formula] -> [(([Formula], [Formula]), [(Term, Term)])] resolveClauses c1 c2 = let zippedElems = [((e1, c1), (e2, c2)) | e1 <- c1, e2 <- c2] in mapMaybe (uncurry unifyPredicates) zippedElems - zippedClauses = [(c1, c2) | c1 <- clauses, c2 <- clauses, c1 /= c2] + zippedClauses = [(c1, c2) | c1 <- clauses', c2 <- clauses', c1 /= c2] clausesWithMgus = concatMap (uncurry resolveClauses) zippedClauses - newClauses = clauses ++ map (\((f1, f2), mgu) -> map (`applyMgu` mgu) f1 ++ map (`applyMgu` mgu) f2) clausesWithMgus -rifStep _ = undefined + newClauses = Set.toList . Set.fromList $ clauses' ++ map (\((f1, f2), mgu) -> map (`applyMgu` mgu) f1 ++ map (`applyMgu` mgu) f2) clausesWithMgus -- do resolution until we have proven unfulfillability of formula set doResolution :: [[Formula]] -> Either () [[Formula]] -doResolution f= do +doResolution f = do f' <- rifStep f - -- TODO after every resolution step make variable names of clauses disjunct doResolution f' {- @@ -305,7 +290,34 @@ To prove a formula we: 3. doResolution on clause list -} proveFormula :: Formula -> Either () [[Formula]] -proveFormula form = doResolution $ makeCNFList (Neg form) +proveFormula form = doResolution . makeCNFList . makeCNF . makeSkolem . makePNF . renameBinders . makeNNF $ Neg form + +proveFormulaIO :: Formula -> IO () +proveFormulaIO f = do + let f' = makeNNF (Neg f) + print f' + putStrLn "" + let f'' = renameBinders f' + print f'' + putStrLn "" + + let f''' = makePNF f'' + print f''' + putStrLn "" + + let f'''' = makeSkolem f''' + print f'''' + putStrLn "" + + let g = makeCNF f'''' + print g + putStrLn "" + + let g' = makeCNFList g + print g' + case doResolution g' of + Left _ -> putStrLn "Success!!" + _ -> return () -- unification examples terma1 :: Term @@ -326,14 +338,14 @@ formula1 :: Formula formula1 = Neg (Conj (Disj (Pred "A" []) (Neg $ Pred "B" [])) (Pred "C" [])) -- PNF and skolem example from gloin -formula2 :: Formula -formula2 = All "x" $ Impl (All "y" $ Pred "L" [Var "y", Var "x"]) (Exists "y" $ Pred "M" [Var "x", Var "y"]) +formula2 :: String +formula2 = "forall x. (forall y. L(y,x)) -> exists y.M(x,y)" -- Resolution example from gloin script formula3 :: Formula formula3 = Impl (Conj (Pred "P" [Fun "a" []]) (All "x" $ Impl (Pred "P" [Var "x"]) (Pred "P" [Fun "f" [Var "x"]]))) (Exists "x" $ Pred "P" [Fun "f" [Fun "f" [Var "x"]]]) --- Resolution example from gloin exercises +-- Resolution example from gloin exercises (already in cnf) formula4 :: Formula formula4 = Conj (Disj (Pred "P" [Fun "f" [Var "x"], Var "y"]) (Disj (Pred "S" [Var "y", Var "z"]) (Pred "P" [Var "y"]))) (Conj (Neg $ Pred "S" [Fun "f" [Fun "f" [Var "x"]], Var "x"]) (Neg $ Pred "P" [Fun "f" [Var "z"]])) @@ -353,13 +365,13 @@ formula5 = Impl (Conj (Conj phi1 phi2) phi3) psi' -- exercise 2: Ärzte und Quacksalber formula6 :: [[Formula]] formula6 = [ - [Neg $ Pred "D" [Var "x1"], Pred "L" [Fun "f" [Var "x1"], Var "x1"]], + [Neg $ Pred "D" [Var "x1"], Pred "L" [Fun "f" [Var "x1"], Var "x1"]], [Pred "P" [Fun "f" [Var "x2"]], Neg $ Pred "L" [Fun "f" [Var "x2"], Var "x2"]], [Neg $ Pred "P" [Var "x3"], Neg $ Pred "Q" [Var "y3"], Neg $ Pred "L" [Var "x3", Var "y3"]], [Pred "D" [Fun "a" []]], [Pred "Q" [Fun "a" []]]] --- Drogenschmuggel but already as clauses +-- Drogenschmuggel but already as clauses, fifth clause is wrong, arguments to S need to be swapped!! formula7 :: [[Formula]] formula7 = [ [Neg $ Pred "E" [Var "x2"], Pred "I" [Var "x2"], Pred "Z" [Fun "f" [Var "x2"]]], @@ -371,14 +383,33 @@ formula7 = [ [Neg $ Pred "Z" [Var "x5"], Neg $ Pred "D" [Var "x5"]] ] +formula8 :: [[Formula]] +formula8 = [ + [Neg $ Pred "E" [Var "x2"], Pred "I" [Var "x2"], Pred "Z" [Fun "f" [Var "x21", Var "x22", Var "x2"]]], + [Neg $ Pred "E" [Var "x3"], Pred "I" [Var "x3"], Pred "S" [Var "x3", Fun "f" [Var "x31", Var "x32", Var "x3"]]], + [Pred "D" [Fun "c" [Var "x5", Var "x4"]]], + [Pred "E" [Fun "c" [Var "x5'", Var "x4'"]]], + [Neg $ Pred "S" [Fun "c" [Var "x5''", Var "x4''"], Var "y"], Pred "D" [Var "y"]], + [Neg $ Pred "I" [Var "x44"], Neg $ Pred "D" [Var "x44"]], + [Neg $ Pred "Z" [Var "x55"], Neg $ Pred "D" [Var "x55"]] + ] + +-- aerzte und quacksalber v2 +formula9 :: Formula +formula9 = Impl (Conj psi1 psi2) psi3 + where + psi1 = All "x" $ Impl (Pred "D" [Var "x"]) (Exists "y" $ Conj (Pred "P" [Var "y"]) (Pred "L" [Var "y", Var "x"])) + psi2 = All "x" $ Impl (Pred "P" [Var "x"]) (All "y" $ Impl (Pred "Q" [Var "y"]) (Neg $ Pred "L" [Var "x", Var "y"])) + psi3 = All "x" $ Impl (Pred "D" [Var "x"]) (Neg $ Pred "Q" [Var "x"]) + main :: IO () main = do putStrLn $ "Now making NNF of formula: " ++ show formula1 print $ makeNNF formula1 putStrLn $ "Now making PNF of formula: " ++ show formula2 - print $ makePNF formula2 + print $ makePNF (fromRight $ parseFormula formula2) putStrLn $ "Now making Skolemform of formula: " ++ show formula2 - print $ makeSkolem formula2 + print $ makeSkolem (fromRight $ parseFormula formula2) putStrLn $ "Now proving formula by resolution: " ++ show formula3 case proveFormula formula3 of Left _ -> putStrLn "Success!" @@ -389,5 +420,13 @@ main = do Right _ -> return () putStrLn $ "Now Proving formula by resolution: " ++ show formula6 case doResolution formula6 of + Left _ -> putStrLn "Success!" + Right _ -> return () + putStrLn $ "Now Proving formula by resolution: " ++ show (Neg formula5) + case proveFormula (Neg formula5) of + Left _ -> putStrLn "Success!" + Right _ -> return () + putStrLn $ "Now proving formula by resolution: " ++ show formula7 + case doResolution formula7 of Left _ -> putStrLn "Success!" Right _ -> return () \ No newline at end of file diff --git a/app/Parser.hs b/app/Parser.hs new file mode 100644 index 0000000..27d2a41 --- /dev/null +++ b/app/Parser.hs @@ -0,0 +1,79 @@ +module Parser (parseFormula) where + +import Lexer +import FOLSyntax +import Text.Parsec +import Text.Parsec.String (Parser) +import Data.Functor + +import Prelude hiding (pred, all) + + +term :: Parser Term +term = try fun <|> var + +fun :: Parser Term +fun = + Fun + <$> identifier + <*> parens (term `sepBy` comma) + +var :: Parser Term +var = Var <$> identifier + + +formula :: Parser Formula +formula = neg <|> impl <|> all <|> exists <|> pred <|> true <|> false "formula" + +pred :: Parser Formula +pred = + Pred + <$> identifier + <*> parens (term `sepBy` comma) + +neg :: Parser Formula +neg = + Neg + <$> (reservedOp "!" *> negFormula) + where negFormula = neg <|> all <|> exists <|> true <|> false <|> parens formula <|> pred "formula under neg" + +impl :: Parser Formula +impl = foldr1 Impl <$> implFormula `sepBy` reservedOp "->" + where implFormula = neg <|> disj <|> conj <|> all <|> exists <|> true <|> false <|> parens formula <|> pred "formula under impl" + +disj :: Parser Formula +disj = foldr1 Disj <$> disjFormula `sepBy` reservedOp "\\/" + where disjFormula = neg <|> conj <|> all <|> exists <|> true <|> false <|> parens formula <|> pred "formula under disj" + +conj :: Parser Formula +conj = foldr1 Conj <$> conjFormula `sepBy` reservedOp "/\\" + where conjFormula = neg <|> all <|> exists <|> true <|> false <|> parens formula <|> pred "formula under conj" + +all :: Parser Formula +all = + All + <$> (reserved "forall" *> identifier) + <*> (dot *> formula) + +exists :: Parser Formula +exists = + Exists + <$> (reserved "exists" *> identifier) + <*> (dot *> formula) + +true :: Parser Formula +true = reserved "true" $> T + +false :: Parser Formula +false = reserved "false" $> F + +-- runners +contents :: Parser a -> Parser a +contents p = do + whiteSpace + r <- p + eof + return r + +parseFormula :: String -> Either ParseError Formula +parseFormula = parse (contents formula) "stdin" \ No newline at end of file diff --git a/resolution.cabal b/resolution.cabal index 2421074..1feb784 100644 --- a/resolution.cabal +++ b/resolution.cabal @@ -66,10 +66,12 @@ executable resolution -- other-extensions: -- Other library packages from which modules are imported. - build-depends: base ^>=4.16.4.0, containers, extra + build-depends: base ^>=4.16.4.0, containers, extra, parsec -- Directories containing source files. hs-source-dirs: app + other-modules: Lexer, Parser, FOLSyntax + -- Base language which the package is written in. default-language: Haskell2010