Folly (empty) → 0.1.0.0

raw patch · 8 files changed

+517/−0 lines, 8 filesdep +HUnitdep +basedep +containerssetup-changed

Dependencies added: HUnit, base, containers, parsec

Files

Folly.cabal +38/−0
LICENSE +30/−0
Setup.hs +2/−0
src/Folly/Formula.hs +283/−0
src/Folly/Resolution.hs +66/−0
src/Folly/Unification.hs +50/−0
src/Folly/Utils.hs +23/−0
src/Main.hs +25/−0

+ Folly.cabal view

@@ -0,0 +1,38 @@+-- Initial Folly.cabal generated by cabal init.  For further documentation,+--  see http://haskell.org/cabal/users-guide/++name:                Folly+version:             0.1.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+		     order logic into other programs as well as an executable+		     theorem prover that uses resolution to prove theorems+		     in first order logic.+license:             BSD3+license-file:        LICENSE+author:              Dillon Huff+maintainer:          Dillon Huff+homepage:	     https://github.com/dillonhuff/Folly+-- copyright:           +-- category:            +build-type:          Simple+cabal-version:       >=1.8++library+  exposed-modules:     Folly.Formula, Folly.Unification, Folly.Resolution, Folly.Utils+  -- other-modules:       +  build-depends:       base < 6, containers+  hs-source-dirs:      src++executable Folly+  main-is:             Main.hs+  -- other-modules:       +  build-depends:       base < 6, containers, parsec+  hs-source-dirs:      src++executable Folly-tests+  main-is:             Main.hs+  -- other-modules:       +  build-depends:       base < 6, HUnit, containers, parsec+  hs-source-dirs:      test, src

+ LICENSE view

@@ -0,0 +1,30 @@+Copyright (c) 2014, Dillon Huff++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Dillon Huff nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

+ Setup.hs view

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

+ src/Folly/Formula.hs view

