-- | 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 :: Test
test01 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> String -> String -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual (String
"Barber's paradox: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Formula -> String
forall a. Pretty a => a -> String
prettyShow Formula
barb String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" (p. 181)")
                    (Set (Set Formula) -> String
forall a. Pretty a => a -> String
prettyShow Set (Set Formula)
expected)
                    (Set (Set (LFormula (FOL Predicate SkTerm))) -> String
forall a. Pretty a => a -> String
prettyShow Set (Set (LFormula (FOL Predicate SkTerm)))
input)
    where shaves :: [SkTerm] -> Formula
shaves = PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
"shaves" :: [SkTerm] -> Formula
          [SkTerm
b, SkTerm
x] = [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"b", TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"x"] :: [SkTerm]
          fx :: [SkTerm] -> SkTerm
fx = FunOf SkTerm -> [SkTerm] -> SkTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp (V -> Int -> Function
Skolem V
"x" Int
1) :: [SkTerm] -> SkTerm
          barb :: Formula
barb = VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"b" (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"x" ([SkTerm] -> Formula
shaves [SkTerm
b, SkTerm
x] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)([SkTerm] -> Formula
shaves [SkTerm
x, SkTerm
x]))) :: Formula
          input :: Set (Set (LFormula SkAtom))
          input :: Set (Set (LFormula (FOL Predicate SkTerm)))
input = (AtomOf (PFormula (FOL Predicate SkTerm))
 -> AtomOf (LFormula (FOL Predicate SkTerm)))
-> PFormula (FOL Predicate SkTerm)
-> Set (Set (LFormula (FOL Predicate SkTerm)))
forall pf lit.
(JustPropositional pf, JustLiteral lit, Ord lit) =>
(AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
simpcnf AtomOf (PFormula (FOL Predicate SkTerm))
-> AtomOf (LFormula (FOL Predicate SkTerm))
FOL Predicate SkTerm -> FOL Predicate SkTerm
forall a. a -> a
id (SkolemT Identity Function (PFormula (FOL Predicate SkTerm))
-> PFormula (FOL Predicate SkTerm)
forall function a.
IsFunction function =>
SkolemT Identity function a -> a
runSkolem ((AtomOf Formula -> AtomOf (PFormula (FOL Predicate SkTerm)))
-> Formula
-> SkolemT Identity Function (PFormula (FOL Predicate SkTerm))
forall formula pf function (m :: * -> *) atom term.
(IsFirstOrder formula, JustPropositional pf, HasSkolem function,
 Monad m, atom ~ AtomOf formula, term ~ TermOf atom,
 function ~ FunOf term, VarOf formula ~ SVarOf function) =>
(AtomOf formula -> AtomOf pf)
-> formula -> StateT (SkolemState function) m pf
skolemize AtomOf Formula -> AtomOf (PFormula (FOL Predicate SkTerm))
FOL Predicate SkTerm -> FOL Predicate SkTerm
forall a. a -> a
id (Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)Formula
barb)) :: PFormula SkAtom)
          -- This is not exactly what is in the book
          expected :: Set (Set Formula)
          expected :: Set (Set Formula)
expected = [Set Formula] -> Set (Set Formula)
forall a. Ord a => [a] -> Set a
Set.fromList [[Formula] -> Set Formula
forall a. Ord a => [a] -> Set a
Set.fromList [[SkTerm] -> Formula
shaves [SkTerm
b,     [SkTerm] -> SkTerm
fx [SkTerm
b]], Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)([SkTerm] -> Formula
shaves [[SkTerm] -> SkTerm
fx [SkTerm
b],[SkTerm] -> SkTerm
fx [SkTerm
b]])],
                                   [Formula] -> Set Formula
