Folly 0.1.4.6 → 0.1.5.0

raw patch · 9 files changed

+183/−90 lines, 9 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• Folly.cabal +4/−4
• src/Folly/Clause.hs +85/−0
• src/Folly/Formula.hs +1/−8
• src/Folly/Resolution.hs +12/−36
• src/Folly/Theorem.hs +2/−2
• src/Folly/Unification.hs +4/−4
• test/Folly/ResolutionTests.hs +61/−22
• test/Main.hs +0/−14
• test/TestMain.hs +14/−0

@@ -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

@@ -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 "  "

@@ -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

@@ -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

@@ -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 

@@ -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

@@ -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

@@ -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

@@ -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