@@ -0,0 +1,283 @@+module Folly.Formula(+  Term, Formula,+  fvt, subTerm, isVar, isConst, isFunc,+  funcName, funcArgs,+  appendVarName,+  var, func, constant,+  te, fa, pr, con, dis, neg, imp, bic, t, f,+  vars, freeVars,+  generalize, subFormula,+  applyToTerms,+  literalArgs,+  toPNF, toSkolemForm, skf,+  Clause,+  toClausalForm,+  matchingLiterals) where++import Control.Monad+import Data.Set as S+import Data.List as L+import Data.Map as M++data Term =+  Constant String    |+  Var String         |+  Func String [Term]+  deriving (Eq, Ord)+           +instance Show Term where+  show = showTerm+   +showTerm :: Term -> String+showTerm (Constant name) = name+showTerm (Var name) = name+showTerm (Func name args) = name ++ "(" ++ (concat $ intersperse ", " $ L.map showTerm args) ++ ")"++isVar (Var _) = True+isVar _ = False++isFunc (Func _ _) = True+isFunc _ = False++isConst (Constant _) = True+isConst _ = False++funcName (Func n _) = n++funcArgs (Func _ a) = a++var n = Var n+func n args = case (L.take 3 n) == "skl" of+  True -> error $ "Function names beginning with skl are reserved for skolemization"+  False -> Func n args+constant n = Constant n++appendVarName :: String -> Term -> Term+appendVarName suffix (Var n) = Var (n ++ suffix)+appendVarName suffix (Func name args) = Func name $ L.map (appendVarName suffix) args+appendVarName _ t = t++fvt :: Term -> Set Term+fvt (Constant _) = S.empty+fvt (Var n) = S.fromList [(Var n)]+fvt (Func name args) = S.foldl S.union S.empty (S.fromList (L.map fvt args))++subTerm :: Map Term Term -> Term -> Term+subTerm _ (Constant name) = Constant name+subTerm sub (Func name args) = (Func name (L.map (subTerm sub) args))+subTerm sub (Var x) = case M.lookup (Var x) sub of+  Just s -> s+  Nothing -> (Var x)++data Formula =+  T                            | +  F                            |+  P String [Term]              |+  B String Formula Formula     |+  N Formula                    |+  Q String Term Formula+  deriving (Eq, Ord)+           +instance Show Formula where+  show = showFormula+  +showFormula :: Formula -> String+showFormula T = "True"+showFormula F = "False"+showFormula (P predName args) = predName ++ "[" ++ (concat $ intersperse ", " $ L.map showTerm args)  ++ "]"+showFormula (N (P name args)) = "~" ++ show (P name args)+showFormula (N f) = "~(" ++ show f ++ ")"+showFormula (B op f1 f2) = "(" ++ show f1 ++ " " ++ op ++ " "  ++ show f2 ++ ")"+showFormula (Q q t f) = "(" ++ q ++ " "  ++ show t ++ " . " ++ show f ++ ")"++applyToTerms :: Formula -> (Term -> Term) -> Formula+applyToTerms (P n args) f = P n $ L.map f args+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)++te :: Term -> Formula -> Formula+te v@(Var _) f = Q "E" v f+te t _ = error $ "Cannot quantify over non-variable term " ++ show t++fa :: Term -> Formula -> Formula+fa v@(Var _) f = Q "V" v f+fa t _ = error $ "Cannot quantify over non-variable term " ++ show t++pr name args = P name args+con f1 f2 = B "&" f1 f2+dis f1 f2 = B "|" f1 f2+imp f1 f2 = B "->" f1 f2+bic f1 f2 = B "<->" f1 f2+neg f = N f+t = T+f = F++vars :: Formula -> Set Term+vars T = S.empty+vars F = S.empty+vars (P name terms) = S.fold S.union S.empty $ S.fromList (L.map fvt terms)+vars (B _ f1 f2) = S.union (vars f1) (vars f2)+vars (N f) = vars f+vars (Q _ v f) = S.insert v (vars f)++freeVars :: Formula -> Set Term+freeVars T = S.empty+freeVars F = S.empty+freeVars (P name terms) = S.fold S.union S.empty $ S.fromList (L.map fvt terms)+freeVars (B _ f1 f2) = S.union (freeVars f1) (freeVars f2)+freeVars (N f) = freeVars f+freeVars (Q _ v f) = S.delete v (freeVars f)++literalArgs :: Formula -> [Term]+literalArgs (P _ a) = a+literalArgs (N (P _ a)) = a+literalArgs l = error $ show l ++ " is not a literal"++matchingLiterals :: Formula -> Formula -> Bool+matchingLiterals (P n1 _) (N (P n2 _)) = n1 == n2+matchingLiterals (N (P n1 _)) (P n2 _) = n1 == n2+matchingLiterals (P _ _) (P _ _) = False+matchingLiterals (N (P _ _)) (N (P _ _)) = False+matchingLiterals l1 l2 = error $ show l1 ++ " or " ++ show l2 ++ " is not a literal"++generalize :: Formula -> Formula+generalize f = applyList genFreeVar f+  where+    genFreeVar = L.map fa (S.toList (freeVars f))++applyList :: [a -> a] -> a -> a+applyList [] a = a+applyList (f:fs) a = applyList fs (f a)++variant :: Set Term -> Term -> Term+variant vars x@(Var n) = case S.member x vars of+  True -> variant vars (Var (n ++ "'"))+  False -> x+  +subFormula :: Map Term Term -> Formula -> Formula+subFormula subst (P name args) = P name $ L.map (subTerm subst) args+subFormula subst (B op f1 f2) = B op (subFormula subst f1) (subFormula subst f2)+subFormula subst (N f) = N (subFormula subst f)+subFormula subst q@(Q _ _ _) = subQuant subst q+subFormula subst f = f++subQuant :: Map Term Term -> Formula -> Formula+subQuant subst (Q n v f) = case (M.filter (== v) subst) == M.empty of+  True -> Q n v (subFormula subst f)+  False -> Q n vNew $ subFormula (M.insert v vNew subst) f+  where+    vNew = variant (freeVars (subFormula (M.delete v subst) f)) v+    +    +toPNF :: Formula -> Formula+toPNF = (transformFormula pullQuantifiers) .+        (transformFormula simplifyFormula) .+        (transformFormula pushNegation) .+        (transformFormula elimVacuousQuantifiers) .+        (transformFormula replaceImp) .+        (transformFormula replaceBic)++pullQuantifiers f@(B "&" (Q "V" x p) (Q "V" y q)) = pullQ True True f fa con x y p q+pullQuantifiers f@(B "|" (Q "E" x p) (Q "E" y q)) = pullQ True True f te dis x y p q+pullQuantifiers f@(B "|" (Q "V" x p) q) = pullQ True False f fa dis x x p q+pullQuantifiers f@(B "|" p (Q "V" y q)) = pullQ False True f fa dis y y p q+pullQuantifiers f@(B "|" (Q "E" x p) q) = pullQ True False f te dis x x p q+pullQuantifiers f@(B "|" p (Q "E" y q)) = pullQ False True f te dis y y p q+pullQuantifiers f@(B "&" (Q "V" x p) q) = pullQ True False f fa con x x p q+pullQuantifiers f@(B "&" p (Q "V" y q)) = pullQ False True f fa con y y p q+pullQuantifiers f@(B "&" (Q "E" x p) q) = pullQ True False f te con x x p q+pullQuantifiers f@(B "&" p (Q "E" y q)) = pullQ False True f te con y y p q+pullQuantifiers f = f++pullQ :: Bool ->+         Bool ->+         Formula ->+         (Term -> Formula -> Formula) ->+         (Formula -> Formula -> Formula) ->+         Term ->+         Term ->+         Formula ->+         Formula ->+         Formula+pullQ l r f quant op x y p q =+  let z = variant (freeVars f) x in+  let ps = if l then subFormula (M.singleton x z) p else p in+  let qs = if r then subFormula (M.singleton y z) q else q in+  quant z (pullQuantifiers $ op ps qs)++simplifyFormula (N (N f)) = f+simplifyFormula (N T) = F+simplifyFormula (N F) = T+simplifyFormula (B "|" T f) = T+simplifyFormula (B "|" f T) = T+simplifyFormula (B "|" F F) = F+simplifyFormula (B "&" F f) = F+simplifyFormula (B "&" f F) = F+simplifyFormula (B "&" T T) = T+simplifyFormula f = f++pushNegation (N (B "|" f1 f2)) = B "&" (pushNegation (N f1)) (pushNegation (N f2))+pushNegation (N (B "&" f1 f2)) = B "|" (pushNegation (N f1)) (pushNegation (N f2))+pushNegation (N (Q "V" x f)) = Q "E" x (pushNegation (N f))+pushNegation (N (Q "E" x f)) = Q "V" x (pushNegation (N f))+pushNegation f = f++elimVacuousQuantifiers (Q n x f) = case S.member x (freeVars f) of+  True -> Q n x f+  False -> f+elimVacuousQuantifiers f = f++replaceImp (B "->" f1 f2) = dis (neg f1) f2+replaceImp f = f++replaceBic (B "<->" f1 f2) = con (imp f1 f2) (imp f2 f1)+replaceBic f = f++transformFormula :: (Formula -> Formula) -> Formula -> Formula+transformFormula tran (B op f1 f2) = tran (B op (transformFormula tran f1) (transformFormula tran f2))+transformFormula tran (Q q x f) = tran (Q q x (transformFormula tran f))+transformFormula tran (N f) = tran (N (transformFormula tran f))+transformFormula tran f = tran f++-- Conversion to Skolem form+toSkolemForm :: Formula -> Formula+toSkolemForm = skolemize . toPNF++skolemize :: Formula -> Formula+skolemize f = (transformFormula removeExistential) $ replaceVarsWithSkolemFuncs f++removeExistential :: Formula -> Formula+removeExistential (Q "E" v f) = f+removeExistential f = f++replaceVarsWithSkolemFuncs :: Formula -> Formula+replaceVarsWithSkolemFuncs f = subFormula varsToSkolemFuncs f+  where+    varsToSkolemFuncs = collectSkolemFuncs f 0 []+    +collectSkolemFuncs :: Formula -> Int -> [Term] -> Map Term Term+collectSkolemFuncs (Q "E" v f) n vars = M.insert v (skf n vars) (collectSkolemFuncs f (n+1) vars)+collectSkolemFuncs (Q "V" v f) n vars = collectSkolemFuncs f n (v:vars)+collectSkolemFuncs _ _ _ = M.empty++skf :: Int -> [Term] -> Term+skf n vars = Func ("skl" ++ show n) vars++-- Conversion to clausal form+type Clause = [Formula]++toClausalForm :: Formula -> [Clause]+toClausalForm = splitClauses . removeUniversals . toSkolemForm++removeUniversals :: Formula -> Formula+removeUniversals (Q "V" v f) = removeUniversals f+removeUniversals f = f++splitClauses :: Formula -> [Clause]+splitClauses (B "&" l r) = (splitClauses l) ++ (splitClauses r)+splitClauses f = [splitDis f]++splitDis :: Formula -> Clause+splitDis (B "|" l r) = (splitDis l) ++ (splitDis r)+splitDis f = [f]

