module Folly.Resolution(isValid) where import Data.List as L import Data.Set as S import Folly.Clause as C import Folly.Formula 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 resolve :: Set Clause -> Bool resolve cls = case S.member C.empty 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 C.empty newClauses of True -> False False -> resolveIter (newClauses:clauseSets) where newClauses = generateNewClauses (head clauseSets) (L.foldl S.union S.empty clauseSets) 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 uniqueVarNames :: [[Formula]] -> [[Formula]] uniqueVarNames cls = zipWith attachSuffix cls (L.map show [1..length cls]) attachSuffix :: [Formula] -> String -> [Formula] attachSuffix cls suffix = L.map (addSuffixToVarNames suffix) cls addSuffixToVarNames :: String -> Formula -> Formula addSuffixToVarNames suffix form = applyToTerms form (appendVarName suffix)