123 lines
No EOL
5.7 KiB
Haskell
123 lines
No EOL
5.7 KiB
Haskell
module Resolution where
|
|
import Data.Set (Set)
|
|
import qualified Data.Set as Set
|
|
import FOLSyntax
|
|
( Formula(Exists, Pred, Neg, Conj, Disj, Impl, All),
|
|
Term(..),
|
|
formulaVars,
|
|
termFreeVars,
|
|
termSubst,
|
|
findFresh )
|
|
import Data.List.Extra ( intersect )
|
|
import Data.Maybe ( mapMaybe )
|
|
|
|
type CNF = Set Clause
|
|
type Clause = Set Literal
|
|
type Literal = Formula
|
|
type Unifier = [(Term, Term)]
|
|
|
|
-- unification algorithm of martelli montanari
|
|
unify :: [(Term, Term)] -> Maybe [(Term, Term)]
|
|
unify [] = Just []
|
|
-- (delete)
|
|
unify ((Var x, Var y) : rest) | x == y = unify rest
|
|
-- (decomp)
|
|
unify ((Fun f es, Fun g ds) : rest) | f == g && length es == length ds = unify $ zip es ds ++ rest
|
|
-- (conflict)
|
|
unify ((Fun _ _, Fun _ _) : _) = Nothing
|
|
-- (orient)
|
|
unify ((Fun f ts, Var x) : rest) = unify $ (Var x, Fun f ts) : rest
|
|
-- (occurs)
|
|
unify ((Var x, t) : _) | x `elem` termFreeVars t && Var x /= t = Nothing
|
|
-- (elim)
|
|
unify ((Var x, t) : rest) | notElem x (termFreeVars t) && x `elem` concatMap (\(t1, t2) -> termFreeVars t1 ++ termFreeVars t2) rest = unify $ (Var x, t) : map (\(t1, t2) -> (termSubst t1 x t, termSubst t2 x t)) rest
|
|
-- decent
|
|
unify ((t, s) : rest) = do
|
|
rest' <- unify rest
|
|
return $ (t, s) : rest'
|
|
|
|
-- unifies predicates, e.g. P(x,y) == P(f(a), z)
|
|
unifyPredicates :: Literal -> Literal -> Maybe Unifier
|
|
unifyPredicates (Pred p1 ts1) (Neg (Pred p2 ts2)) | p1 == p2 && length p1 == length p2 = unify $ zip ts1 ts2
|
|
unifyPredicates _ _ = Nothing
|
|
|
|
setConcat :: Ord a => [Set a] -> Set a
|
|
setConcat = foldr Set.union Set.empty
|
|
|
|
-- a single resolution step as described in gloin
|
|
resolveStep :: CNF -> Either () CNF
|
|
resolveStep clauses = if Set.empty `Set.member` clauses then Left () else Right $ clauses `Set.union` newClauses
|
|
where
|
|
-- rename all variables
|
|
zippedClauses = [(c1, c2) | c1 <- Set.toList clauses, c2 <- Set.toList clauses, c1 /= c2]
|
|
newClauses = setConcat $ map (uncurry resolveClauses) zippedClauses
|
|
|
|
-- applies an mgu to a given formula, asserts that the formula contains no quantifiers
|
|
applyMgu :: Formula -> [(Term, Term)] -> Formula
|
|
applyMgu (Pred p ts) mgu = Pred p $ map (`applyMguTerm` mgu) ts
|
|
applyMgu (Neg f) mgu = Neg $ applyMgu f mgu
|
|
applyMgu (Conj f1 f2) mgu = Conj (applyMgu f1 mgu) (applyMgu f2 mgu)
|
|
applyMgu (Disj f1 f2) mgu = Disj (applyMgu f1 mgu) (applyMgu f2 mgu)
|
|
applyMgu (Impl f1 f2) mgu = Impl (applyMgu f1 mgu) (applyMgu f2 mgu)
|
|
applyMgu f _ = f
|
|
-- applies mgu to term
|
|
applyMguTerm :: Term -> [(Term, Term)] -> Term
|
|
applyMguTerm (Var x) [] = Var x
|
|
applyMguTerm (Var x) ((Var y, t) : rest) = if x == y then t else applyMguTerm (Var x) rest
|
|
applyMguTerm (Fun f ts) mgu = Fun f $ map (`applyMguTerm` mgu) ts
|
|
applyMguTerm t _ = t
|
|
|
|
-- takes two clauses and makes the variables these clauses disjunct
|
|
makeVariablesDisjunct :: Clause -> Clause -> (Clause, Clause)
|
|
makeVariablesDisjunct c1 c2 = (c1', c2')
|
|
where
|
|
(used, c1') = makeClauseDisjunct [] c1
|
|
(_, c2') = makeClauseDisjunct used c2
|
|
-- takes a list of variable names and ensures that the clause does not contain these variables (by renaming), then returns all variables used in the clause + used before
|
|
makeClauseDisjunct :: [String] -> Clause -> ([String], Clause)
|
|
makeClauseDisjunct used clause = (concatMap formulaVars newClause ++ newUsed, newClause)
|
|
where
|
|
criticalVars = used `intersect` concatMap formulaVars clause
|
|
(newUsed, newClause) = foldr foldFun (used, clause) criticalVars
|
|
where
|
|
foldFun oldVar (used', clause') = (v' : used', Set.map (\f -> renameFormula f oldVar v') clause')
|
|
where
|
|
v' = findFresh used'
|
|
|
|
-- renames all occurences of variable v with v' in a term
|
|
renameTerm :: Term -> String -> String -> Term
|
|
renameTerm t@(Var x) v v' = if x == v then Var v' else t
|
|
renameTerm (Fun g ts) v v' = Fun g (map (\t -> renameTerm t v v') ts)
|
|
|
|
-- renames all occurences of free variable v with v' in a formula
|
|
renameFormula :: Formula -> String -> String -> Formula
|
|
renameFormula (Pred p ts) v v' = Pred p (map (\t -> renameTerm t v v') ts)
|
|
renameFormula (Neg f') v v' = Neg $ renameFormula f' v v'
|
|
renameFormula (Conj f1 f2) v v' = Conj (renameFormula f1 v v') (renameFormula f2 v v')
|
|
renameFormula (Disj f1 f2) v v' = Disj (renameFormula f1 v v') (renameFormula f2 v v')
|
|
renameFormula (Impl f1 f2) v v' = Impl (renameFormula f1 v v') (renameFormula f2 v v')
|
|
renameFormula (All y f') v v' | y /= v = All y $ renameFormula f' v v'
|
|
renameFormula (Exists y f') v v' | y /= v = Exists y $ renameFormula f' v v'
|
|
renameFormula f' _ _ = f'
|
|
|
|
-- takes two clauses and tries to unify every literal in a crossproduct, returns the set of all clauses resulting from this resolution step
|
|
resolveClauses :: Clause -> Clause -> Set Clause
|
|
resolveClauses c1 c2 = Set.fromList newClauses
|
|
where
|
|
-- first make variables in both clauses disjunct
|
|
(c1', c2') = makeVariablesDisjunct c1 c2
|
|
zippedLiterals = [(lit1, lit2) | lit1 <- Set.toList c1', lit2 <- Set.toList c2']
|
|
newClauses = concat $ mapMaybe (\(l1, l2) -> do
|
|
-- first calculate mgu
|
|
mgu <- unifyPredicates l1 l2
|
|
-- now apply mgu to clauses without l1 and l2
|
|
let c1'' = Set.map (`applyMgu` mgu) (c1' `Set.difference` Set.singleton l1)
|
|
let c2'' = Set.map (`applyMgu` mgu) (c2' `Set.difference` Set.singleton l2)
|
|
return [c1'', c2'']
|
|
) zippedLiterals
|
|
|
|
-- do resolution until we have proven unfulfillability of formula set
|
|
doResolution :: CNF -> Either () CNF
|
|
doResolution f = do
|
|
f' <- resolveStep f
|
|
doResolution f' |