+ src/Folly/Resolution.hs view

@@ -0,0 +1,66 @@+module Folly.Resolution(+  isValid) where++import Data.List as L+import Data.Maybe+import Data.Set as S++import Folly.Formula+import Folly.Theorem+import Folly.Unification++isValid :: Theorem -> Bool+isValid t = not $ resolve clauseSet+  where+    formulas = (neg (conclusion t)) : (hypothesis t)+    clauses = uniqueVarNames $ L.concat $ L.map toClausalForm formulas+    clauseSet = S.fromList clauses++resolve :: Set Clause -> Bool+resolve cls = case S.member [] cls of+  True -> False+  False -> resolveIter [cls]++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+    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))++generateNewClauses :: Set Clause -> Set Clause -> Set Clause+generateNewClauses recent old = 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 :: Clause -> Clause -> Set Clause+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 -> 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 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++uniqueVarNames :: [Clause] -> [Clause]+uniqueVarNames cls = zipWith attachSuffix cls (L.map show [1..length cls])++attachSuffix :: Clause -> String -> Clause+attachSuffix cls suffix = L.map (addSuffixToVarNames suffix) cls++addSuffixToVarNames :: String -> Formula -> Formula+addSuffixToVarNames suffix form = applyToTerms form (appendVarName suffix)