forall a. Ord a => [a] -> Set a
Set.fromList [[SkTerm] -> Formula
shaves [[SkTerm] -> SkTerm
fx [SkTerm
b],[SkTerm] -> SkTerm
fx [SkTerm
b]], Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)([SkTerm] -> Formula
shaves [SkTerm
b,     [SkTerm] -> SkTerm
fx [SkTerm
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 :: 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 Set lit
l =
    case Set lit -> Maybe (lit, Set lit)
forall a. Set a -> Maybe (a, Set a)
Set.minView Set lit
l of
      Just (lit
a, Set lit
rest) ->
          case Set lit -> Maybe (lit, Set lit)
forall a. Set a -> Maybe (a, Set a)
Set.minView Set lit
rest of
            Just (lit
b, Set lit
_) -> lit -> lit -> StateT (Map v term) Failing ()
forall lit1 lit2 atom1 atom2 v term (m :: * -> *).
(IsLiteral lit1, HasApply atom1, atom1 ~ AtomOf lit1,
 term ~ TermOf atom1, JustLiteral lit2, HasApply atom2,
 atom2 ~ AtomOf lit2, term ~ TermOf atom2, Unify m (atom1, atom2),
 term ~ UTermOf (atom1, atom2), v ~ TVarOf term, MonadFail m) =>
lit1 -> lit2 -> StateT (Map v term) m ()
unify_literals lit
a lit
b StateT (Map v term) Failing ()
-> StateT (Map v term) Failing (Map v term)
-> StateT (Map v term) Failing (Map v term)
forall a b.
StateT (Map v term) Failing a
-> StateT (Map v term) Failing b -> StateT (Map v term) Failing b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Set lit -> StateT (Map v term) Failing (Map v term)
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 Set lit
rest
            Maybe (lit, Set lit)
_ -> Map v term -> Map v term
forall term v.
(IsTerm term, v ~ TVarOf term) =>
Map v term -> Map v term
solve (Map v term -> Map v term)
-> StateT (Map v term) Failing (Map v term)
-> StateT (Map v term) Failing (Map v term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT (Map v term) Failing (Map v term)
forall s (m :: * -> *). MonadState s m => m s
get
      Maybe (lit, Set lit)
_ -> Map v term -> Map v term
forall term v.
(IsTerm term, v ~ TVarOf term) =>
Map v term -> Map v term
solve (Map v term -> Map v term)
-> StateT (Map v term) Failing (Map v term)
-> StateT (Map v term) Failing (Map v term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT (Map v term) Failing (Map v term)
forall s (m :: * -> *). MonadState s m => m s
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 :: 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 lit
p lit
q = ([String] -> Bool)
-> (Map v term -> Bool) -> Failing (Map v term) -> Bool
forall b a. ([String] -> b) -> (a -> b) -> Failing a -> b
failing (Bool -> [String] -> Bool
forall a b. a -> b -> a
const Bool
False) (Bool -> Map v term -> Bool
forall a b. a -> b -> a
const Bool
True) (StateT (Map v term) Failing ()
-> Map v term -> Failing (Map v term)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT (lit -> lit -> StateT (Map v term) Failing ()
forall lit1 lit2 atom1 atom2 v term (m :: * -> *).
(IsLiteral lit1, HasApply atom1, atom1 ~ AtomOf lit1,
 term ~ TermOf atom1, JustLiteral lit2, HasApply atom2,
 atom2 ~ AtomOf lit2, term ~ TermOf atom2, Unify m (atom1, atom2),
 term ~ UTermOf (atom1, atom2), v ~ TVarOf term, MonadFail m) =>
lit1 -> lit2 -> StateT (Map v term) m ()
unify_literals lit
p lit
q) Map v term
forall k a. Map k a
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 :: forall lit atom term v.
(JustLiteral lit, Ord lit, HasApply atom, IsTerm term,
 atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
(v -> v) -> Set lit -> Set lit
rename v -> v
pfx Set lit
cls =
    (lit -> lit) -> Set lit -> Set lit
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Map v term -> lit -> lit
forall lit atom term v.
(JustLiteral lit, HasApply atom, IsTerm term, atom ~ AtomOf lit,
 term ~ TermOf atom, v ~ TVarOf term) =>
Map v term -> lit -> lit
lsubst ([(v, term)] -> Map v term
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList (Set (v, term) -> [(v, term)]
forall a. Set a -> [a]
Set.toList ((v -> (v, term)) -> Set v -> Set (v, term)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\v
v -> (v
v, (TVarOf term -> term
forall term. IsTerm term => TVarOf term -> term
vt (v -> v
pfx v
v)))) Set v
fvs)))) Set lit
cls
    where
      fvs :: Set v
fvs = (Set v -> Set v -> Set v) -> Set v -> Set (Set v) -> Set v
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set v
forall a. Set a
Set.empty ((lit -> Set v) -> Set lit -> Set (Set v)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map lit -> Set v
forall formula atom term v.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula,
 term ~ TermOf atom, v ~ TVarOf term) =>
formula -> Set v
var Set lit
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 :: forall lit atom term v.
(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 Set lit
cl1 Set lit
cl2 lit
p Set lit
acc =
    if Set lit -> Bool
forall a. Set a -> Bool
Set.null Set lit
ps2 then Set lit
acc else ((Set lit, Set lit) -> Set lit -> Set lit)
-> Set lit -> Set (Set lit, Set lit) -> Set lit
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Set lit, Set lit) -> Set lit -> Set lit
doPair Set lit
acc Set (Set lit, Set lit)
pairs
    where
      doPair :: (Set lit, Set lit) -> Set lit -> Set lit
doPair (Set lit
s1,Set lit
s2) Set lit
sof =
          case StateT
  (Map v (UTermOf (atom, atom)))
  Failing
  (Map v (UTermOf (atom, atom)))
-> Map v (UTermOf (atom, atom))
-> Failing (Map v (UTermOf (atom, atom)))
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT (Set lit
-> StateT
     (Map v (UTermOf (atom, atom)))
     Failing
     (Map v (UTermOf (atom, atom)))
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 (Set lit -> Set lit -> Set lit
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set lit
s1 ((lit -> lit) -> Set lit -> Set lit
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map lit -> lit
forall formula. IsLiteral formula => formula -> formula
(.~.) Set lit
s2))) Map v (UTermOf (atom, atom))
forall k a. Map k a
Map.empty of
            Success Map v (UTermOf (atom, atom))
mp -> Set lit -> Set lit -> Set lit
forall a. Ord a => Set a -> Set a -> Set a
Set.union ((lit -> lit) -> Set lit -> Set lit
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Map v (UTermOf (atom, atom)) -> lit -> lit
forall lit atom term v.
(JustLiteral lit, HasApply atom, IsTerm term, atom ~ AtomOf lit,
 term ~ TermOf atom, v ~ TVarOf term) =>
Map v term -> lit -> lit
lsubst Map v (UTermOf (atom, atom))
mp) (Set lit -> Set lit -> Set lit
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Set lit -> Set lit -> Set lit
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set lit
cl1 Set lit
s1) (Set lit -> Set lit -> Set lit
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set lit
cl2 Set lit
s2))) Set lit
sof
            Failure [String]
_ -> Set lit
sof
      -- pairs :: Set (Set fof, Set fof)
      pairs :: Set (Set lit, Set lit)
pairs = (Set lit -> Set lit -> (Set lit, Set lit))
-> Set (Set lit) -> Set (Set lit) -> Set (Set lit, Set lit)
forall a b c (set :: * -> *).
(SetLike set, Ord c) =>
(a -> b -> c) -> set a -> set b -> set c
allpairs (,) ((Set lit -> Set lit) -> Set (Set lit) -> Set (Set lit)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (lit -> Set lit -> Set lit
forall a. Ord a => a -> Set a -> Set a
Set.insert lit
p) (Set lit -> Set (Set lit)
forall a. Ord a => Set a -> Set (Set a)
allsubsets Set lit
ps1)) (Set lit -> Set (Set lit)
forall a. Ord a => Set a -> Set (Set a)
allnonemptysubsets Set lit
ps2)
      -- ps1 :: Set fof
      ps1 :: Set lit
ps1 = (lit -> Bool) -> Set lit -> Set lit
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\ lit
q -> lit
q lit -> lit -> Bool
forall a. Eq a => a -> a -> Bool
/= lit
p Bool -> Bool -> Bool
&& lit -> lit -> Bool
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 lit
p lit
q) Set lit
cl1
      -- ps2 :: Set fof
      ps2 :: Set lit
ps2 = (lit -> Bool) -> Set lit -> Set lit
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (lit -> lit -> Bool
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 (lit -> lit
forall formula. IsLiteral formula => formula -> formula
(.~.) lit
p)) Set lit
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 :: forall lit atom term v.
(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 Set lit
cls1 Set lit
cls2 =
    let cls1' :: Set lit
cls1' = (v -> v) -> Set lit -> Set lit
forall lit atom term v.
(JustLiteral lit, Ord lit, HasApply atom, IsTerm term,
 atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
(v -> v) -> Set lit -> Set lit
rename (String -> v -> v
forall v. IsVariable v => String -> v -> v
prefix String
"x") Set lit
cls1
        cls2' :: Set lit
cls2' = (v -> v) -> Set lit -> Set lit
forall lit atom term v.
(JustLiteral lit, Ord lit, HasApply atom, IsTerm term,
 atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
(v -> v) -> Set lit -> Set lit
rename (String -> v -> v
forall v. IsVariable v => String -> v -> v
prefix String
"y") Set lit
cls2 in
    (lit -> Set lit -> Set lit) -> Set lit -> Set lit -> Set lit
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Set lit -> Set lit -> lit -> Set lit -> Set lit
forall lit atom term v.
(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 Set lit
cls1' Set lit
cls2') Set lit
forall a. Set a
Set.empty Set lit
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 :: forall lit atom term v.
(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 Set (Set lit)
used Set (Set lit)
unused =
    Failing Bool
-> ((Set lit, Set (Set lit)) -> Failing Bool)
-> Maybe (Set lit, Set (Set lit))
-> Failing Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([String] -> Failing Bool
forall a. [String] -> Failing a
Failure [String
"No proof found"]) (Set lit, Set (Set lit)) -> Failing Bool
step (Set (Set lit) -> Maybe (Set lit, Set (Set lit))
forall a. Set a -> Maybe (a, Set a)
Set.minView Set (Set lit)
unused)
    where
      step :: (Set lit, Set (Set lit)) -> Failing Bool
step (Set lit
cl, Set (Set lit)
ros) =
          if Set lit -> Set (Set lit) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Set lit
forall a. Set a
Set.empty Set (Set lit)
news then Bool -> Failing Bool
forall a. a -> Failing a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True else Set (Set lit) -> Set (Set lit) -> Failing Bool
forall lit atom term v.
(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 Set (Set lit)
used' (Set (Set lit) -> Set (Set lit) -> Set (Set lit)
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set (Set lit)
ros Set (Set lit)
news)
          where
            used' :: Set (Set lit)
used' = Set lit -> Set (Set lit) -> Set (Set lit)
forall a. Ord a => a -> Set a -> Set a
Set.insert Set lit
cl Set (Set lit)
used
            -- resolve_clauses is not in the Failing monad, so setmapfilter isn't appropriate.
            news :: Set (Set lit)
news = (Set lit -> Set (Set lit) -> Set (Set lit))
-> Set (Set lit) -> Set (Set lit) -> Set (Set lit)
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold Set lit -> Set (Set lit) -> Set (Set lit)
forall a. Ord a => a -> Set a -> Set a
Set.insert Set (Set lit)
forall a. Set a
Set.empty ({-setmapfilter-} (Set lit -> Set lit) -> Set (Set lit) -> Set (Set lit)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Set lit -> Set lit -> Set lit
forall lit atom term v.
(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 Set lit
cl) Set (Set lit)
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 :: 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 fof
fm = Set (Set (LFormula atom))
-> Set (Set (LFormula atom)) -> Failing Bool
forall lit atom term v.
(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 Set (Set (LFormula atom))
forall a. Set a
Set.empty ((AtomOf (PFormula atom) -> AtomOf (LFormula atom))
-> PFormula atom -> Set (Set (LFormula atom))
forall pf lit.
(JustPropositional pf, JustLiteral lit, Ord lit) =>
(AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
simpcnf atom -> atom
AtomOf (PFormula atom) -> AtomOf (LFormula atom)
forall a. a -> a
id ((AtomOf fof -> AtomOf (PFormula atom)) -> fof -> PFormula atom
forall fof pf.
(IsQuantified fof, JustPropositional pf) =>
(AtomOf fof -> AtomOf pf) -> fof -> pf
specialize atom -> atom
AtomOf fof -> AtomOf (PFormula atom)
forall a. a -> a
id (fof -> fof
forall formula. IsFirstOrder formula => formula -> formula
pnf fof
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 :: 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 fof
fm = fof -> SkolemT m function fof
forall formula function (m :: * -> *) atom term.
(IsFirstOrder formula, HasSkolem function, Monad m,
 atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
 VarOf formula ~ SVarOf function) =>
formula -> SkolemT m function formula
askolemize (fof -> fof
forall formula. IsLiteral formula => formula -> formula
(.~.)(fof -> fof
forall formula. IsFirstOrder formula => formula -> formula
generalize fof
fm)) SkolemT m function fof
-> (fof -> StateT (SkolemState function) m (Set (Failing Bool)))
-> StateT (SkolemState function) m (Set (Failing Bool))
forall a b.
StateT (SkolemState function) m a
-> (a -> StateT (SkolemState function) m b)
-> StateT (SkolemState function) m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Set (Failing Bool)
-> StateT (SkolemState function) m (Set (Failing Bool))
forall a. a -> StateT (SkolemState function) m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Set (Failing Bool)
 -> StateT (SkolemState function) m (Set (Failing Bool)))
-> (fof -> Set (Failing Bool))
-> fof
-> StateT (SkolemState function) m (Set (Failing Bool))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set fof -> Failing Bool) -> Set (Set fof) -> Set (Failing Bool)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (fof -> Failing Bool
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 (fof -> Failing Bool)
-> (Set fof -> fof) -> Set fof -> Failing Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set fof -> fof
forall (t :: * -> *) formula.
(Foldable t, IsFormula formula, IsPropositional formula) =>
t formula -> formula
list_conj) (Set (Set fof) -> Set (Failing Bool))
-> (fof -> Set (Set fof)) -> fof -> Set (Failing Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (fof -> Set (Set fof)
forall fof atom term function v.
(IsFirstOrder fof, Ord fof, atom ~ AtomOf fof, term ~ TermOf atom,
 function ~ FunOf term, v ~ VarOf fof, v ~ TVarOf term) =>
fof -> Set (Set fof)
simpdnf' :: fof -> Set (Set fof))

-- | Simple example that works well.
davis_putnam_example_formula :: Formula
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 :: Test
test02 =
    Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> Set (Failing Bool) -> Set (Failing Bool) -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"Davis-Putnam example 1" Set (Failing Bool)
expected (SkolemT Identity Function (Set (Failing Bool))
-> Set (Failing Bool)
forall function a.
IsFunction function =>
SkolemT Identity function a -> a
runSkolem (Formula -> SkolemT Identity Function (Set (Failing Bool))
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 Formula
davis_putnam_example_formula))
        where
          expected :: Set (Failing Bool)
expected = Failing Bool -> Set (Failing Bool)
forall a. a -> Set a
Set.singleton (Bool -> Failing Bool
forall a. a -> Failing a
Success Bool
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 :: forall term v.
(IsTerm term, v ~ TVarOf term) =>
Map v term -> [(term, term)] -> Failing (Map v term)
match_terms Map v term
env [] = Map v term -> Failing (Map v term)
forall a. a -> Failing a
Success Map v term
env
match_terms Map v term
env ((term
p, term
q) : [(term, term)]
oth) =
    (TVarOf term -> Failing (Map v term))
-> (FunOf term -> [term] -> Failing (Map v term))
-> term
-> Failing (Map v term)
forall term r.
IsTerm term =>
(TVarOf term -> r) -> (FunOf term -> [term] -> r) -> term -> r
forall r.
(TVarOf term -> r) -> (FunOf term -> [term] -> r) -> term -> r
foldTerm v -> Failing (Map v term)
TVarOf term -> Failing (Map v term)
vr FunOf term -> [term] -> Failing (Map v term)
fn term
p
    where
      vr :: v -> Failing (Map v term)
vr v
x | Bool -> Bool
not (Map v term -> v -> Bool
forall t a. Ord t => Map t a -> t -> Bool
defined Map v term
env v
x) = Map v term -> [(term, term)] -> Failing (Map v term)
forall term v.
(IsTerm term, v ~ TVarOf term) =>
Map v term -> [(term, term)] -> Failing (Map v term)
match_terms ((v
x v -> term -> Map v term -> Map v term
forall k a. Ord k => k -> a -> Map k a -> Map k a
|-> term
q) Map v term
env) [(term, term)]
oth
           | Map v term -> v -> Maybe term
forall k a. Ord k => Map k a -> k -> Maybe a
apply Map v term
env v
x Maybe term -> Maybe term -> Bool
forall a. Eq a => a -> a -> Bool
== term -> Maybe term
forall a. a -> Maybe a
Just term
q = Map v term -> [(term, term)] -> Failing (Map v term)
forall term v.
(IsTerm term, v ~ TVarOf term) =>
Map v term -> [(term, term)] -> Failing (Map v term)
match_terms Map v term
env [(term, term)]
oth
           | Bool
otherwise = String -> Failing (Map v term)
forall a. String -> Failing a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"match_terms"
      fn :: FunOf term -> [term] -> Failing (Map v term)
fn FunOf term
f [term]
fa =
          (TVarOf term -> Failing (Map v term))
-> (FunOf term -> [term] -> Failing (Map v term))
-> term
-> Failing (Map v term)
forall term r.
IsTerm term =>
(TVarOf term -> r) -> (FunOf term -> [term] -> r) -> term -> r
forall r.
(TVarOf term -> r) -> (FunOf term -> [term] -> r) -> term -> r
foldTerm v -> Failing (Map v term)
TVarOf term -> Failing (Map v term)
forall {m :: * -> *} {p} {a}. MonadFail m => p -> m a
vr' FunOf term -> [term] -> Failing (Map v term)
fn' term
q
          where
            fn' :: FunOf term -> [term] -> Failing (Map v term)
fn' FunOf term
g [term]
ga | FunOf term
f FunOf term -> FunOf term -> Bool
forall a. Eq a => a -> a -> Bool
== FunOf term
g Bool -> Bool -> Bool
&& [term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [term]
fa Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [term]
ga = Map v term -> [(term, term)] -> Failing (Map v term)
forall term v.
(IsTerm term, v ~ TVarOf term) =>
Map v term -> [(term, term)] -> Failing (Map v term)
match_terms Map v term
env ([term] -> [term] -> [(term, term)]
forall a b. [a] -> [b] -> [(a, b)]
zip [term]
fa [term]
ga [(term, term)] -> [(term, term)] -> [(term, term)]
forall a. [a] -> [a] -> [a]
++ [(term, term)]
oth)
            fn' FunOf term
_ [term]
_ = String -> Failing (Map v term)
forall a. String -> Failing a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"match_terms"
            vr' :: p -> m a
vr' p
_ = String -> m a
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"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 :: forall atom term v.
(JustApply atom, IsTerm term, term ~ TermOf atom,
 v ~ TVarOf term) =>
Map v term -> (atom, atom) -> Failing (Map v term)
match_atoms Map v term
env (atom
a1, atom
a2) =
    Failing (Map v term)
-> (Failing (Map v term) -> Failing (Map v term))
-> Maybe (Failing (Map v term))
-> Failing (Map v term)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([String] -> Failing (Map v term)
forall a. [String] -> Failing a
Failure [String
"match_atoms"]) Failing (Map v term) -> Failing (Map v term)
forall a. a -> a
id ((PredOf atom -> [(term, term)] -> Maybe (Failing (Map v term)))
-> atom -> atom -> Maybe (Failing (Map v term))
forall atom1 term predicate atom2 r.
(JustApply atom1, term ~ TermOf atom1, predicate ~ PredOf atom1,
 JustApply atom2, term ~ TermOf atom2, predicate ~ PredOf atom2) =>
(predicate -> [(term, term)] -> Maybe r)
-> atom1 -> atom2 -> Maybe r
zipApplys (\PredOf atom
_ [(term, term)]
pairs -> Failing (Map v term) -> Maybe (Failing (Map v term))
forall a. a -> Maybe a
Just (Map v term -> [(term, term)] -> Failing (Map v term)
forall term v.
(IsTerm term, v ~ TVarOf term) =>
Map v term -> [(term, term)] -> Failing (Map v term)
match_terms Map v term
env [(term, term)]
pairs)) atom
a1 atom
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 :: forall atom term v.
(HasEquate atom, IsTerm term, term ~ TermOf atom,
 v ~ TVarOf term) =>
Map v term -> (atom, atom) -> Failing (Map v term)
match_atoms_eq Map v term
env (atom
a1, atom
a2) =
    Failing (Map v term)
-> (Failing (Map v term) -> Failing (Map v term))
-> Maybe (Failing (Map v term))
-> Failing (Map v term)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([String] -> Failing (Map v term)
forall a. [String] -> Failing a
Failure [String
"match_atoms_eq"]) Failing (Map v term) -> Failing (Map v term)
forall a. a -> a
id ((TermOf atom
 -> TermOf atom
 -> TermOf atom
 -> TermOf atom
 -> Maybe (Failing (Map v term)))
-> (PredOf atom
    -> [(TermOf atom, TermOf atom)] -> Maybe (Failing (Map v term)))
-> atom
-> atom
-> Maybe (Failing (Map v term))
forall atom1 atom2 r.
(HasEquate atom1, HasEquate atom2, PredOf atom1 ~ PredOf atom2) =>
(TermOf atom1
 -> TermOf atom1 -> TermOf atom2 -> TermOf atom2 -> Maybe r)
-> (PredOf atom1 -> [(TermOf atom1, TermOf atom2)] -> Maybe r)
-> atom1
-> atom2
-> Maybe r
zipEquates (\TermOf atom
l1 TermOf atom
r1 TermOf atom
l2 TermOf atom
r2 -> Failing (Map v term) -> Maybe (Failing (Map v term))
forall a. a -> Maybe a
Just (Map v term -> [(term, term)] -> Failing (Map v term)
forall term v.
(IsTerm term, v ~ TVarOf term) =>
Map v term -> [(term, term)] -> Failing (Map v term)
match_terms Map v term
env [(term
TermOf atom
l1, term
TermOf atom
l2), (term
TermOf atom
r1, term
TermOf atom
r2)]))
                                                      (\PredOf atom
_ [(TermOf atom, TermOf atom)]
pairs -> Failing (Map v term) -> Maybe (Failing (Map v term))
forall a. a -> Maybe a
Just (Map v term -> [(term, term)] -> Failing (Map v term)
forall term v.
(IsTerm term, v ~ TVarOf term) =>
Map v term -> [(term, term)] -> Failing (Map v term)
match_terms Map v term
env [(term, term)]
[(TermOf atom, TermOf atom)]
pairs)) atom
a1 atom
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 :: 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 Map v term
env lit
t1 lit
t2 =
    Failing (Map v term)
-> Maybe (Failing (Map v term)) -> Failing (Map v term)
forall a. a -> Maybe a -> a
fromMaybe (String -> Failing (Map v term)
forall a. String -> Failing a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"match_literals") ((lit -> lit -> Maybe (Failing (Map v term)))
-> (lit -> lit -> Maybe (Failing (Map v term)))
-> (Bool -> Bool -> Maybe (Failing (Map v term)))
-> (AtomOf lit -> AtomOf lit -> Maybe (Failing (Map v term)))
-> lit
-> lit
-> Maybe (Failing (Map v term))
forall lit1 lit2 r.
(IsLiteral lit1, IsLiteral lit2) =>
(lit1 -> lit2 -> Maybe r)
-> (lit1 -> lit2 -> Maybe r)
-> (Bool -> Bool -> Maybe r)
-> (AtomOf lit1 -> AtomOf lit2 -> Maybe r)
-> lit1
-> lit2
-> Maybe r
zipLiterals' lit -> lit -> Maybe (Failing (Map v term))
forall {p} {p} {a}. p -> p -> Maybe a
ho lit -> lit -> Maybe (Failing (Map v term))
ne Bool -> Bool -> Maybe (Failing (Map v term))
tf atom -> atom -> Maybe (Failing (Map v term))
AtomOf lit -> AtomOf lit -> Maybe (Failing (Map v term))
at lit
t1 lit
t2)
    where
      ho :: p -> p -> Maybe a
ho p
_ p
_ = Maybe a
forall a. Maybe a
Nothing
      ne :: lit -> lit -> Maybe (Failing (Map v term))
ne lit
p lit
q = Failing (Map v term) -> Maybe (Failing (Map v term))
forall a. a -> Maybe a
Just (Failing (Map v term) -> Maybe (Failing (Map v term)))
-> Failing (Map v term) -> Maybe (Failing (Map v term))
forall a b. (a -> b) -> a -> b
$ Map v term -> lit -> lit -> Failing (Map v term)
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 Map v term
env lit
p lit
q
      tf :: Bool -> Bool -> Maybe (Failing (Map v term))
tf Bool
a Bool
b = if Bool
a Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
b then Failing (Map v term) -> Maybe (Failing (Map v term))
forall a. a -> Maybe a
Just (Map v term -> Failing (Map v term)
forall a. a -> Failing a
Success Map v term
env) else Maybe (Failing (Map v term))
forall a. Maybe a
Nothing
      at :: atom -> atom -> Maybe (Failing (Map v term))
at atom
a1 atom
a2 = Failing (Map v term) -> Maybe (Failing (Map v term))
forall a. a -> Maybe a
Just (Map v term -> (atom, atom) -> Failing (Map v term)
forall a v term.
Match a v term =>
Map v term -> a -> Failing (Map v term)
match Map v term
env (atom
a1, atom
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 :: 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 fof
fm = fof -> SkolemT m function fof
forall formula function (m :: * -> *) atom term.
(IsFirstOrder formula, HasSkolem function, Monad m,
 atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
 VarOf formula ~ SVarOf function) =>
formula -> SkolemT m function formula
askolemize (fof -> fof
forall formula. IsLiteral formula => formula -> formula
(.~.) (fof -> fof
forall formula. IsFirstOrder formula => formula -> formula
generalize fof
fm)) SkolemT m function fof
-> (fof -> StateT (SkolemState function) m (Set (Failing Bool)))
-> StateT (SkolemState function) m (Set (Failing Bool))
forall a b.
StateT (SkolemState function) m a
-> (a -> StateT (SkolemState function) m b)
-> StateT (SkolemState function) m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Set (Failing Bool)
-> StateT (SkolemState function) m (Set (Failing Bool))
forall a. a -> StateT (SkolemState function) m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Set (Failing Bool)
 -> StateT (SkolemState function) m (Set (Failing Bool)))
-> (fof -> Set (Failing Bool))
-> fof
-> StateT (SkolemState function) m (Set (Failing Bool))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set fof -> Failing Bool) -> Set (Set fof) -> Set (Failing Bool)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (fof -> Failing Bool
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 (fof -> Failing Bool)
-> (Set fof -> fof) -> Set fof -> Failing Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set fof -> fof
forall (t :: * -> *) formula.
(Foldable t, IsFormula formula, IsPropositional formula) =>
t formula -> formula
list_conj) (Set (Set fof) -> Set (Failing Bool))
-> (fof -> Set (Set fof)) -> fof -> Set (Failing Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (fof -> Set (Set fof)
forall fof atom term function v.
(IsFirstOrder fof, Ord fof, atom ~ AtomOf fof, term ~ TermOf atom,
 function ~ FunOf term, v ~ VarOf fof, v ~ TVarOf term) =>
fof -> Set (Set fof)
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 :: 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 fof
fm = Set (Set (LFormula atom))
-> Set (Set (LFormula atom)) -> Failing Bool
forall lit atom term v.
(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 Set (Set (LFormula atom))
forall a. Set a
Set.empty ((AtomOf (PFormula atom) -> AtomOf (LFormula atom))
-> PFormula atom -> Set (Set (LFormula atom))
forall pf lit.
(JustPropositional pf, JustLiteral lit, Ord lit) =>
(AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
simpcnf atom -> atom
AtomOf (PFormula atom) -> AtomOf (LFormula atom)
forall a. a -> a
id ((AtomOf fof -> AtomOf (PFormula atom)) -> fof -> PFormula atom
forall fof pf.
(IsQuantified fof, JustPropositional pf) =>
(AtomOf fof -> AtomOf pf) -> fof -> pf
specialize atom -> atom
AtomOf fof -> AtomOf (PFormula atom)
forall a. a -> a
id (fof -> fof
forall formula. IsFirstOrder formula => formula -> formula
pnf fof
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 :: forall lit atom term v.
(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 Set (Set lit)
used Set (Set lit)
unused =
    case Set (Set lit) -> Maybe (Set lit, Set (Set lit))
forall a. Set a -> Maybe (a, Set a)
Set.minView Set (Set lit)
unused of
      Maybe (Set lit, Set (Set lit))
Nothing -> [String] -> Failing Bool
forall a. [String] -> Failing a
Failure [String
"No proof found"]
      Just (Set lit
cl, Set (Set lit)
ros) ->
          -- print_string(string_of_int(length used) ^ " used; "^ string_of_int(length unused) ^ " unused.");
          -- print_newline();
          let used' :: Set (Set lit)
used' = Set lit -> Set (Set lit) -> Set (Set lit)
forall a. Ord a => a -> Set a -> Set a
Set.insert Set lit
cl Set (Set lit)
used in
          let news :: Set (Set lit)
news = (Set lit -> Set lit) -> Set (Set lit) -> Set (Set lit)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Set lit -> Set lit -> Set lit
forall lit atom term v.
(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 Set lit
cl) Set (Set lit)
used' in
          if Set lit -> Set (Set lit) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Set lit
forall a. Set a
Set.empty Set (Set lit)
news then Bool -> Failing Bool
forall a. a -> Failing a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True else Set (Set lit) -> Set (Set lit) -> Failing Bool
forall lit atom term v.
(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 Set (Set lit)
used' ((Set lit -> Set (Set lit) -> Set (Set lit))
-> Set (Set lit) -> Set (Set lit) -> Set (Set lit)
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Set lit -> Set lit -> Set (Set lit) -> Set (Set lit)
forall atom lit term v.
(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 Set lit
cl) Set (Set lit)
ros Set (Set lit)
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 :: forall atom lit term v.
(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 Set lit
gcl Set lit
cl Set (Set lit)
unused =
    if Set lit -> Bool
forall lit. (Ord lit, IsLiteral lit) => Set lit -> Bool
trivial Set lit
cl Bool -> Bool -> Bool
|| (Set lit -> Bool) -> Set (Set lit) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
setAny (\ Set lit
c -> Set lit -> Set lit -> Bool
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) =>
Set lit -> Set lit -> Bool
subsumes_clause Set lit
c Set lit
cl) (Set lit -> Set (Set lit) -> Set (Set lit)
forall a. Ord a => a -> Set a -> Set a
Set.insert Set lit
gcl Set (Set lit)
unused)
    then Set (Set lit)
unused
    else Set lit -> Set (Set lit) -> Set (Set lit)
forall atom lit term v.
(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 Set lit
cl Set (Set lit)
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 :: forall atom lit term v.
(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 Set lit
cl Set (Set lit)
st =
    case Set (Set lit) -> Maybe (Set lit, Set (Set lit))
forall a. Set a -> Maybe (a, Set a)
Set.minView Set (Set lit)
st of
      Maybe (Set lit, Set (Set lit))
Nothing -> Set lit -> Set (Set lit)
forall a. a -> Set a
Set.singleton Set lit
cl
      Just (Set lit
c, Set (Set lit)
st') -> if Set lit -> Set lit -> Bool
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) =>
Set lit -> Set lit -> Bool
subsumes_clause Set lit
cl Set lit
c
                       then Set lit -> Set (Set lit) -> Set (Set lit)
forall a. Ord a => a -> Set a -> Set a
Set.insert Set lit
cl Set (Set lit)
st'
                       else Set lit -> Set (Set lit) -> Set (Set lit)
forall a. Ord a => a -> Set a -> Set a
Set.insert Set lit
c (Set lit -> Set (Set lit) -> Set (Set lit)
forall atom lit term v.
(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 Set lit
cl Set (Set lit)
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 :: 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) =>
Set lit -> Set lit -> Bool
subsumes_clause Set lit
cls1 Set lit
cls2 =
    ([String] -> Bool)
-> (Map v term -> Bool) -> Failing (Map v term) -> Bool
forall b a. ([String] -> b) -> (a -> b) -> Failing a -> b
failing (Bool -> [String] -> Bool
forall a b. a -> b -> a
const Bool
False) (Bool -> Map v term -> Bool
forall a b. a -> b -> a
const Bool
True) (Map v term -> Set lit -> Failing (Map v term)
subsume Map v term
forall k a. Map k a
Map.empty Set lit
cls1)
    where
      subsume :: Map v term -> Set lit -> Failing (Map v term)
subsume Map v term
env Set lit
cls =
          case Set lit -> Maybe (lit, Set lit)
forall a. Set a -> Maybe (a, Set a)
Set.minView Set lit
cls of
            Maybe (lit, Set lit)
Nothing -> Map v term -> Failing (Map v term)
forall a. a -> Failing a
Success Map v term
env
            Just (lit
l1, Set lit
clt) -> (lit -> Failing (Map v term)) -> Set lit -> Failing (Map v term)
forall t a. (t -> Failing a) -> Set t -> Failing a
settryfind (\ lit
l2 -> case (Map v term -> lit -> lit -> Failing (Map v term)
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 Map v term
env lit
l1 lit
l2) of
                                                    Success Map v term
env' -> Map v term -> Set lit -> Failing (Map v term)
subsume Map v term
env' Set lit
clt
                                                    Failure [String]
msgs -> [String] -> Failing (Map v term)
forall a. [String] -> Failing a
Failure [String]
msgs) Set lit
cls2

test03 :: Test
test03 :: Test
test03 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> Set (Failing Bool) -> Set (Failing Bool) -> Assertion
forall a.
(?loc::CallStack, Eq a, Pretty a) =>
String -> a -> a -> Assertion
assertEqual' String
"Davis-Putnam example 2" Set (Failing Bool)
expected (SkolemT Identity Function (Set (Failing Bool))
-> Set (Failing Bool)
forall function a.
IsFunction function =>
SkolemT Identity function a -> a
runSkolem (Formula -> SkolemT Identity Function (Set (Failing Bool))
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 Formula
davis_putnam_example_formula))
        where
          expected :: Set (Failing Bool)
expected = Failing Bool -> Set (Failing Bool)
forall a. a -> Set a
Set.singleton (Bool -> Failing Bool
forall a. a -> Failing a
Success Bool
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 :: 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 fof
fm =
    fof -> SkolemT m function fof
forall formula function (m :: * -> *) atom term.
(IsFirstOrder formula, HasSkolem function, Monad m,
 atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
 VarOf formula ~ SVarOf function) =>
formula -> SkolemT m function formula
askolemize (fof -> fof
forall formula. IsLiteral formula => formula -> formula
(.~.) (fof -> fof
forall formula. IsFirstOrder formula => formula -> formula
generalize fof
fm)) SkolemT m function fof
-> (fof -> StateT (SkolemState function) m (Set (Failing Bool)))
-> StateT (SkolemState function) m (Set (Failing Bool))
forall a b.
StateT (SkolemState function) m a
-> (a -> StateT (SkolemState function) m b)
-> StateT (SkolemState function) m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Set (Failing Bool)
-> StateT (SkolemState function) m (Set (Failing Bool))
forall a. a -> StateT (SkolemState function) m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Set (Failing Bool)
 -> StateT (SkolemState function) m (Set (Failing Bool)))
-> (fof -> Set (Failing Bool))
-> fof
-> StateT (SkolemState function) m (Set (Failing Bool))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set fof -> Failing Bool) -> Set (Set fof) -> Set (Failing Bool)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (fof -> Failing Bool
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 (fof -> Failing Bool)
-> (Set fof -> fof) -> Set fof -> Failing Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set fof -> fof
forall (t :: * -> *) formula.
(Foldable t, IsFormula formula, IsPropositional formula) =>
t formula -> formula
list_conj) (Set (Set fof) -> Set (Failing Bool))
-> (fof -> Set (Set fof)) -> fof -> Set (Failing Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (fof -> Set (Set fof)
forall fof atom term function v.
(IsFirstOrder fof, Ord fof, atom ~ AtomOf fof, term ~ TermOf atom,
 function ~ FunOf term, v ~ VarOf fof, v ~ TVarOf term) =>
fof -> Set (Set fof)
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 :: 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 fof
fm = Set (Set (LFormula atom))
-> Set (Set (LFormula atom)) -> Failing Bool
forall lit atom term v.
(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 Set (Set (LFormula atom))
forall a. Set a
Set.empty ((AtomOf (PFormula atom) -> AtomOf (LFormula atom))
-> PFormula atom -> Set (Set (LFormula atom))
forall pf lit.
(JustPropositional pf, JustLiteral lit, Ord lit) =>
(AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
simpcnf atom -> atom
AtomOf (PFormula atom) -> AtomOf (LFormula atom)
forall a. a -> a
id ((AtomOf fof -> AtomOf (PFormula atom)) -> fof -> PFormula atom
forall fof pf.
(IsQuantified fof, JustPropositional pf) =>
(AtomOf fof -> AtomOf pf) -> fof -> pf
specialize atom -> atom
AtomOf fof -> AtomOf (PFormula atom)
forall a. a -> a
id (fof -> fof
forall formula. IsFirstOrder formula => formula -> formula
pnf fof
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 :: forall lit atom term v.
(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 Set (Set lit)
used Set (Set lit)
unused =
    case Set (Set lit) -> Maybe (Set lit, Set (Set lit))
forall a. Set a -> Maybe (a, Set a)
Set.minView Set (Set lit)
unused of
      Maybe (Set lit, Set (Set lit))
Nothing -> [String] -> Failing Bool
forall a. [String] -> Failing a
Failure [String
"No proof found"]
      Just (Set lit
cl, Set (Set lit)
ros) ->
          -- print_string(string_of_int(length used) ^ " used; "^ string_of_int(length unused) ^ " unused.");
          -- print_newline();
          let used' :: Set (Set lit)
used' = Set lit -> Set (Set lit) -> Set (Set lit)
forall a. Ord a => a -> Set a -> Set a
Set.insert Set lit
cl Set (Set lit)
used in
          let news :: Set (Set lit)
news = (Set lit -> Set lit) -> Set (Set lit) -> Set (Set lit)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Set lit -> Set lit -> Set lit
forall lit atom term v.
(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 Set lit
cl) Set (Set lit)
used' in
          if Set lit -> Set (Set lit) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Set lit
forall a. Set a
Set.empty Set (Set lit)
news
          then Bool -> Failing Bool
forall a. a -> Failing a
Success Bool
True
          else Set (Set lit) -> Set (Set lit) -> Failing Bool
forall lit atom term v.
(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 Set (Set lit)
used' ((Set lit -> Set (Set lit) -> Set (Set lit))
-> Set (Set lit) -> Set (Set lit) -> Set (Set lit)
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Set lit -> Set lit -> Set (Set lit) -> Set (Set lit)
forall atom lit term v.
(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 Set lit
cl) Set (Set lit)
ros Set (Set lit)
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 :: forall lit atom term v.
(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 Set lit
cls1 Set lit
cls2 =
    if (lit -> Bool) -> Set lit -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
setAll lit -> Bool
forall formula. IsLiteral formula => formula -> Bool
positive Set lit
cls1 Bool -> Bool -> Bool
|| (lit -> Bool) -> Set lit -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
setAll lit -> Bool
forall formula. IsLiteral formula => formula -> Bool
positive Set lit
cls2
    then Set lit -> Set lit -> Set lit
forall lit atom term v.
(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 Set lit
cls1 Set lit
cls2
    else Set lit
forall a. Set a
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 :: 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 fof
fm =
    fof -> SkolemT m function fof
forall formula function (m :: * -> *) atom term.
(IsFirstOrder formula, HasSkolem function, Monad m,
 atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
 VarOf formula ~ SVarOf function) =>
formula -> SkolemT m function formula
askolemize (fof -> fof
forall formula. IsLiteral formula => formula -> formula
(.~.)(fof -> fof
forall formula. IsFirstOrder formula => formula -> formula
generalize fof
fm)) SkolemT m function fof
-> (fof -> StateT (SkolemState function) m (Set (Failing Bool)))
-> StateT (SkolemState function) m (Set (Failing Bool))
forall a b.
StateT (SkolemState function) m a
-> (a -> StateT (SkolemState function) m b)
-> StateT (SkolemState function) m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Set (Failing Bool)
-> StateT (SkolemState function) m (Set (Failing Bool))
forall a. a -> StateT (SkolemState function) m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Set (Failing Bool)
 -> StateT (SkolemState function) m (Set (Failing Bool)))
-> (fof -> Set (Failing Bool))
-> fof
-> StateT (SkolemState function) m (Set (Failing Bool))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set fof -> Failing Bool) -> Set (Set fof) -> Set (Failing Bool)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (fof -> Failing Bool
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 (fof -> Failing Bool)
-> (Set fof -> fof) -> Set fof -> Failing Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set fof -> fof
forall (t :: * -> *) formula.
(Foldable t, IsFormula formula, IsPropositional formula) =>
t formula -> formula
list_conj) (Set (Set fof) -> Set (Failing Bool))
-> (fof -> Set (Set fof)) -> fof -> Set (Failing Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (fof -> Set (Set fof)
forall fof atom term function v.
(IsFirstOrder fof, Ord fof, atom ~ AtomOf fof, term ~ TermOf atom,
 function ~ FunOf term, v ~ VarOf fof, v ~ TVarOf term) =>
fof -> Set (Set fof)
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 :: 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 fof
fm =
    (Set (Set (LFormula atom))
 -> Set (Set (LFormula atom)) -> Failing Bool)
-> (Set (Set (LFormula atom)), Set (Set (LFormula atom)))
-> Failing Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Set (Set (LFormula atom))
-> Set (Set (LFormula atom)) -> Failing Bool
forall lit atom term v.
(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 ((Set (LFormula atom) -> Bool)
-> Set (Set (LFormula atom))
-> (Set (Set (LFormula atom)), Set (Set (LFormula atom)))
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition ((LFormula atom -> Bool) -> Set (LFormula atom) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
setAny LFormula atom -> Bool
forall formula. IsLiteral formula => formula -> Bool
positive) ((AtomOf (PFormula atom) -> AtomOf (LFormula atom))
-> PFormula atom -> Set (Set (LFormula atom))
forall pf lit.
(JustPropositional pf, JustLiteral lit, Ord lit) =>
(AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
simpcnf atom -> atom
AtomOf (PFormula atom) -> AtomOf (LFormula atom)
forall a. a -> a
id ((AtomOf fof -> AtomOf (PFormula atom)) -> fof -> PFormula atom
forall fof pf.
(IsQuantified fof, JustPropositional pf) =>
(AtomOf fof -> AtomOf pf) -> fof -> pf
specialize atom -> atom
AtomOf fof -> AtomOf (PFormula atom)
forall a. a -> a
id (fof -> fof
forall formula. IsFirstOrder formula => formula -> formula
pnf fof
fm) :: PFormula atom) :: Set (Set (LFormula atom))))

instance Match (SkAtom, SkAtom) V SkTerm where
    match :: Map V SkTerm
-> (FOL Predicate SkTerm, FOL Predicate SkTerm)
-> Failing (Map V SkTerm)
match = Map V SkTerm
-> (FOL Predicate SkTerm, FOL Predicate SkTerm)
-> Failing (Map V SkTerm)
forall atom term v.
(HasEquate atom, IsTerm term, term ~ TermOf atom,
 v ~ TVarOf term) =>
Map v term -> (atom, atom) -> Failing (Map v term)
match_atoms_eq


gilmore_1 :: Test
gilmore_1 :: Test
gilmore_1 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> Set (Failing Bool) -> Set (Failing Bool) -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"Gilmore 1" Set (Failing Bool)
expected (SkolemT Identity Function (Set (Failing Bool))
-> Set (Failing Bool)
forall function a.
IsFunction function =>
SkolemT Identity function a -> a
runSkolem (Formula -> SkolemT Identity Function (Set (Failing Bool))
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 Formula
fm))
    where
      expected :: Set (Failing Bool)
expected = Failing Bool -> Set (Failing Bool)
forall a. a -> Set a
Set.singleton (Bool -> Failing Bool
forall a. a -> Failing a
Success Bool
True)
      fm :: Formula
      fm :: Formula
fm = VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"x" (Formula -> Formula) -> (Formula -> Formula) -> Formula -> Formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"y" (Formula -> Formula) -> (Formula -> Formula) -> Formula -> Formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"z" (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$
           (([TermOf (AtomOf Formula)] -> Formula
f[SkTerm
TermOf (AtomOf Formula)
y] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. [TermOf (AtomOf Formula)] -> Formula
g[SkTerm
TermOf (AtomOf Formula)
y]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. [TermOf (AtomOf Formula)] -> Formula
f[SkTerm
TermOf (AtomOf Formula)
x]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&.
           (([TermOf (AtomOf Formula)] -> Formula
f[SkTerm
TermOf (AtomOf Formula)
y] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. [TermOf (AtomOf Formula)] -> Formula
h[SkTerm
TermOf (AtomOf Formula)
y]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. [TermOf (AtomOf Formula)] -> Formula
g[SkTerm
TermOf (AtomOf Formula)
x]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&.
           ((([TermOf (AtomOf Formula)] -> Formula
f[SkTerm
TermOf (AtomOf Formula)
y] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. [TermOf (AtomOf Formula)] -> Formula
g[SkTerm
TermOf (AtomOf Formula)
y]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. [TermOf (AtomOf Formula)] -> Formula
h[SkTerm
TermOf (AtomOf Formula)
y]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. [TermOf (AtomOf Formula)] -> Formula
h[SkTerm
TermOf (AtomOf Formula)
x])
           Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. [TermOf (AtomOf Formula)] -> Formula
f[SkTerm
TermOf (AtomOf Formula)
z] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. [TermOf (AtomOf Formula)] -> Formula
g[SkTerm
TermOf (AtomOf Formula)
z] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. [TermOf (AtomOf Formula)] -> Formula
h[SkTerm
TermOf (AtomOf Formula)
z]
      [SkTerm
x, SkTerm
y, SkTerm
z] = [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"x", TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"y", TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"z"] :: [SkTerm]
      [[TermOf (AtomOf Formula)] -> Formula
f, [TermOf (AtomOf Formula)] -> Formula
g, [TermOf (AtomOf Formula)] -> Formula
h] = [PredOf (AtomOf Formula) -> [TermOf (AtomOf Formula)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp PredOf (AtomOf Formula)
"F", PredOf (AtomOf Formula) -> [TermOf (AtomOf Formula)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp PredOf (AtomOf Formula)
"G", PredOf (AtomOf Formula) -> [TermOf (AtomOf Formula)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp PredOf (AtomOf Formula)
"H"]

-- The Pelletier examples again.
p1 :: Test
p1 :: Test
p1 =
    let [Formula
p, Formula
q] = [PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp (String -> Predicate
forall a. IsString a => String -> a
fromString String
"p") [], PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp (String -> Predicate
forall a. IsString a => String -> a
fromString String
"q") []] :: [Formula] in
    Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> Set (Failing Bool) -> Set (Failing Bool) -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"p1" Set (Failing Bool)
forall a. Set a
Set.empty (SkolemT Identity Function (Set (Failing Bool))
-> Set (Failing Bool)
forall function a.
IsFunction function =>
SkolemT Identity function a -> a
runSkolem (Formula -> SkolemT Identity Function (Set (Failing Bool))
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 ((Formula
p Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. Formula
q Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)Formula
q Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)Formula
p) :: Formula)))

{-
-- -------------------------------------------------------------------------
-- The Pelletier examples again.
-- -------------------------------------------------------------------------

{- **********

let p1 = time presolution
 <<p ==> 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
 <<p \/ ~p>>;;

let p7 = time presolution
 <<p \/ ~ ~ ~p>>;;

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 <=> p>>;;

let p12 = time presolution
 <<((p <=> q) <=> r) <=> (p <=> (q <=> r))>>;;

let p13 = time presolution
 <<p \/ q /\ r <=> (p \/ q) /\ (p \/ r)>>;;

let p14 = time presolution
 <<(p <=> q) <=> (q \/ ~p) /\ (~q \/ p)>>;;

let p15 = time presolution
 <<p ==> q <=> ~p \/ q>>;;

let p16 = time presolution
 <<(p ==> q) \/ (q ==> p)>>;;

let p17 = time presolution
 <<p /\ (q ==> r) ==> s <=> (~p \/ q \/ s) /\ (~p \/ ~r \/ s)>>;;

-- -------------------------------------------------------------------------
-- Monadic Predicate Logic.
-- -------------------------------------------------------------------------

let p18 = time presolution
 <<exists y. forall x. P(y) ==> P(x)>>;;

let p19 = time presolution
 <<exists x. forall y z. (P(y) ==> Q(z)) ==> P(x) ==> Q(x)>>;;

let p20 = time presolution
 <<(forall x y. exists z. forall w. P(x) /\ Q(y) ==> R(z) /\ U(w))
   ==> (exists x y. P(x) /\ Q(y)) ==> (exists z. R(z))>>;;

let p21 = time presolution
 <<(exists x. P ==> Q(x)) /\ (exists x. Q(x) ==> P)
   ==> (exists x. P <=> Q(x))>>;;

let p22 = time presolution
 <<(forall x. P <=> Q(x)) ==> (P <=> (forall x. Q(x)))>>;;

let p23 = time presolution
 <<(forall x. P \/ Q(x)) <=> P \/ (forall x. Q(x))>>;;

let p24 = time presolution
 <<~(exists x. U(x) /\ Q(x)) /\
   (forall x. P(x) ==> Q(x) \/ R(x)) /\
   ~(exists x. P(x) ==> (exists x. Q(x))) /\
   (forall x. Q(x) /\ R(x) ==> U(x)) ==>
   (exists x. P(x) /\ R(x))>>;;

let p25 = time presolution
 <<(exists x. P(x)) /\
   (forall x. U(x) ==> ~G(x) /\ R(x)) /\
   (forall x. P(x) ==> G(x) /\ U(x)) /\
   ((forall x. P(x) ==> Q(x)) \/ (exists x. Q(x) /\ P(x))) ==>
   (exists x. Q(x) /\ P(x))>>;;

let p26 = time presolution
 <<((exists x. P(x)) <=> (exists x. Q(x))) /\
   (forall x y. P(x) /\ Q(y) ==> (R(x) <=> U(y))) ==>
   ((forall x. P(x) ==> R(x)) <=> (forall x. Q(x) ==> U(x)))>>;;

let p27 = time presolution
 <<(exists x. P(x) /\ ~Q(x)) /\
   (forall x. P(x) ==> R(x)) /\
   (forall x. U(x) /\ V(x) ==> P(x)) /\
   (exists x. R(x) /\ ~Q(x)) ==>
   (forall x. U(x) ==> ~R(x)) ==>
   (forall x. U(x) ==> ~V(x))>>;;

let p28 = time presolution
 <<(forall x. P(x) ==> (forall x. Q(x))) /\
   ((forall x. Q(x) \/ R(x)) ==> (exists x. Q(x) /\ R(x))) /\
   ((exists x. R(x)) ==> (forall x. L(x) ==> M(x))) ==>
   (forall x. P(x) /\ L(x) ==> M(x))>>;;

let p29 = time presolution
 <<(exists x. P(x)) /\ (exists x. G(x)) ==>
   ((forall x. P(x) ==> H(x)) /\ (forall x. G(x) ==> J(x)) <=>
    (forall x y. P(x) /\ G(y) ==> H(x) /\ J(y)))>>;;

let p30 = time presolution
 <<(forall x. P(x) \/ G(x) ==> ~H(x)) /\
   (forall x. (G(x) ==> ~U(x)) ==> P(x) /\ H(x)) ==>
   (forall x. U(x))>>;;

let p31 = time presolution
 <<~(exists x. P(x) /\ (G(x) \/ H(x))) /\ (exists x. Q(x) /\ P(x)) /\
   (forall x. ~H(x) ==> J(x)) ==>
   (exists x. Q(x) /\ J(x))>>;;

let p32 = time presolution
 <<(forall x. P(x) /\ (G(x) \/ H(x)) ==> Q(x)) /\
   (forall x. Q(x) /\ H(x) ==> J(x)) /\
   (forall x. R(x) ==> H(x)) ==>
   (forall x. P(x) /\ R(x) ==> J(x))>>;;

let p33 = time presolution
 <<(forall x. P(a) /\ (P(x) ==> P(b)) ==> P(c)) <=>
   (forall x. P(a) ==> P(x) \/ P(c)) /\ (P(a) ==> P(b) ==> P(c))>>;;

let p34 = time presolution
 <<((exists x. forall y. P(x) <=> P(y)) <=>
    ((exists x. Q(x)) <=> (forall y. Q(y)))) <=>
   ((exists x. forall y. Q(x) <=> Q(y)) <=>
    ((exists x. P(x)) <=> (forall y. P(y))))>>;;

let p35 = time presolution
 <<exists x y. P(x,y) ==> (forall x y. P(x,y))>>;;

-- -------------------------------------------------------------------------
--  Full predicate logic (without Identity and Functions)
-- -------------------------------------------------------------------------

let p36 = time presolution
 <<(forall x. exists y. P(x,y)) /\
   (forall x. exists y. G(x,y)) /\
   (forall x y. P(x,y) \/ G(x,y)
   ==> (forall z. P(y,z) \/ G(y,z) ==> H(x,z)))
       ==> (forall x. exists y. H(x,y))>>;;

let p37 = time presolution
 <<(forall z.
     exists w. forall x. exists y. (P(x,z) ==> P(y,w)) /\ P(y,z) /\
     (P(y,w) ==> (exists u. Q(u,w)))) /\
   (forall x z. ~P(x,z) ==> (exists y. Q(y,z))) /\
   ((exists x y. Q(x,y)) ==> (forall x. R(x,x))) ==>
   (forall x. exists y. R(x,y))>>;;

{- ** This one seems too slow

let p38 = time presolution
 <<(forall x.
     P(a) /\ (P(x) ==> (exists y. P(y) /\ R(x,y))) ==>
     (exists z w. P(z) /\ R(x,w) /\ R(w,z))) <=>
   (forall x.
     (~P(a) \/ P(x) \/ (exists z w. P(z) /\ R(x,w) /\ R(w,z))) /\
     (~P(a) \/ ~(exists y. P(y) /\ R(x,y)) \/
     (exists z w. P(z) /\ R(x,w) /\ R(w,z))))>>;;

 ** -}

let p39 = time presolution
 <<~(exists x. forall y. P(y,x) <=> ~P(y,y))>>;;

let p40 = time presolution
 <<(exists y. forall x. P(x,y) <=> P(x,x))
  ==> ~(forall x. exists y. forall z. P(z,y) <=> ~P(z,x))>>;;

let p41 = time presolution
 <<(forall z. exists y. forall x. P(x,y) <=> P(x,z) /\ ~P(x,x))
  ==> ~(exists z. forall x. P(x,z))>>;;

{- ** Also very slow

let p42 = time presolution
 <<~(exists y. forall x. P(x,y) <=> ~(exists z. P(x,z) /\ P(z,x)))>>;;

 ** -}

{- ** and this one too..

let p43 = time presolution
 <<(forall x y. Q(x,y) <=> forall z. P(z,x) <=> P(z,y))
   ==> forall x y. Q(x,y) <=> Q(y,x)>>;;

 ** -}

let p44 = time presolution
 <<(forall x. P(x) ==> (exists y. G(y) /\ H(x,y)) /\
   (exists y. G(y) /\ ~H(x,y))) /\
   (exists x. J(x) /\ (forall y. G(y) ==> H(x,y))) ==>
   (exists x. J(x) /\ ~P(x))>>;;

{- ** and this...

let p45 = time presolution
 <<(forall x.
     P(x) /\ (forall y. G(y) /\ H(x,y) ==> J(x,y)) ==>
       (forall y. G(y) /\ H(x,y) ==> R(y))) /\
   ~(exists y. L(y) /\ R(y)) /\
   (exists x. P(x) /\ (forall y. H(x,y) ==>
     L(y)) /\ (forall y. G(y) /\ H(x,y) ==> J(x,y))) ==>
   (exists x. P(x) /\ ~(exists y. G(y) /\ H(x,y)))>>;;

 ** -}

{- ** and this

let p46 = time presolution
 <<(forall x. P(x) /\ (forall y. P(y) /\ H(y,x) ==> G(y)) ==> G(x)) /\
   ((exists x. P(x) /\ ~G(x)) ==>
    (exists x. P(x) /\ ~G(x) /\
               (forall y. P(y) /\ ~G(y) ==> J(x,y)))) /\
   (forall x y. P(x) /\ P(y) /\ H(x,y) ==> ~J(y,x)) ==>
   (forall x. P(x) ==> G(x))>>;;

 ** -}

-- -------------------------------------------------------------------------
-- Example from Manthey and Bry, CADE-9.
-- -------------------------------------------------------------------------

let p55 = time presolution
 <<lives(agatha) /\ lives(butler) /\ lives(charles) /\
   (killed(agatha,agatha) \/ killed(butler,agatha) \/
    killed(charles,agatha)) /\
   (forall x y. killed(x,y) ==> hates(x,y) /\ ~richer(x,y)) /\
   (forall x. hates(agatha,x) ==> ~hates(charles,x)) /\
   (hates(agatha,agatha) /\ hates(agatha,charles)) /\
   (forall x. lives(x) /\ ~richer(x,agatha) ==> hates(butler,x)) /\
   (forall x. hates(agatha,x) ==> hates(butler,x)) /\
   (forall x. ~hates(x,agatha) \/ ~hates(x,butler) \/ ~hates(x,charles))
   ==> killed(agatha,agatha) /\
       ~killed(butler,agatha) /\
       ~killed(charles,agatha)>>;;

let p57 = time presolution
 <<P(f((a),b),f(b,c)) /\
   P(f(b,c),f(a,c)) /\
   (forall (x) y z. P(x,y) /\ P(y,z) ==> P(x,z))
   ==> P(f(a,b),f(a,c))>>;;

-- -------------------------------------------------------------------------
-- See info-hol, circa 1500.
-- -------------------------------------------------------------------------

let p58 = time presolution
 <<forall P Q R. forall x. exists v. exists w. forall y. forall z.
    ((P(x) /\ Q(y)) ==> ((P(v) \/ R(w))  /\ (R(z) ==> Q(v))))>>;;

let p59 = time presolution
 <<(forall x. P(x) <=> ~P(f(x))) ==> (exists x. P(x) /\ ~P(f(x)))>>;;

let p60 = time presolution
 <<forall x. P(x,f(x)) <=>
            exists y. (forall z. P(z,y) ==> P(z,f(x))) /\ P(x,y)>>;;

-- -------------------------------------------------------------------------
-- From Gilmore's classic paper.
-- -------------------------------------------------------------------------

let gilmore_1 = time presolution
 <<exists x. forall y 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)>>;;

{- ** This is not valid, according to Gilmore

let gilmore_2 = time presolution
 <<exists x y. forall z.
        (F(x,z) <=> F(z,y)) /\ (F(z,y) <=> F(z,z)) /\ (F(x,y) <=> F(y,x))
        ==> (F(x,y) <=> F(x,z))>>;;

 ** -}

let gilmore_3 = time presolution
 <<exists x. forall y z.
        ((F(y,z) ==> (G(y) ==> H(x))) ==> F(x,x)) /\
        ((F(z,x) ==> G(x)) ==> H(z)) /\
        F(x,y)
        ==> F(z,z)>>;;

let gilmore_4 = time presolution
 <<exists x y. forall z.
        (F(x,y) ==> F(y,z) /\ F(z,z)) /\
        (F(x,y) /\ G(x,y) ==> G(x,z) /\ G(z,z))>>;;

let gilmore_5 = time presolution
 <<(forall x. exists y. F(x,y) \/ F(y,x)) /\
   (forall x y. F(y,x) ==> F(y,y))
   ==> exists z. F(z,z)>>;;

let gilmore_6 = time presolution
 <<forall x. exists y.
        (exists u. forall v. F(u,x) ==> G(v,u) /\ G(u,x))
        ==> (exists u. forall v. F(u,y) ==> G(v,u) /\ G(u,y)) \/
            (forall u v. exists w. G(v,u) \/ H(w,y,u) ==> G(u,w))>>;;

let gilmore_7 = time presolution
 <<(forall x. K(x) ==> exists y. L(y) /\ (F(x,y) ==> G(x,y))) /\
   (exists z. K(z) /\ forall u. L(u) ==> F(z,u))
   ==> exists v w. K(v) /\ L(w) /\ G(v,w)>>;;

let gilmore_8 = time presolution
 <<exists x. forall y z.
        ((F(y,z) ==> (G(y) ==> (forall u. exists v. H(u,v,x)))) ==> F(x,x)) /\
        ((F(z,x) ==> G(x)) ==> (forall u. exists v. H(u,v,z))) /\
        F(x,y)
        ==> F(z,z)>>;;

{- ** This one still isn't easy!

let gilmore_9 = time presolution
 <<forall x. exists y. forall z.
        ((forall u. exists v. F(y,u,v) /\ G(y,u) /\ ~H(y,x))
          ==> (forall u. exists v. F(x,u,v) /\ G(z,u) /\ ~H(x,z))
             ==> (forall u. exists v. F(x,u,v) /\ G(y,u) /\ ~H(x,y))) /\
        ((forall u. exists v. F(x,u,v) /\ G(y,u) /\ ~H(x,y))
         ==> ~(forall u. exists v. F(x,u,v) /\ G(z,u) /\ ~H(x,z))
             ==> (forall u. exists v. F(y,u,v) /\ G(y,u) /\ ~H(y,x)) /\
                 (forall u. exists v. F(z,u,v) /\ G(y,u) /\ ~H(z,y)))>>;;

 ** -}

-- -------------------------------------------------------------------------
-- Example from Davis-Putnam papers where Gilmore procedure is poor.
-- -------------------------------------------------------------------------

let davis_putnam_example = time presolution
 <<exists x. exists y. forall z.
        (F(x,y) ==> (F(y,z) /\ F(z,z))) /\
        ((F(x,y) /\ G(x,y)) ==> (G(x,z) /\ G(z,z)))>>;;

*********** -}
END_INTERACTIVE;;

-- -------------------------------------------------------------------------
-- Example
-- -------------------------------------------------------------------------

START_INTERACTIVE;;
let gilmore_1 = resolution
 <<exists x. forall y 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)>>;;

-- -------------------------------------------------------------------------
-- Pelletiers yet again.
-- -------------------------------------------------------------------------

{- ************

let p1 = time resolution
 <<p ==> 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
 <<p \/ ~p>>;;

let p7 = time resolution
 <<p \/ ~ ~ ~p>>;;

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 <=> p>>;;

let p12 = time resolution
 <<((p <=> q) <=> r) <=> (p <=> (q <=> r))>>;;

let p13 = time resolution
 <<p \/ q /\ r <=> (p \/ q) /\ (p \/ r)>>;;

let p14 = time resolution
 <<(p <=> q) <=> (q \/ ~p) /\ (~q \/ p)>>;;

let p15 = time resolution
 <<p ==> q <=> ~p \/ q>>;;

let p16 = time resolution
 <<(p ==> q) \/ (q ==> p)>>;;

let p17 = time resolution
 <<p /\ (q ==> r) ==> s <=> (~p \/ q \/ s) /\ (~p \/ ~r \/ s)>>;;

(* ------------------------------------------------------------------------- *)
(* Monadic Predicate Logic.                                                  *)
(* ------------------------------------------------------------------------- *)

let p18 = time resolution
 <<exists y. forall x. P(y) ==> P(x)>>;;

let p19 = time resolution
 <<exists x. forall y z. (P(y) ==> Q(z)) ==> P(x) ==> Q(x)>>;;

let p20 = time resolution
 <<(forall x y. exists z. forall w. P(x) /\ Q(y) ==> R(z) /\ U(w)) ==>
   (exists x y. P(x) /\ Q(y)) ==>
   (exists z. R(z))>>;;

let p21 = time resolution
 <<(exists x. P ==> Q(x)) /\ (exists x. Q(x) ==> P) ==> (exists x. P <=> Q(x))>>;;

let p22 = time resolution
 <<(forall x. P <=> Q(x)) ==> (P <=> (forall x. Q(x)))>>;;

let p23 = time resolution
 <<(forall x. P \/ Q(x)) <=> P \/ (forall x. Q(x))>>;;

let p24 = time resolution
 <<~(exists x. U(x) /\ Q(x)) /\
   (forall x. P(x) ==> Q(x) \/ R(x)) /\
   ~(exists x. P(x) ==> (exists x. Q(x))) /\
   (forall x. Q(x) /\ R(x) ==> U(x)) ==>
   (exists x. P(x) /\ R(x))>>;;

let p25 = time resolution
 <<(exists x. P(x)) /\
   (forall x. U(x) ==> ~G(x) /\ R(x)) /\
   (forall x. P(x) ==> G(x) /\ U(x)) /\
   ((forall x. P(x) ==> Q(x)) \/ (exists x. Q(x) /\ P(x))) ==>
   (exists x. Q(x) /\ P(x))>>;;

let p26 = time resolution
 <<((exists x. P(x)) <=> (exists x. Q(x))) /\
   (forall x y. P(x) /\ Q(y) ==> (R(x) <=> U(y))) ==>
   ((forall x. P(x) ==> R(x)) <=> (forall x. Q(x) ==> U(x)))>>;;

let p27 = time resolution
 <<(exists x. P(x) /\ ~Q(x)) /\
   (forall x. P(x) ==> R(x)) /\
   (forall x. U(x) /\ V(x) ==> P(x)) /\
   (exists x. R(x) /\ ~Q(x)) ==>
   (forall x. U(x) ==> ~R(x)) ==>
   (forall x. U(x) ==> ~V(x))>>;;

let p28 = time resolution
 <<(forall x. P(x) ==> (forall x. Q(x))) /\
   ((forall x. Q(x) \/ R(x)) ==> (exists x. Q(x) /\ R(x))) /\
   ((exists x. R(x)) ==> (forall x. L(x) ==> M(x))) ==>
   (forall x. P(x) /\ L(x) ==> M(x))>>;;

let p29 = time resolution
 <<(exists x. P(x)) /\ (exists x. G(x)) ==>
   ((forall x. P(x) ==> H(x)) /\ (forall x. G(x) ==> J(x)) <=>
    (forall x y. P(x) /\ G(y) ==> H(x) /\ J(y)))>>;;

let p30 = time resolution
 <<(forall x. P(x) \/ G(x) ==> ~H(x)) /\ (forall x. (G(x) ==> ~U(x)) ==>
     P(x) /\ H(x)) ==>
   (forall x. U(x))>>;;

let p31 = time resolution
 <<~(exists x. P(x) /\ (G(x) \/ H(x))) /\ (exists x. Q(x) /\ P(x)) /\
   (forall x. ~H(x) ==> J(x)) ==>
   (exists x. Q(x) /\ J(x))>>;;

let p32 = time resolution
 <<(forall x. P(x) /\ (G(x) \/ H(x)) ==> Q(x)) /\
   (forall x. Q(x) /\ H(x) ==> J(x)) /\
   (forall x. R(x) ==> H(x)) ==>
   (forall x. P(x) /\ R(x) ==> J(x))>>;;

let p33 = time resolution
 <<(forall x. P(a) /\ (P(x) ==> P(b)) ==> P(c)) <=>
   (forall x. P(a) ==> P(x) \/ P(c)) /\ (P(a) ==> P(b) ==> P(c))>>;;

let p34 = time resolution
 <<((exists x. forall y. P(x) <=> P(y)) <=>
   ((exists x. Q(x)) <=> (forall y. Q(y)))) <=>
   ((exists x. forall y. Q(x) <=> Q(y)) <=>
  ((exists x. P(x)) <=> (forall y. P(y))))>>;;

let p35 = time resolution
 <<exists x y. P(x,y) ==> (forall x y. P(x,y))>>;;

(* ------------------------------------------------------------------------- *)
(*  Full predicate logic (without Identity and Functions)                    *)
(* ------------------------------------------------------------------------- *)

let p36 = time resolution
 <<(forall x. exists y. P(x,y)) /\
   (forall x. exists y. G(x,y)) /\
   (forall x y. P(x,y) \/ G(x,y)
   ==> (forall z. P(y,z) \/ G(y,z) ==> H(x,z)))
       ==> (forall x. exists y. H(x,y))>>;;

let p37 = time resolution
 <<(forall z.
     exists w. forall x. exists y. (P(x,z) ==> P(y,w)) /\ P(y,z) /\
     (P(y,w) ==> (exists u. Q(u,w)))) /\
   (forall x z. ~P(x,z) ==> (exists y. Q(y,z))) /\
   ((exists x y. Q(x,y)) ==> (forall x. R(x,x))) ==>
   (forall x. exists y. R(x,y))>>;;

(*** This one seems too slow

let p38 = time resolution
 <<(forall x.
     P(a) /\ (P(x) ==> (exists y. P(y) /\ R(x,y))) ==>
     (exists z w. P(z) /\ R(x,w) /\ R(w,z))) <=>
   (forall x.
     (~P(a) \/ P(x) \/ (exists z w. P(z) /\ R(x,w) /\ R(w,z))) /\
     (~P(a) \/ ~(exists y. P(y) /\ R(x,y)) \/
     (exists z w. P(z) /\ R(x,w) /\ R(w,z))))>>;;

 ***)

let p39 = time resolution
 <<~(exists x. forall y. P(y,x) <=> ~P(y,y))>>;;

let p40 = time resolution
 <<(exists y. forall x. P(x,y) <=> P(x,x))
  ==> ~(forall x. exists y. forall z. P(z,y) <=> ~P(z,x))>>;;

let p41 = time resolution
 <<(forall z. exists y. forall x. P(x,y) <=> P(x,z) /\ ~P(x,x))
  ==> ~(exists z. forall x. P(x,z))>>;;

(*** Also very slow

let p42 = time resolution
 <<~(exists y. forall x. P(x,y) <=> ~(exists z. P(x,z) /\ P(z,x)))>>;;

 ***)

(*** and this one too..

let p43 = time resolution
 <<(forall x y. Q(x,y) <=> forall z. P(z,x) <=> P(z,y))
   ==> forall x y. Q(x,y) <=> Q(y,x)>>;;

 ***)

let p44 = time resolution
 <<(forall x. P(x) ==> (exists y. G(y) /\ H(x,y)) /\
   (exists y. G(y) /\ ~H(x,y))) /\
   (exists x. J(x) /\ (forall y. G(y) ==> H(x,y))) ==>
   (exists x. J(x) /\ ~P(x))>>;;

(*** and this...

let p45 = time resolution
 <<(forall x.
     P(x) /\ (forall y. G(y) /\ H(x,y) ==> J(x,y)) ==>
       (forall y. G(y) /\ H(x,y) ==> R(y))) /\
   ~(exists y. L(y) /\ R(y)) /\
   (exists x. P(x) /\ (forall y. H(x,y) ==>
     L(y)) /\ (forall y. G(y) /\ H(x,y) ==> J(x,y))) ==>
   (exists x. P(x) /\ ~(exists y. G(y) /\ H(x,y)))>>;;

 ***)

(*** and this

let p46 = time resolution
 <<(forall x. P(x) /\ (forall y. P(y) /\ H(y,x) ==> G(y)) ==> G(x)) /\
   ((exists x. P(x) /\ ~G(x)) ==>
    (exists x. P(x) /\ ~G(x) /\
               (forall y. P(y) /\ ~G(y) ==> J(x,y)))) /\
   (forall x y. P(x) /\ P(y) /\ H(x,y) ==> ~J(y,x)) ==>
   (forall x. P(x) ==> G(x))>>;;

 ***)

(* ------------------------------------------------------------------------- *)
(* Example from Manthey and Bry, CADE-9.                                     *)
(* ------------------------------------------------------------------------- *)

let p55 = time resolution
 <<lives(agatha) /\ lives(butler) /\ lives(charles) /\
   (killed(agatha,agatha) \/ killed(butler,agatha) \/
    killed(charles,agatha)) /\
   (forall x y. killed(x,y) ==> hates(x,y) /\ ~richer(x,y)) /\
   (forall x. hates(agatha,x) ==> ~hates(charles,x)) /\
   (hates(agatha,agatha) /\ hates(agatha,charles)) /\
   (forall x. lives(x) /\ ~richer(x,agatha) ==> hates(butler,x)) /\
   (forall x. hates(agatha,x) ==> hates(butler,x)) /\
   (forall x. ~hates(x,agatha) \/ ~hates(x,butler) \/ ~hates(x,charles))
   ==> killed(agatha,agatha) /\
       ~killed(butler,agatha) /\
       ~killed(charles,agatha)>>;;

let p57 = time resolution
 <<P(f((a),b),f(b,c)) /\
   P(f(b,c),f(a,c)) /\
   (forall (x) y z. P(x,y) /\ P(y,z) ==> P(x,z))
   ==> P(f(a,b),f(a,c))>>;;

(* ------------------------------------------------------------------------- *)
(* See info-hol, circa 1500.                                                 *)
(* ------------------------------------------------------------------------- *)

let p58 = time resolution
 <<forall P Q R. forall x. exists v. exists w. forall y. forall z.
    ((P(x) /\ Q(y)) ==> ((P(v) \/ R(w))  /\ (R(z) ==> Q(v))))>>;;

let p59 = time resolution
 <<(forall x. P(x) <=> ~P(f(x))) ==> (exists x. P(x) /\ ~P(f(x)))>>;;

let p60 = time resolution
 <<forall x. P(x,f(x)) <=>
            exists y. (forall z. P(z,y) ==> P(z,f(x))) /\ P(x,y)>>;;

(* ------------------------------------------------------------------------- *)
(* From Gilmore's classic paper.                                             *)
(* ------------------------------------------------------------------------- *)

let gilmore_1 = time resolution
 <<exists x. forall y 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)>>;;

(*** This is not valid, according to Gilmore

let gilmore_2 = time resolution
 <<exists x y. forall z.
        (F(x,z) <=> F(z,y)) /\ (F(z,y) <=> F(z,z)) /\ (F(x,y) <=> F(y,x))
        ==> (F(x,y) <=> F(x,z))>>;;

 ***)

let gilmore_3 = time resolution
 <<exists x. forall y z.
        ((F(y,z) ==> (G(y) ==> H(x))) ==> F(x,x)) /\
        ((F(z,x) ==> G(x)) ==> H(z)) /\
        F(x,y)
        ==> F(z,z)>>;;

let gilmore_4 = time resolution
 <<exists x y. forall z.
        (F(x,y) ==> F(y,z) /\ F(z,z)) /\
        (F(x,y) /\ G(x,y) ==> G(x,z) /\ G(z,z))>>;;

let gilmore_5 = time resolution
 <<(forall x. exists y. F(x,y) \/ F(y,x)) /\
   (forall x y. F(y,x) ==> F(y,y))
   ==> exists z. F(z,z)>>;;

let gilmore_6 = time resolution
 <<forall x. exists y.
        (exists u. forall v. F(u,x) ==> G(v,u) /\ G(u,x))
        ==> (exists u. forall v. F(u,y) ==> G(v,u) /\ G(u,y)) \/
            (forall u v. exists w. G(v,u) \/ H(w,y,u) ==> G(u,w))>>;;

let gilmore_7 = time resolution
 <<(forall x. K(x) ==> exists y. L(y) /\ (F(x,y) ==> G(x,y))) /\
   (exists z. K(z) /\ forall u. L(u) ==> F(z,u))
   ==> exists v w. K(v) /\ L(w) /\ G(v,w)>>;;

let gilmore_8 = time resolution
 <<exists x. forall y z.
        ((F(y,z) ==> (G(y) ==> (forall u. exists v. H(u,v,x)))) ==> F(x,x)) /\
        ((F(z,x) ==> G(x)) ==> (forall u. exists v. H(u,v,z))) /\
        F(x,y)
        ==> F(z,z)>>;;

(*** This one still isn't easy!

let gilmore_9 = time resolution
 <<forall x. exists y. forall z.
        ((forall u. exists v. F(y,u,v) /\ G(y,u) /\ ~H(y,x))
          ==> (forall u. exists v. F(x,u,v) /\ G(z,u) /\ ~H(x,z))
             ==> (forall u. exists v. F(x,u,v) /\ G(y,u) /\ ~H(x,y))) /\
        ((forall u. exists v. F(x,u,v) /\ G(y,u) /\ ~H(x,y))
         ==> ~(forall u. exists v. F(x,u,v) /\ G(z,u) /\ ~H(x,z))
             ==> (forall u. exists v. F(y,u,v) /\ G(y,u) /\ ~H(y,x)) /\
                 (forall u. exists v. F(z,u,v) /\ G(y,u) /\ ~H(z,y)))>>;;

 ***)

(* ------------------------------------------------------------------------- *)
(* Example from Davis-Putnam papers where Gilmore procedure is poor.         *)
(* ------------------------------------------------------------------------- *)

let davis_putnam_example = time resolution
 <<exists x. exists y. forall z.
        (F(x,y) ==> (F(y,z) /\ F(z,z))) /\
        ((F(x,y) /\ G(x,y)) ==> (G(x,z) /\ G(z,z)))>>;;
-}
-}

-- | The (in)famous Los problem.
los :: Test
los :: Test
los =
    let [SkTerm
x, SkTerm
y, SkTerm
z] = (V -> SkTerm) -> [V] -> [SkTerm]
forall a b. (a -> b) -> [a] -> [b]
List.map (TVarOf SkTerm -> SkTerm
V -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt :: V -> SkTerm) [V
"x", V
"y", V
"z"]
        [[SkTerm] -> Formula
p, [SkTerm] -> Formula
q] = (Predicate -> [SkTerm] -> Formula)
-> [Predicate] -> [[SkTerm] -> Formula]
forall a b. (a -> b) -> [a] -> [b]
List.map Predicate -> [SkTerm] -> Formula
PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp [Predicate
"P", Predicate
"Q"] :: [[SkTerm] -> Formula]
        fm :: Formula
fm = (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"x" (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"y" (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"z" (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ [SkTerm] -> Formula
p[SkTerm
x,SkTerm
y] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. [SkTerm] -> Formula
p[SkTerm
y,SkTerm
z] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. [SkTerm] -> Formula
p[SkTerm
x,SkTerm
z]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&.
             (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"x" (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"y" (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"z" (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ [SkTerm] -> Formula
q[SkTerm
x,SkTerm
y] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. [SkTerm] -> Formula
q[SkTerm
y,SkTerm
z] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. [SkTerm] -> Formula
q[SkTerm
x,SkTerm
z]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&.
             (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"x" (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"y" (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ [SkTerm] -> Formula
q[SkTerm
x,SkTerm
y] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. [SkTerm] -> Formula
q[SkTerm
y,SkTerm
x]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&.
             (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"x" (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"y" (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ [SkTerm] -> Formula
p[SkTerm
x,SkTerm
y] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. [SkTerm] -> Formula
q[SkTerm
x,SkTerm
y])
             Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"x" (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"y" (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ [SkTerm] -> Formula
p[SkTerm
x,SkTerm
y]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"x" (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"y" (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$ [SkTerm] -> Formula
q[SkTerm
x,SkTerm
y]) :: Formula
        result :: Set (Failing Bool)
result = {-time-} SkolemT Identity Function (Set (Failing Bool))
-> Set (Failing Bool)
forall function a.
IsFunction function =>
SkolemT Identity function a -> a
runSkolem (Formula -> SkolemT Identity Function (Set (Failing Bool))
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 Formula
fm)
        expected :: Set (Failing Bool)
expected = Failing Bool -> Set (Failing Bool)
forall a. a -> Set a
Set.singleton (Bool -> Failing Bool
forall a. a -> Failing a
Success Bool
True) in
    Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> Set (Failing Bool) -> Set (Failing Bool) -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"los (p. 198)" Set (Failing Bool)
expected Set (Failing Bool)
result

testResolution :: Test
testResolution :: Test
testResolution = String -> Test -> Test
TestLabel String
"Resolution" ([Test] -> Test
TestList [Test
test01, Test
test02, Test
test03, Test
gilmore_1, Test
p1, Test
los])