-- | Resolution. -- -- Copyright (c) 2003-2007, John Harrison. (See "LICENSE.txt" for details.) {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE QuasiQuotes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# OPTIONS_GHC -Wall #-} module Data.Logic.ATP.Resolution ( match_atoms , match_atoms_eq , resolution1 , resolution2 , resolution3 , presolution -- , matchAtomsEq , davis_putnam_example_formula , testResolution ) where import Control.Monad.State (execStateT, get, StateT) import Data.List as List (map) import Data.Logic.ATP.Apply (HasApply(TermOf), JustApply, pApp, zipApplys) import Data.Logic.ATP.Equate (HasEquate, zipEquates) import Data.Logic.ATP.FOL (generalize, IsFirstOrder, lsubst, var) import Data.Logic.ATP.Formulas (IsFormula(AtomOf)) import Data.Logic.ATP.Lib (allpairs, allsubsets, allnonemptysubsets, apply, defined, Failing(..), failing, (|->), setAll, setAny, settryfind) import Data.Logic.ATP.Lit ((.~.), IsLiteral, JustLiteral, LFormula, positive, zipLiterals') import Data.Logic.ATP.Pretty (assertEqual', Pretty, prettyShow) import Data.Logic.ATP.Prop ((.|.), (.&.), (.=>.), (.<=>.), list_conj, PFormula, simpcnf, trivial) import Data.Logic.ATP.Quantified (exists, for_all, IsQuantified(VarOf)) import Data.Logic.ATP.Parser (fof) import Data.Logic.ATP.Skolem (askolemize, Formula, Function(Skolem), HasSkolem(SVarOf), pnf, runSkolem, simpdnf', SkAtom, skolemize, SkolemT, specialize, SkTerm) import Data.Logic.ATP.Term (fApp, foldTerm, IsTerm(FunOf, TVarOf), prefix, V, vt) import Data.Logic.ATP.Unif (solve, Unify(UTermOf), unify_literals) import Data.Map.Strict as Map import Data.Maybe (fromMaybe) import Data.Set as Set import Data.String (fromString) import Test.HUnit -- | Barber's paradox is an example of why we need factoring. test01 :: Test test01 = TestCase $ assertEqual ("Barber's paradox: " ++ prettyShow barb ++ " (p. 181)") (prettyShow expected) (prettyShow input) where shaves = pApp "shaves" :: [SkTerm] -> Formula [b, x] = [vt "b", vt "x"] :: [SkTerm] fx = fApp (Skolem "x" 1) :: [SkTerm] -> SkTerm barb = exists "b" (for_all "x" (shaves [b, x] .<=>. (.~.)(shaves [x, x]))) :: Formula input :: Set (Set (LFormula SkAtom)) input = simpcnf id (runSkolem (skolemize id ((.~.)barb)) :: PFormula SkAtom) -- This is not exactly what is in the book expected :: Set (Set Formula) expected = Set.fromList [Set.fromList [shaves [b, fx [b]], (.~.)(shaves [fx [b],fx [b]])], Set.fromList [shaves [fx [b],fx [b]], (.~.)(shaves [b, fx [b]])]] -- x = vt (fromString "x") -- b = vt (fromString "b") -- fx = fApp (Skolem "x" 1) -- | MGU of a set of literals. mgu :: forall lit atom term v. (JustLiteral lit, HasApply atom, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), IsTerm term, atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => Set lit -> StateT (Map v term) Failing (Map v term) mgu l = case Set.minView l of Just (a, rest) -> case Set.minView rest of Just (b, _) -> unify_literals a b >> mgu rest _ -> solve <$> get _ -> solve <$> get unifiable :: forall lit term atom v. (JustLiteral lit, IsTerm term, HasApply atom, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => lit -> lit -> Bool unifiable p q = failing (const False) (const True) (execStateT (unify_literals p q) Map.empty :: Failing (Map v term)) -- ------------------------------------------------------------------------- -- Rename a clause. -- ------------------------------------------------------------------------- rename :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => (v -> v) -> Set lit -> Set lit rename pfx cls = Set.map (lsubst (Map.fromList (Set.toList (Set.map (\v -> (v, (vt (pfx v)))) fvs)))) cls where fvs = Set.fold Set.union Set.empty (Set.map var cls) -- ------------------------------------------------------------------------- -- General resolution rule, incorporating factoring as in Robinson's paper. -- ------------------------------------------------------------------------- resolvents :: (JustLiteral lit, Ord lit, HasApply atom, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), IsTerm term, atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => Set lit -> Set lit -> lit -> Set lit -> Set lit resolvents cl1 cl2 p acc = if Set.null ps2 then acc else Set.fold doPair acc pairs where doPair (s1,s2) sof = case execStateT (mgu (Set.union s1 (Set.map (.~.) s2))) Map.empty of Success mp -> Set.union (Set.map (lsubst mp) (Set.union (Set.difference cl1 s1) (Set.difference cl2 s2))) sof Failure _ -> sof -- pairs :: Set (Set fof, Set fof) pairs = allpairs (,) (Set.map (Set.insert p) (allsubsets ps1)) (allnonemptysubsets ps2) -- ps1 :: Set fof ps1 = Set.filter (\ q -> q /= p && unifiable p q) cl1 -- ps2 :: Set fof ps2 = Set.filter (unifiable ((.~.) p)) cl2 resolve_clauses :: (JustLiteral lit, Ord lit, HasApply atom, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), IsTerm term, atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => Set lit -> Set lit -> Set lit resolve_clauses cls1 cls2 = let cls1' = rename (prefix "x") cls1 cls2' = rename (prefix "y") cls2 in Set.fold (resolvents cls1' cls2') Set.empty cls1' -- ------------------------------------------------------------------------- -- Basic "Argonne" loop. -- ------------------------------------------------------------------------- resloop1 :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => Set (Set lit) -> Set (Set lit) -> Failing Bool resloop1 used unused = maybe (Failure ["No proof found"]) step (Set.minView unused) where step (cl, ros) = if Set.member Set.empty news then return True else resloop1 used' (Set.union ros news) where used' = Set.insert cl used -- resolve_clauses is not in the Failing monad, so setmapfilter isn't appropriate. news = Set.fold Set.insert Set.empty ({-setmapfilter-} Set.map (resolve_clauses cl) used') pure_resolution1 :: forall fof atom term v. (atom ~ AtomOf fof, term ~ TermOf atom, v ~ TVarOf term, IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Ord fof, Pretty fof ) => fof -> Failing Bool pure_resolution1 fm = resloop1 Set.empty (simpcnf id (specialize id (pnf fm) :: PFormula atom) :: Set (Set (LFormula atom))) resolution1 :: forall m fof atom term v function. (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Ord fof, HasSkolem function, Monad m, atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => fof -> SkolemT m function (Set (Failing Bool)) resolution1 fm = askolemize ((.~.)(generalize fm)) >>= return . Set.map (pure_resolution1 . list_conj) . (simpdnf' :: fof -> Set (Set fof)) -- | Simple example that works well. davis_putnam_example_formula :: Formula davis_putnam_example_formula = [fof| ∃ x y. (∀ z. ((F(x,y)⇒F(y,z)∧F(z,z))∧(F(x,y)∧G(x,y)⇒G(x,z)∧G(z,z)))) |] {- exists "x" . exists "y" .for_all "z" $ (f [x, y] .=>. (f [y, z] .&. f [z, z])) .&. ((f [x, y] .&. g [x, y]) .=>. (g [x, z] .&. g [z, z])) where [x, y, z] = [vt "x", vt "y", vt "z"] :: [SkTerm] [g, f] = [pApp "G", pApp "F"] :: [[SkTerm] -> Formula] -} test02 :: Test test02 = TestCase $ assertEqual "Davis-Putnam example 1" expected (runSkolem (resolution1 davis_putnam_example_formula)) where expected = Set.singleton (Success True) -- ------------------------------------------------------------------------- -- Matching of terms and literals. -- ------------------------------------------------------------------------- class Match a v term where match :: Map v term -> a -> Failing (Map v term) match_terms :: forall term v. (IsTerm term, v ~ TVarOf term) => Map v term -> [(term, term)] -> Failing (Map v term) match_terms env [] = Success env match_terms env ((p, q) : oth) = foldTerm vr fn p where vr x | not (defined env x) = match_terms ((x |-> q) env) oth | apply env x == Just q = match_terms env oth | otherwise = fail "match_terms" fn f fa = foldTerm vr' fn' q where fn' g ga | f == g && length fa == length ga = match_terms env (zip fa ga ++ oth) fn' _ _ = fail "match_terms" vr' _ = fail "match_terms" match_atoms :: (JustApply atom, IsTerm term, term ~ TermOf atom, v ~ TVarOf term) => Map v term -> (atom, atom) -> Failing (Map v term) match_atoms env (a1, a2) = maybe (Failure ["match_atoms"]) id (zipApplys (\_ pairs -> Just (match_terms env pairs)) a1 a2) match_atoms_eq :: (HasEquate atom, IsTerm term, term ~ TermOf atom, v ~ TVarOf term) => Map v term -> (atom, atom) -> Failing (Map v term) match_atoms_eq env (a1, a2) = maybe (Failure ["match_atoms_eq"]) id (zipEquates (\l1 r1 l2 r2 -> Just (match_terms env [(l1, l2), (r1, r2)])) (\_ pairs -> Just (match_terms env pairs)) a1 a2) match_literals :: forall lit atom term v. (IsLiteral lit, HasApply atom, IsTerm term, Match (atom, atom) v term, atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => Map v term -> lit -> lit -> Failing (Map v term) match_literals env t1 t2 = fromMaybe (fail "match_literals") (zipLiterals' ho ne tf at t1 t2) where ho _ _ = Nothing ne p q = Just $ match_literals env p q tf a b = if a == b then Just (Success env) else Nothing at a1 a2 = Just (match env (a1, a2)) -- | With deletion of tautologies and bi-subsumption with "unused". resolution2 :: forall fof atom term v function m. (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof, atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => fof -> SkolemT m function (Set (Failing Bool)) resolution2 fm = askolemize ((.~.) (generalize fm)) >>= return . Set.map (pure_resolution2 . list_conj) . (simpdnf' :: fof -> Set (Set fof)) pure_resolution2 :: forall fof atom term v. (IsFirstOrder fof, Ord fof, Pretty fof, HasApply atom, IsTerm term, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, atom ~ AtomOf fof, term ~ TermOf atom, v ~ TVarOf term) => fof -> Failing Bool pure_resolution2 fm = resloop2 Set.empty (simpcnf id (specialize id (pnf fm) :: PFormula atom) :: Set (Set (LFormula atom))) resloop2 :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => Set (Set lit) -> Set (Set lit) -> Failing Bool resloop2 used unused = case Set.minView unused of Nothing -> Failure ["No proof found"] Just (cl, ros) -> -- print_string(string_of_int(length used) ^ " used; "^ string_of_int(length unused) ^ " unused."); -- print_newline(); let used' = Set.insert cl used in let news = Set.map (resolve_clauses cl) used' in if Set.member Set.empty news then return True else resloop2 used' (Set.fold (incorporate cl) ros news) incorporate :: (atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term, IsLiteral lit, Ord lit, HasApply atom, Match (atom, atom) v term, IsTerm term) => Set lit -> Set lit -> Set (Set lit) -> Set (Set lit) incorporate gcl cl unused = if trivial cl || setAny (\ c -> subsumes_clause c cl) (Set.insert gcl unused) then unused else replace cl unused replace :: (atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term, IsLiteral lit, Ord lit, IsTerm term, HasApply atom, Match (atom, atom) v term) => Set lit -> Set (Set lit) -> Set (Set lit) replace cl st = case Set.minView st of Nothing -> Set.singleton cl Just (c, st') -> if subsumes_clause cl c then Set.insert cl st' else Set.insert c (replace cl st') -- | Test for subsumption subsumes_clause :: (IsLiteral lit, HasApply atom, IsTerm term, Match (atom, atom) v term, atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => Set lit -> Set lit -> Bool subsumes_clause cls1 cls2 = failing (const False) (const True) (subsume Map.empty cls1) where subsume env cls = case Set.minView cls of Nothing -> Success env Just (l1, clt) -> settryfind (\ l2 -> case (match_literals env l1 l2) of Success env' -> subsume env' clt Failure msgs -> Failure msgs) cls2 test03 :: Test test03 = TestCase $ assertEqual' "Davis-Putnam example 2" expected (runSkolem (resolution2 davis_putnam_example_formula)) where expected = Set.singleton (Success True) -- | Positive (P1) resolution. presolution :: forall fof atom term v function m. (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof, Pretty fof, atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => fof -> SkolemT m function (Set (Failing Bool)) presolution fm = askolemize ((.~.) (generalize fm)) >>= return . Set.map (pure_presolution . list_conj) . (simpdnf' :: fof -> Set (Set fof)) pure_presolution :: forall fof atom term v. (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, Ord fof, Pretty fof, atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof, v ~ TVarOf term) => fof -> Failing Bool pure_presolution fm = presloop Set.empty (simpcnf id (specialize id (pnf fm :: fof) :: PFormula atom) :: Set (Set (LFormula atom))) presloop :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Match (atom, atom) v term, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => Set (Set lit) -> Set (Set lit) -> Failing Bool presloop used unused = case Set.minView unused of Nothing -> Failure ["No proof found"] Just (cl, ros) -> -- print_string(string_of_int(length used) ^ " used; "^ string_of_int(length unused) ^ " unused."); -- print_newline(); let used' = Set.insert cl used in let news = Set.map (presolve_clauses cl) used' in if Set.member Set.empty news then Success True else presloop used' (Set.fold (incorporate cl) ros news) presolve_clauses :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => Set lit -> Set lit -> Set lit presolve_clauses cls1 cls2 = if setAll positive cls1 || setAll positive cls2 then resolve_clauses cls1 cls2 else Set.empty -- | Introduce a set-of-support restriction. resolution3 :: forall fof atom term v function m. (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof, atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => fof -> SkolemT m function (Set (Failing Bool)) resolution3 fm = askolemize ((.~.)(generalize fm)) >>= return . Set.map (pure_resolution3 . list_conj) . (simpdnf' :: fof -> Set (Set fof)) pure_resolution3 :: forall fof atom term v. (atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof, v ~ TVarOf term, IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, Ord fof, Pretty fof) => fof -> Failing Bool pure_resolution3 fm = uncurry resloop2 (Set.partition (setAny positive) (simpcnf id (specialize id (pnf fm) :: PFormula atom) :: Set (Set (LFormula atom)))) instance Match (SkAtom, SkAtom) V SkTerm where match = match_atoms_eq gilmore_1 :: Test gilmore_1 = TestCase $ assertEqual "Gilmore 1" expected (runSkolem (resolution3 fm)) where expected = Set.singleton (Success True) fm :: Formula fm = exists "x" . for_all "y" . for_all "z" $ ((f[y] .=>. g[y]) .<=>. f[x]) .&. ((f[y] .=>. h[y]) .<=>. g[x]) .&. (((f[y] .=>. g[y]) .=>. h[y]) .<=>. h[x]) .=>. f[z] .&. g[z] .&. h[z] [x, y, z] = [vt "x", vt "y", vt "z"] :: [SkTerm] [f, g, h] = [pApp "F", pApp "G", pApp "H"] -- The Pelletier examples again. p1 :: Test p1 = let [p, q] = [pApp (fromString "p") [], pApp (fromString "q") []] :: [Formula] in TestCase $ assertEqual "p1" Set.empty (runSkolem (presolution ((p .=>. q .<=>. (.~.)q .=>. (.~.)p) :: Formula))) {- -- ------------------------------------------------------------------------- -- The Pelletier examples again. -- ------------------------------------------------------------------------- {- ********** let p1 = time presolution <
q <=> ~q ==> ~p>>;; let p2 = time presolution <<~ ~p <=> p>>;; let p3 = time presolution <<~(p ==> q) ==> q ==> p>>;; let p4 = time presolution <<~p ==> q <=> ~q ==> p>>;; let p5 = time presolution <<(p \/ q ==> p \/ r) ==> p \/ (q ==> r)>>;; let p6 = time presolution <
>;; let p7 = time presolution <
>;; let p8 = time presolution <<((p ==> q) ==> p) ==> p>>;; let p9 = time presolution <<(p \/ q) /\ (~p \/ q) /\ (p \/ ~q) ==> ~(~q \/ ~q)>>;; let p10 = time presolution <<(q ==> r) /\ (r ==> p /\ q) /\ (p ==> q /\ r) ==> (p <=> q)>>;; let p11 = time presolution <
p>>;; let p12 = time presolution <<((p <=> q) <=> r) <=> (p <=> (q <=> r))>>;; let p13 = time presolution <
(p \/ q) /\ (p \/ r)>>;; let p14 = time presolution <<(p <=> q) <=> (q \/ ~p) /\ (~q \/ p)>>;; let p15 = time presolution <
q <=> ~p \/ q>>;; let p16 = time presolution <<(p ==> q) \/ (q ==> p)>>;; let p17 = time presolution <
r) ==> s <=> (~p \/ q \/ s) /\ (~p \/ ~r \/ s)>>;;
-- -------------------------------------------------------------------------
-- Monadic Predicate Logic.
-- -------------------------------------------------------------------------
let p18 = time presolution
< P(x,z))
==> P(f(a,b),f(a,c))>>;;
-- -------------------------------------------------------------------------
-- See info-hol, circa 1500.
-- -------------------------------------------------------------------------
let p58 = time presolution
< q <=> ~q ==> ~p>>;;
let p2 = time resolution
<<~ ~p <=> p>>;;
let p3 = time resolution
<<~(p ==> q) ==> q ==> p>>;;
let p4 = time resolution
<<~p ==> q <=> ~q ==> p>>;;
let p5 = time resolution
<<(p \/ q ==> p \/ r) ==> p \/ (q ==> r)>>;;
let p6 = time resolution
< >;;
let p7 = time resolution
< >;;
let p8 = time resolution
<<((p ==> q) ==> p) ==> p>>;;
let p9 = time resolution
<<(p \/ q) /\ (~p \/ q) /\ (p \/ ~q) ==> ~(~q \/ ~q)>>;;
let p10 = time resolution
<<(q ==> r) /\ (r ==> p /\ q) /\ (p ==> q /\ r) ==> (p <=> q)>>;;
let p11 = time resolution
< p>>;;
let p12 = time resolution
<<((p <=> q) <=> r) <=> (p <=> (q <=> r))>>;;
let p13 = time resolution
< (p \/ q) /\ (p \/ r)>>;;
let p14 = time resolution
<<(p <=> q) <=> (q \/ ~p) /\ (~q \/ p)>>;;
let p15 = time resolution
< q <=> ~p \/ q>>;;
let p16 = time resolution
<<(p ==> q) \/ (q ==> p)>>;;
let p17 = time resolution
< r) ==> s <=> (~p \/ q \/ s) /\ (~p \/ ~r \/ s)>>;;
(* ------------------------------------------------------------------------- *)
(* Monadic Predicate Logic. *)
(* ------------------------------------------------------------------------- *)
let p18 = time resolution
< P(x,z))
==> P(f(a,b),f(a,c))>>;;
(* ------------------------------------------------------------------------- *)
(* See info-hol, circa 1500. *)
(* ------------------------------------------------------------------------- *)
let p58 = time resolution
<