diff --git a/Folly.cabal b/Folly.cabal --- a/Folly.cabal +++ b/Folly.cabal @@ -2,7 +2,7 @@ -- see http://haskell.org/cabal/users-guide/ name: Folly -version: 0.1.4.6 +version: 0.1.5.0 synopsis: A first order logic library in Haskell description: An implementation of first order logic in Haskell that includes a library of modules for incorporating first @@ -20,7 +20,7 @@ cabal-version: >=1.8 library - exposed-modules: Folly.Formula, Folly.Unification, Folly.Resolution, Folly.Utils, Folly.Theorem, Folly.Lexer, Folly.Parser + exposed-modules: Folly.Formula, Folly.Unification, Folly.Resolution, Folly.Utils, Folly.Theorem, Folly.Lexer, Folly.Parser, Folly.Clause build-depends: base < 6, containers, parsec hs-source-dirs: src @@ -31,7 +31,7 @@ hs-source-dirs: src executable Folly-tests - main-is: Main.hs - other-modules: Folly.FormulaTests, Folly.LexerTests, Folly.ParserTests, Folly.ResolutionTests, Folly.UnificationTests, Folly.TestUtils + main-is: TestMain.hs + other-modules: Folly.FormulaTests, Folly.LexerTests, Folly.ParserTests, Folly.ResolutionTests, Folly.UnificationTests, Folly.TestUtils, Folly.Clause build-depends: base < 6, HUnit, containers, parsec hs-source-dirs: test, src diff --git a/src/Folly/Clause.hs b/src/Folly/Clause.hs new file mode 100644 --- /dev/null +++ b/src/Folly/Clause.hs @@ -0,0 +1,85 @@ +module Folly.Clause(Clause, + givenClause, Folly.Clause.empty, + deleteTautologies, + resolvedClauses, + showTrace) where + +import Data.List as L +import Data.Maybe +import Data.Set as S + +import Folly.Formula +import Folly.Unification + +data Clause = Clause (Set Formula) Justification + deriving (Show) + +instance Eq Clause where + (==) (Clause cs1 _) (Clause cs2 _) = cs1 == cs2 + +instance Ord Clause where + (<=) (Clause cs1 _) (Clause cs2 _) = cs1 <= cs2 + +givenClause cs = Clause cs Given +resolvedClause cs lc rc mgu = Clause cs (Resolved lc rc mgu) + +empty = Clause S.empty Given + +data Justification + = Given + | Resolved Clause Clause Unifier + deriving (Eq, Ord, Show) + +deleteTautologies :: Set Clause -> Set Clause +deleteTautologies formulas = S.filter (not . dnfIsTautology) formulas + +dnfIsTautology :: Clause -> Bool +dnfIsTautology (Clause lits _) = isTautology lits + +isTautology :: Set Formula -> Bool +isTautology c = S.size (S.intersection atoms negAtoms) > 0 + where + atoms = S.filter isAtom c + negAtoms = S.map stripNegations $ S.filter (not . isAtom) c + +resolvedClauses :: Clause -> Clause -> Set Clause +resolvedClauses l@(Clause left _) r@(Clause right _) = + case left == right of + True -> S.empty + False -> S.fromList resClauses + where + possibleResCombos = [(x, l, y, r) | x <- (S.toList left), y <- (S.toList right)] + mResClauses = L.map (\(x, l, y, r) -> tryToResolve x l y r) possibleResCombos + resClauses = L.map fromJust $ L.filter (/= Nothing) mResClauses + +tryToResolve :: Formula -> Clause -> Formula -> Clause -> Maybe Clause +tryToResolve leftLiteral leftClause rightLiteral rightClause = + case matchingLiterals leftLiteral rightLiteral of + True -> unifiedResolvedClause leftLiteral leftClause rightLiteral rightClause + False -> Nothing + +unifiedResolvedClause :: Formula -> Clause -> Formula -> Clause -> Maybe Clause +unifiedResolvedClause lLit l@(Clause lc _) rLit r@(Clause rc _) = + case L.length (literalArgs lLit) == L.length (literalArgs rLit) of + True -> + case mostGeneralUnifier $ zip (literalArgs lLit) (literalArgs rLit) of + Just mgu -> + Just $ mkResolvedClause mgu resolvedLits l r + Nothing -> Nothing + False -> Nothing + where + resolvedLits = S.union (S.delete lLit lc) (S.delete rLit rc) + +mkResolvedClause :: Unifier -> Set Formula -> Clause -> Clause -> Clause +mkResolvedClause mgu lits lc rc = + resolvedClause (S.map (\lit -> applyToTerms lit (applyUnifier mgu)) lits) lc rc mgu + +showTrace c = showTraceRec 0 c + +showTraceRec n c@(Clause cs Given) = (ind n) ++ "GIVEN " ++ show cs +showTraceRec n c@(Clause cs (Resolved a b u)) = + (ind n) ++ show cs ++ "\t" ++ show u ++ "\n" ++ + showTraceRec (n+1) a ++ "\n" ++ + showTraceRec (n+1) b + +ind n = L.concat $ L.replicate n " " diff --git a/src/Folly/Formula.hs b/src/Folly/Formula.hs --- a/src/Folly/Formula.hs +++ b/src/Folly/Formula.hs @@ -5,13 +5,12 @@ appendVarName, var, func, constant, te, fa, pr, con, dis, neg, imp, bic, t, f, - vars, freeVars, + vars, freeVars, isAtom, stripNegations, generalize, subFormula, applyToTerms, literalArgs, toPNF, toSkolemForm, skf, toClausalForm, - isTautology, matchingLiterals) where import Control.Monad @@ -295,9 +294,3 @@ splitDis :: Formula -> [Formula] splitDis (B "|" l r) = (splitDis l) ++ (splitDis r) splitDis f = [f] - -isTautology :: [Formula] -> Bool -isTautology c = L.length (L.intersect atoms negAtoms) > 0 - where - atoms = L.filter isAtom c - negAtoms = L.map stripNegations $ L.filter (not . isAtom) c diff --git a/src/Folly/Resolution.hs b/src/Folly/Resolution.hs --- a/src/Folly/Resolution.hs +++ b/src/Folly/Resolution.hs @@ -1,60 +1,39 @@ -module Folly.Resolution( - isValid) where +module Folly.Resolution(isValid) where import Data.List as L -import Data.Maybe import Data.Set as S +import Folly.Clause as C import Folly.Formula import Folly.Theorem -import Folly.Unification isValid :: Theorem -> Bool isValid t = not $ resolve $ deleteTautologies $ clauseSet where formulas = (neg (conclusion t)) : (hypothesis t) - clauses = uniqueVarNames $ L.concat $ L.map toClausalForm formulas + clauses = L.map (givenClause . S.fromList) $ uniqueVarNames $ toClausalForm $ L.foldr (\l r -> con l r) (head formulas) (tail formulas) clauseSet = S.fromList clauses -resolve :: Set [Formula] -> Bool -resolve cls = case S.member [] cls of - True -> True +resolve :: Set Clause -> Bool +resolve cls = case S.member C.empty cls of + True -> False False -> resolveIter [cls] -resolveIter :: [Set [Formula]] -> Bool +resolveIter :: [Set Clause] -> Bool resolveIter [] = error "Empty list of clause sets" resolveIter clauseSets = case S.size newClauses == 0 of True -> True - False -> case S.member [] newClauses of + False -> case S.member C.empty newClauses of True -> False False -> resolveIter (newClauses:clauseSets) where - newClauses = case L.length clauseSets of - 1 -> generateNewClauses (head clauseSets) (head clauseSets) - _ -> generateNewClauses (head clauseSets) (L.foldl S.union S.empty (tail clauseSets)) + newClauses = generateNewClauses (head clauseSets) (L.foldl S.union S.empty clauseSets) -generateNewClauses :: Set [Formula] -> Set [Formula] -> Set [Formula] +generateNewClauses :: Set Clause -> Set Clause -> Set Clause generateNewClauses recent old = deleteTautologies $ newClauses where - newClauses = S.fold S.union S.empty $ S.map (\ c -> genNewClauses c old) recent - genNewClauses c cs = S.fold S.union S.empty $ S.map (\ x -> resolvedClauses c x) cs - -resolvedClauses :: [Formula] -> [Formula] -> Set [Formula] -resolvedClauses left right = S.fromList resClauses - where - mResClauses = L.map (\ x -> (L.map (\ y -> tryToResolve x left y right) right)) left - resClauses = L.map fromJust $ L.filter (/= Nothing) $ L.concat mResClauses - -tryToResolve :: Formula -> [Formula] -> Formula -> [Formula] -> Maybe [Formula] -tryToResolve leftLiteral leftClause rightLiteral rightClause = - case matchingLiterals leftLiteral rightLiteral of - True -> unifiedResolvedClause leftLiteral leftClause rightLiteral rightClause - False -> Nothing - -unifiedResolvedClause :: Formula -> [Formula] -> Formula -> [Formula] -> Maybe [Formula] -unifiedResolvedClause lLit lc rLit rc = case mostGeneralUnifier $ zip (literalArgs lLit) (literalArgs rLit) of - Just mgu -> Just $ L.map (\ lit -> applyToTerms lit (applyUnifier mgu)) ((L.delete lLit lc) ++ (L.delete rLit rc)) - Nothing -> Nothing + newClauses = S.fold S.union S.empty $ S.map (\c -> genNewClauses c old) recent + genNewClauses c cs = S.fold S.union S.empty $ S.map (\x -> resolvedClauses c x) cs uniqueVarNames :: [[Formula]] -> [[Formula]] uniqueVarNames cls = zipWith attachSuffix cls (L.map show [1..length cls]) @@ -64,6 +43,3 @@ addSuffixToVarNames :: String -> Formula -> Formula addSuffixToVarNames suffix form = applyToTerms form (appendVarName suffix) - -deleteTautologies :: Set [Formula] -> Set [Formula] -deleteTautologies clauses = S.filter (not . isTautology) clauses diff --git a/src/Folly/Theorem.hs b/src/Folly/Theorem.hs --- a/src/Folly/Theorem.hs +++ b/src/Folly/Theorem.hs @@ -15,10 +15,10 @@ show = showThm showThm :: Theorem -> String -showThm (Theorem h c) = "Hypothesis:\n" ++ hypStr ++ "\n\n|=\n\n" ++ conclStr +showThm (Theorem h c) = "\n" ++ hypStr ++ "\n\n|=\n\n" ++ conclStr where hypStr = (L.concat $ L.intersperse "\n" $ L.map show h) - conclStr = "Conclusion:\n" ++ show c + conclStr = show c theorem = Theorem diff --git a/src/Folly/Unification.hs b/src/Folly/Unification.hs --- a/src/Folly/Unification.hs +++ b/src/Folly/Unification.hs @@ -1,7 +1,7 @@ -module Folly.Unification( - applyUnifier, - mostGeneralUnifier, - unifier) where +module Folly.Unification(Unifier, + applyUnifier, + mostGeneralUnifier, + unifier) where import Control.Monad import Data.List as L diff --git a/test/Folly/ResolutionTests.hs b/test/Folly/ResolutionTests.hs --- a/test/Folly/ResolutionTests.hs +++ b/test/Folly/ResolutionTests.hs @@ -11,31 +11,70 @@ testIsValid = testFunction isValid isValidTestCases +x = var "x" +y = var "y" +z = var "z" +a = var "a" +d = var "d" +p = var "p" + +one = constant "1" +john = constant "John" +fido = constant "Fido" + +times a b = func "*" [a, b] + +eq a b = pr "=" [a, b] +dog d = pr "Dog" [d] +owns a b = pr "Owns" [a, b] +kills a b = pr "Kills" [a, b] +loves a b = pr "Loves" [a, b] +lovesAnimals a = pr "LovesAnimals" [a] + isValidTestCases :: [(Theorem, Bool)] isValidTestCases = - [(theorem [] (fa (var "a") (dis (pr "d" [var "a"]) (neg (pr "d" [var "a"])))), True), - (theorem [] (pr "d" [var "k"]), False), - (theorem [pr "Dog" [var "x"]] (pr "Dog" [var "x"]), True), - (theorem - [(fa (var "d") (imp (pr "Dog" [var "d"]) (pr "Loves" [constant "John", var "d"]))), - (pr "Dog" [constant "Fido"])] - (pr "Loves" [constant "John", constant "Fido"]), True), - (theorem - [(fa (var "p") (imp (te (var "d") (con (pr "Dog" [var "d"]) (pr "Owns" [var "p", var "d"]))) (pr "LovesAnimals" [var "p"]))), - (imp (pr "LovesAnimals" [var "x"]) (fa (var "a") (neg (pr "Kills" [var "x", var "a"])))), - (pr "Owns" [constant "John", constant "Fido"]), - (pr "Dog" [constant "Fido"])] - (fa (var "a") (neg (pr "Kills" [constant "John", var "a"]))), True), - (theorem groupWithEquals (imp (con (con (con (pr "=" [func "*" [var "x", var "y"], constant "1"]) (pr "=" [func "*" [var "y", var "x"], constant "1"])) (pr "=" [func "*" [var "x", var "z"], constant "1"])) (pr "=" [func "*" [var "z", var "x"], constant "1"])) (pr "=" [var "y", var "z"])), True), - (theorem groupWithEquals (imp (fa (var "x") (con (pr "=" [func "*" [var "x", var "z"], constant "1"]) (pr "=" [func "*" [var "z", var "x"], constant "1"]))) (pr "=" [var "z", constant "1"])), True)] + [(dog1, True), + (dog2, False), + (dog3, True), + (dog4, True), + (dog5, True), + (dog6, False), + (group1, True), + (group2, True)] +-- (group3, False)] +dog1 = theorem [] (fa a (dis (dog a) (neg (dog a)))) +dog2 = theorem [] (dog a) +dog3 = theorem [dog x] (dog x) +dog4 = theorem [(fa d (imp (dog d) (loves john d))), dog fido] (loves john fido) +dog5 = theorem + [(fa p (imp (te d (con (dog d) (owns p d))) (lovesAnimals p))), + (imp (lovesAnimals x) (fa a (neg (kills x a)))), + owns john fido, + dog fido] + (fa a (neg (kills john a))) +dog6 = theorem [] (con (dog a) (neg $ dog a)) + +group1 = theorem + groupAxioms + (imp + (con (con (con (eq (times x y) one) (eq (times y x) one)) (eq (times x z) one)) (eq (times z x) one)) + (eq y z)) +group2 = theorem groupAxioms (imp (fa x (con (eq (times x z) one) (eq (times z x) one))) (eq z one)) + +group3 = + theorem groupAxioms (fa x (fa y (eq (times x y) (times y x)))) + +group4 = theorem (tail equalityAxioms) (head equalityAxioms) + equalityAxioms :: [Formula] equalityAxioms = - [(fa (var "x") (pr "=" [var "x", var "x"])), - (fa (var "x") (fa (var "y") (imp (pr "=" [var "x", var "y"]) (pr "=" [var "y", var "x"])))), - (fa (var "x") (fa (var "y") (fa (var "z") (imp (con (pr "=" [var "x", var "y"]) (pr "=" [var "y", var "z"])) (pr "=" [var "x", var "z"])))))] + [(fa x (pr "=" [x, x])), + (fa x (fa y (imp (eq x y) (eq y x)))), + (fa x (fa y (fa z (imp (con (eq x y) (eq y z)) (eq x z)))))] -groupWithEquals = - [(fa (var "x") (te (var "y") (con (pr "=" [func "*" [var "x", var "y"], constant "1"]) (pr "=" [func "*" [var "y", var "x"], constant "1"])))), - (fa (var "x") (fa (var "y") (fa (var "z") (pr "=" [func "*" [var "x", func "*" [var "y", var "z"]], func "*" [func "*" [var "x", var "y"], var "z"]])))), - (fa (var "x") (con (pr "=" [func "*" [var "x", constant "1"], var "x"]) (pr "=" [func "*" [constant "1", var "x"], constant "x"])))] ++ equalityAxioms +groupAxioms = + [(fa x (te y (con (eq (times x y) one) (eq (times y x) one)))), + (fa x (fa y (fa z (eq (times x (times y z)) (times (times x y) z))))), + (fa x (con (eq (times x one) x) (eq (times one x) x)))] ++ + equalityAxioms diff --git a/test/Main.hs b/test/Main.hs deleted file mode 100644 --- a/test/Main.hs +++ /dev/null @@ -1,14 +0,0 @@ -module Main(main) where - -import Folly.FormulaTests -import Folly.LexerTests -import Folly.ParserTests -import Folly.ResolutionTests -import Folly.UnificationTests - -main = do - allFormulaTests - allLexerTests - allParserTests - allResolutionTests - allUnificationTests diff --git a/test/TestMain.hs b/test/TestMain.hs new file mode 100644 --- /dev/null +++ b/test/TestMain.hs @@ -0,0 +1,14 @@ +module TestMain(main) where + +import Folly.FormulaTests +import Folly.LexerTests +import Folly.ParserTests +import Folly.ResolutionTests +import Folly.UnificationTests + +main = do + allFormulaTests + allLexerTests + allParserTests + allResolutionTests + allUnificationTests