Folly 0.1.2.0 → 0.1.3.0

raw patch · 4 files changed

+25/−5 lines, 4 files

Files

Folly.cabal +1/−1
src/Folly/Formula.hs +15/−0
src/Folly/Resolution.hs +6/−3
src/Main.hs +3/−1

Folly.cabal view

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

src/Folly/Formula.hs view

@@ -12,6 +12,7 @@   toPNF, toSkolemForm, skf,   Clause,   toClausalForm,+  isTautology,   matchingLiterals) where  import Control.Monad@@ -129,6 +130,14 @@ freeVars (N f) = freeVars f freeVars (Q _ v f) = S.delete v (freeVars f) +isAtom :: Formula -> Bool+isAtom (P _ _) = True+isAtom _ = False++stripNegations :: Formula -> Formula+stripNegations (N t) = t+stripNegations f = f+ literalArgs :: Formula -> [Term] literalArgs (P _ a) = a literalArgs (N (P _ a)) = a@@ -289,3 +298,9 @@ splitDis :: Formula -> Clause splitDis (B "|" l r) = (splitDis l) ++ (splitDis r) splitDis f = [f]++isTautology :: Clause -> 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

src/Folly/Resolution.hs view

@@ -10,7 +10,7 @@ import Folly.Unification  isValid :: Theorem -> Bool-isValid t = not $ resolve clauseSet+isValid t = not $ resolve $ deleteTautologies $ clauseSet   where     formulas = (neg (conclusion t)) : (hypothesis t)     clauses = uniqueVarNames $ L.concat $ L.map toClausalForm formulas@@ -18,7 +18,7 @@  resolve :: Set Clause -> Bool resolve cls = case S.member [] cls of-  True -> False+  True -> True   False -> resolveIter [cls]  resolveIter :: [Set Clause] -> Bool@@ -34,7 +34,7 @@       _ -> generateNewClauses (head clauseSets) (L.foldl S.union S.empty (tail clauseSets))  generateNewClauses :: Set Clause -> Set Clause -> Set Clause-generateNewClauses recent old = newClauses+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@@ -64,3 +64,6 @@  addSuffixToVarNames :: String -> Formula -> Formula addSuffixToVarNames suffix form = applyToTerms form (appendVarName suffix)++deleteTautologies :: Set Clause -> Set Clause+deleteTautologies clauses = S.filter (not . isTautology) clauses

src/Main.hs view

@@ -20,6 +20,8 @@     Failed errMsg -> putStrLn errMsg     Succeeded t -> do       putStr $ show t-      putStrLn $ "\n\nis " ++ (show $ isValid t)+      case isValid t of+        True -> putStrLn "\n\nIs Valid"+        False -> putStrLn "\n\nIs not valid"  processTheoremFile thmFileContents = (lexer thmFileContents) >>= parseTheorem