Folly 0.1.5.2 → 0.2.0.0

raw patch · 5 files changed

+74/−38 lines, 5 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Folly.cabal +1/−1
• src/Folly/Clause.hs +16/−4
• src/Folly/Formula.hs +11/−2
• src/Folly/Resolution.hs +31/−30
• src/Folly/Unification.hs +15/−1

@@ -2,7 +2,7 @@ --  see http://haskell.org/cabal/users-guide/  name:                Folly-version:             0.1.5.2+version:             0.2.0.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

@@ -5,6 +5,7 @@                     showTrace) where  import Data.List as L+import Data.Map as M import Data.Maybe import Data.Set as S @@ -21,15 +22,21 @@   (<=) (Clause cs1 _) (Clause cs2 _) = cs1 <= cs2  givenClause cs = Clause cs Given-resolvedClause cs lc rc mgu = Clause cs (Resolved lc rc mgu)+resolvedClause cs lc rc mgu = Clause cs (Resolved lc rc mgu M.empty)  empty = Clause S.empty Given  data Justification   = Given-  | Resolved Clause Clause Unifier+  | Resolved Clause Clause Unifier Unifier     deriving (Eq, Ord, Show) +applySub :: Unifier -> Clause -> Clause+applySub u c@(Clause lits j) =+  Clause (S.map (\lit -> applyToTerms lit (applyUnifier u)) lits) j++allVars (Clause cs _) = L.concatMap collectVars $ S.toList cs+ deleteTautologies :: Set Clause -> Set Clause deleteTautologies formulas = S.filter (not . dnfIsTautology) formulas @@ -43,7 +50,12 @@     negAtoms = S.map stripNegations $ S.filter (not . isAtom) c  resolvedClauses :: Clause -> Clause -> Set Clause-resolvedClauses l@(Clause left _) r@(Clause right _) =+resolvedClauses c1 c2 =+  let rho = uniqueVarSub (allVars c1) (allVars c2) in+   resolvedClausesU (applySub rho c1) c2++resolvedClausesU :: Clause -> Clause -> Set Clause+resolvedClausesU l@(Clause left _) r@(Clause right _) =   case left == right of    True ->  S.empty    False -> S.fromList resClauses@@ -77,7 +89,7 @@ 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)) =+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

@@ -1,8 +1,8 @@ module Folly.Formula(   Term, Formula,   fvt, subTerm, isVar, isConst, isFunc,-  funcName, funcArgs,-  appendVarName,+  funcName, funcArgs, varName,+  appendVarName, collectVars,   var, func, constant,   te, fa, pr, con, dis, neg, imp, bic, t, f,   vars, freeVars, isAtom, stripNegations,@@ -51,6 +51,8 @@   False -> Func n args constant n = Constant n +varName (Var n) = n+ appendVarName :: String -> Term -> Term appendVarName suffix (Var n) = Var (n ++ suffix) appendVarName suffix (Func name args) = Func name $ L.map (appendVarName suffix) args@@ -94,6 +96,13 @@ applyToTerms (B n l r) f = B n (applyToTerms l f) (applyToTerms r f) applyToTerms (Q n v l) f = Q n (f v) (applyToTerms l f) applyToTerms (N l) f = N (applyToTerms l f)++collectVars :: Formula -> [Term]+collectVars (P _ args) = L.concatMap (\t -> if isVar t then [t] else []) args+collectVars (N f) = collectVars f+collectVars (B _ a b) = collectVars a ++ collectVars b+collectVars (Q _ v f) = v:(collectVars f)+collectVars _ = []  te :: Term -> Formula -> Formula te v@(Var _) f = Q "E" v f

@@ -1,4 +1,7 @@-module Folly.Resolution(isValid) where+module Folly.Resolution(isValid,+                        isValid',+                        standardSkolem,+                        maxClause) where  import Data.List as L import Data.Set as S@@ -8,38 +11,36 @@ import Folly.Theorem  isValid :: Theorem -> Bool-isValid t = not $ resolve $ deleteTautologies $ clauseSet-  where-    formulas = (neg (conclusion t)) : (hypothesis t)-    clauses = L.map (givenClause . S.fromList) $ uniqueVarNames $ toClausalForm $ L.foldr (\l r -> con l r) (head formulas) (tail formulas)-    clauseSet = S.fromList clauses+isValid t = isValid' maxClause standardSkolem t -resolve :: Set Clause -> Bool-resolve cls = case S.member C.empty cls of-  True -> False-  False -> resolveIter [cls]+maxClause cs = S.findMax cs -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 C.empty newClauses of-    True -> False-    False -> resolveIter (newClauses:clauseSets)+standardSkolem t = deleteTautologies $ clauseSet   where-    newClauses = generateNewClauses (head clauseSets) (L.foldl S.union S.empty clauseSets)--generateNewClauses :: Set Clause -> Set Clause -> Set Clause-generateNewClauses recent old = deleteTautologies $ newClauses+    formulas = (neg (conclusion t)) : (hypothesis t)+    clauses = L.map (givenClause . S.fromList) $ toClausalForm $ L.foldr (\l r -> con l r) (head formulas) (tail formulas)+    clauseSet = S.fromList clauses+  +isValid' :: (Set Clause -> Clause) -> -- Clause selection+            (Theorem -> Set Clause) -> -- Preprocessor+            Theorem -> Bool+isValid' s p t =+  case S.size clauses == 0 of+   True -> False+   False -> not $ resolve s (S.singleton (s clauses)) (S.delete (s clauses) clauses)   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--uniqueVarNames :: [[Formula]] -> [[Formula]]-uniqueVarNames cls = zipWith attachSuffix cls (L.map show [1..length cls])+    clauses = p t -attachSuffix :: [Formula] -> String -> [Formula]-attachSuffix cls suffix = L.map (addSuffixToVarNames suffix) cls+resolve :: (Set Clause -> Clause) -> Set Clause -> Set Clause -> Bool+resolve s axioms cls = case S.member C.empty axioms ||+                            S.member C.empty cls of+  True -> False+  False -> case S.size cls == 0 of+    True -> True+    False ->+      let c = s cls+          newClauses = genNewClauses c axioms in+       resolve s (S.insert c axioms) (S.delete c $ S.union newClauses cls) -addSuffixToVarNames :: String -> Formula -> Formula-addSuffixToVarNames suffix form = applyToTerms form (appendVarName suffix)+genNewClauses c cls =+  S.fold S.union S.empty $ S.map (\x -> S.union (resolvedClauses c x) (resolvedClauses x c)) (S.delete c cls)

@@ -1,7 +1,8 @@ module Folly.Unification(Unifier,                          applyUnifier,                          mostGeneralUnifier,-                         unifier) where+                         unifier,+                         uniqueVarSub) where  import Control.Monad import Data.List as L@@ -12,6 +13,19 @@  type Unifier = Map Term Term +uniqueVarSub :: [Term] -> [Term] -> Unifier+uniqueVarSub lt rt =+  let overlappingNames = L.intersect lt rt in+   case overlappingNames of+    [] -> M.empty+    _ -> M.fromList $ L.zip overlappingNames (genUniqueVars (L.length overlappingNames) (lt ++ rt))++genUniqueVars n exclude =+  let excludedNames = L.reverse $ L.sort $ L.map varName exclude+      prefixes = L.replicate n $ L.head excludedNames+      newNames = L.zipWith (\p z -> p ++ show z) prefixes $ [1..n] in+   L.map var newNames+    unifier :: [(Term, Term)] -> Unifier unifier subs = M.fromList subs