+ src/Folly/Unification.hs view

@@ -0,0 +1,50 @@+module Folly.Unification(+  applyUnifier,+  mostGeneralUnifier,+  unifier) where++import Control.Monad+import Data.List as L+import Data.Map as M+import Data.Set as S++import Folly.Formula++type Unifier = Map Term Term++unifier :: [(Term, Term)] -> Unifier+unifier subs = M.fromList subs++applyUnifier :: Unifier -> Term -> Term+applyUnifier u t = case possibleSubs u t of+  True -> applyUnifier u (subTerm u t)+  False -> t++possibleSubs :: Unifier -> Term -> Bool+possibleSubs u t = (length $ L.intersect (keys u) (S.toList (fvt t))) /= 0++mostGeneralUnifier :: [(Term, Term)] -> Maybe Unifier+mostGeneralUnifier toUnify = liftM M.fromList $ martelliMontanari toUnify++martelliMontanari :: [(Term, Term)] -> Maybe [(Term, Term)]+martelliMontanari [] = Just []+martelliMontanari ((t1, t2):rest) = case t1 == t2 of+  True -> martelliMontanari rest+  False -> case isVar t1 of+    True -> eliminateVar t1 t2 rest +    False -> case isVar t2 of+      True -> martelliMontanari ((t2, t1):rest)+      False -> case isFunc t1 && isFunc t2 && funcName t1 == funcName t2 of+        True -> martelliMontanari $ (zip (funcArgs t1) (funcArgs t2)) ++ rest+        False -> Nothing++eliminateVar :: Term -> Term -> [(Term, Term)] -> Maybe [(Term, Term)]+eliminateVar var term rest = case S.member var (fvt term) of+  True -> Nothing+  False -> liftM ((:) (var, term)) $ martelliMontanari $ applyToAll (var, term) rest++applyToAll :: (Term, Term) -> [(Term, Term)] -> [(Term, Term)]+applyToAll sub toUnify = L.map applyToPair toUnify+  where+    applyToPair (x, y) = (applyUnifier uni x, applyUnifier uni y)+    uni = unifier [sub]

+ src/Folly/Utils.hs view

@@ -0,0 +1,23 @@+module Folly.Utils(+  Name,+  Error(..), extractValue) where++type Name = String++data Error a =+  Succeeded a |+  Failed String+  deriving (Show)++instance Monad Error where+  return a = Succeeded a+  (Succeeded a) >>= f = f a+  (Failed errMsg) >>= f = (Failed errMsg)++instance Eq a => Eq (Error a) where+  (==) (Succeeded v1) (Succeeded v2) = v1 == v2+  (==) _ _ = False++extractValue :: Error a -> a+extractValue (Succeeded val) = val+extractValue (Failed errMsg) = error $ "Computation Failed: " ++ errMsg

+ src/Main.hs view

@@ -0,0 +1,25 @@+module Main(main) where++import System.Environment+import System.IO++import Folly.Lexer+import Folly.Parser+import Folly.Formula+import Folly.Resolution+import Folly.Theorem+import Folly.Utils++main :: IO ()+main = do+  (fileName:rest) <- getArgs+  fHandle <- openFile fileName ReadMode+  thmString <- hGetContents fHandle+  let thm = processTheoremFile thmString+  case thm of+    Failed errMsg -> putStrLn errMsg+    Succeeded t -> do+      putStr $ show t+      putStrLn $ "\n\nis " ++ (show $ isValid t)++processTheoremFile thmFileContents = (lexer thmFileContents) >>= parseTheorem