-- | Tableaux, seen as an optimized version of a Prawitz-like procedure.
--
-- Copyright (c) 2003-2007, John Harrison. (See "LICENSE.txt" for details.)

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wall #-}

module Data.Logic.ATP.Tableaux
    ( prawitz
    , K(K)
    , tab
    , testTableaux
    ) where

import Data.Logic.ATP.Apply (HasApply(TermOf), pApp)
import Control.Monad.Fail
import Control.Monad.RWS (RWS)
import Control.Monad.State (execStateT, StateT)
import Data.List as List (map)
import Data.Logic.ATP.FOL (asubst, fv, generalize, IsFirstOrder, subst)
import Data.Logic.ATP.Formulas (atomic, IsFormula(asBool, AtomOf), onatoms, overatoms)
import Data.Logic.ATP.Herbrand (davisputnam)
import Data.Logic.ATP.Lib ((|=>), allpairs, deepen, Depth(Depth), distrib, evalRS, Failing(Success, Failure), failing, settryfind, tryfindM)
import Data.Logic.ATP.Lit ((.~.), convertToLiteral, IsLiteral, JustLiteral, LFormula, positive)
import Data.Logic.ATP.LitWrapper (JL)
import Data.Logic.ATP.Pretty (assertEqual', Pretty(pPrint), prettyShow, text)
import Data.Logic.ATP.Prop ( (.&.), (.=>.), (.<=>.), (.|.), BinOp((:&:), (:|:)), PFormula, simpdnf)
import Data.Logic.ATP.Quantified (exists, foldQuantified, for_all, Quant((:!:)))
import Data.Logic.ATP.Skolem (askolemize, Formula, HasSkolem(SVarOf, toSkolem), runSkolem, simpdnf', skolemize, SkTerm)
import Data.Logic.ATP.Term (fApp, IsTerm(TVarOf, FunOf), vt)
import Data.Logic.ATP.Unif (Unify(UTermOf), unify_literals)
import Data.Map.Strict as Map
import Data.Set as Set
import Data.String (IsString(..))
import Prelude hiding (compare)
import Test.HUnit hiding (State)

-- | Unify complementary literals.
unify_complements :: (IsLiteral lit1, JustLiteral lit2, HasApply atom1, HasApply atom2,
                      Unify m (atom1, atom2), term ~ UTermOf (atom1, atom2), v ~ TVarOf term,
                      atom1 ~ AtomOf lit1, term ~ TermOf atom1,
                      atom2 ~ AtomOf lit2, term ~ TermOf atom2, MonadFail m) =>
                     lit1 -> lit2 -> StateT (Map v term) m ()
unify_complements :: forall lit1 lit2 atom1 atom2 (m :: * -> *) term v.
(IsLiteral lit1, JustLiteral lit2, HasApply atom1, HasApply atom2,
 Unify m (atom1, atom2), term ~ UTermOf (atom1, atom2),
 v ~ TVarOf term, atom1 ~ AtomOf lit1, term ~ TermOf atom1,
 atom2 ~ AtomOf lit2, term ~ TermOf atom2, MonadFail m) =>
lit1 -> lit2 -> StateT (Map v term) m ()
unify_complements lit1
p lit2
q = lit1 -> lit2 -> StateT (Map v term) m ()
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 lit1
p (lit2 -> lit2
forall formula. IsLiteral formula => formula -> formula
(.~.) lit2
q)

-- | Unify and refute a set of disjuncts.
unify_refute :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term,
                 Unify Failing (atom, atom), term ~ UTermOf (atom, atom), v ~ TVarOf term,
                 atom ~ AtomOf lit, term ~ TermOf atom) =>
                Set (Set lit) -> Map v term -> Failing (Map v term)
unify_refute :: forall lit atom term v.
(JustLiteral lit, Ord lit, HasApply atom, IsTerm term,
 Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
 v ~ TVarOf term, atom ~ AtomOf lit, term ~ TermOf atom) =>
Set (Set lit) -> Map v term -> Failing (Map v term)
unify_refute Set (Set lit)
djs Map v term
env =
    case Set (Set lit) -> Maybe (Set lit, Set (Set lit))
forall a. Set a -> Maybe (a, Set a)
Set.minView Set (Set lit)
djs of
      Maybe (Set lit, Set (Set lit))
Nothing -> Map v term -> Failing (Map v term)
forall a. a -> Failing a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Map v term
env
      Just (Set lit
d, Set (Set lit)
odjs) ->
          ((lit, lit) -> Failing (Map v term))
-> Set (lit, lit) -> Failing (Map v term)
forall t a. (t -> Failing a) -> Set t -> Failing a
settryfind (\ (lit
p, lit
n) -> 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 (m :: * -> *) term v.
(IsLiteral lit1, JustLiteral lit2, HasApply atom1, HasApply atom2,
 Unify m (atom1, atom2), term ~ UTermOf (atom1, atom2),
 v ~ TVarOf term, atom1 ~ AtomOf lit1, term ~ TermOf atom1,
 atom2 ~ AtomOf lit2, term ~ TermOf atom2, MonadFail m) =>
lit1 -> lit2 -> StateT (Map v term) m ()
unify_complements lit
p lit
n) Map v term
env Failing (Map v term)
-> (Map v term -> Failing (Map v term)) -> Failing (Map v term)
forall a b. Failing a -> (a -> Failing b) -> Failing b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Set (Set lit) -> Map v term -> Failing (Map v term)
forall lit atom term v.
(JustLiteral lit, Ord lit, HasApply atom, IsTerm term,
 Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
 v ~ TVarOf term, atom ~ AtomOf lit, term ~ TermOf atom) =>
Set (Set lit) -> Map v term -> Failing (Map v term)
unify_refute Set (Set lit)
odjs) Set (lit, lit)
pairs
          where
            pairs :: Set (lit, lit)
pairs = (lit -> lit -> (lit, lit)) -> Set lit -> Set lit -> Set (lit, lit)
forall a b c (set :: * -> *).
(SetLike set, Ord c) =>
(a -> b -> c) -> set a -> set b -> set c
allpairs (,) Set lit
pos Set lit
neg
            (Set lit
pos,Set lit
neg) = (lit -> Bool) -> Set lit -> (Set lit, Set lit)
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition lit -> Bool
forall formula. IsLiteral formula => formula -> Bool
positive Set lit
d

-- | Hence a Prawitz-like procedure (using unification on DNF).
prawitz_loop :: forall lit atom v term.
                (JustLiteral lit, Ord lit, HasApply atom, Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
                 atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
                Set (Set lit) -> [v] -> Set (Set lit) -> Int -> (Map v term, Int)
prawitz_loop :: forall lit atom v term.
(JustLiteral lit, Ord lit, HasApply atom,
 Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
 atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
Set (Set lit) -> [v] -> Set (Set lit) -> Int -> (Map v term, Int)
prawitz_loop Set (Set lit)
djs0 [v]
fvs Set (Set lit)
djs Int
n =
    let inst :: Map v (TermOf atom)
inst = [(v, TermOf atom)] -> Map v (TermOf atom)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([v] -> [TermOf atom] -> [(v, TermOf atom)]
forall a b. [a] -> [b] -> [(a, b)]
zip [v]
fvs ((Int -> TermOf atom) -> [Int] -> [TermOf atom]
forall a b. (a -> b) -> [a] -> [b]
List.map Int -> TermOf atom
newvar [Int
1..]))
        djs1 :: Set (Set lit)
djs1 = Set (Set lit) -> Set (Set lit) -> Set (Set lit)
forall a. Ord a => Set (Set a) -> Set (Set a) -> Set (Set a)
distrib ((Set lit -> Set lit) -> Set (Set lit) -> Set (Set lit)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((lit -> lit) -> Set lit -> Set lit
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((AtomOf lit -> AtomOf lit) -> lit -> lit
forall formula.
IsFormula formula =>
(AtomOf formula -> AtomOf formula) -> formula -> formula
onatoms (Map v (TermOf atom) -> atom -> atom
forall atom term v.
(HasApply atom, IsTerm term, term ~ TermOf atom,
 v ~ TVarOf term) =>
Map v term -> atom -> atom
asubst Map v (TermOf atom)
inst))) Set (Set lit)
djs0) Set (Set lit)
djs in
    case Set (Set lit) -> Map v term -> Failing (Map v term)
forall lit atom term v.
(JustLiteral lit, Ord lit, HasApply atom, IsTerm term,
 Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
 v ~ TVarOf term, atom ~ AtomOf lit, term ~ TermOf atom) =>
Set (Set lit) -> Map v term -> Failing (Map v term)
unify_refute Set (Set lit)
djs1 Map v term
forall k a. Map k a
Map.empty of
      Failure [[Char]]
_ -> Set (Set lit) -> [v] -> Set (Set lit) -> Int -> (Map v term, Int)
forall lit atom v term.
(JustLiteral lit, Ord lit, HasApply atom,
 Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
 atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
Set (Set lit) -> [v] -> Set (Set lit) -> Int -> (Map v term, Int)
prawitz_loop Set (Set lit)
djs0 [v]
fvs Set (Set lit)
djs1 (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
      Success Map v term
env -> (Map v term
env, Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
    where
      newvar :: Int -> TermOf atom
newvar Int
k = TVarOf (TermOf atom) -> TermOf atom
forall term. IsTerm term => TVarOf term -> term
vt ([Char] -> TVarOf (TermOf atom)
forall a. IsString a => [Char] -> a
fromString ([Char]
"_" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
* [v] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [v]
fvs Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
k)))

prawitz :: forall formula atom term function v.
           (IsFirstOrder formula, Ord formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), HasSkolem function, Show formula,
            atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
            v ~ TVarOf term, v ~ SVarOf function) =>
           formula -> Int
prawitz :: forall formula atom term function v.
(IsFirstOrder formula, Ord formula, Unify Failing (atom, atom),
 term ~ UTermOf (atom, atom), HasSkolem function, Show formula,
 atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
 v ~ TVarOf term, v ~ SVarOf function) =>
formula -> Int
prawitz formula
fm =
    (Map v (UTermOf (atom, atom)), Int) -> Int
forall a b. (a, b) -> b
snd (Set (Set (LFormula atom))
-> [v]
-> Set (Set (LFormula atom))
-> Int
-> (Map v (UTermOf (atom, atom)), Int)
forall lit atom v term.
(JustLiteral lit, Ord lit, HasApply atom,
 Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
 atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
Set (Set lit) -> [v] -> Set (Set lit) -> Int -> (Map v term, Int)
prawitz_loop Set (Set (LFormula atom))
dnf (Set v -> [v]
forall a. Set a -> [a]
Set.toList Set v
fvs) Set (Set (LFormula atom))
forall {a}. Set (Set a)
dnf0 Int
0)
    where
      dnf0 :: Set (Set a)
dnf0 = Set a -> Set (Set a)
forall a. a -> Set a
Set.singleton Set a
forall a. Set a
Set.empty
      dnf :: Set (Set (LFormula atom))
dnf = ((AtomOf (PFormula atom) -> AtomOf (LFormula atom))
-> PFormula atom -> Set (Set (LFormula atom))
forall pf lit.
(JustPropositional pf, IsLiteral lit, JustLiteral lit, Ord lit) =>
(AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
simpdnf atom -> atom
AtomOf (PFormula atom) -> AtomOf (LFormula atom)
forall a. a -> a
id PFormula atom
pf :: Set (Set (LFormula atom)))
      fvs :: Set v
fvs = (AtomOf (PFormula atom) -> Set v -> Set v)
-> PFormula atom -> Set v -> Set v
forall formula r.
IsFormula formula =>
(AtomOf formula -> r -> r) -> formula -> r -> r
forall r.
(AtomOf (PFormula atom) -> r -> r) -> PFormula atom -> r -> r
overatoms (\ AtomOf (PFormula atom)
a Set v
s -> Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
Set.union (formula -> Set v
forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
formula -> Set v
fv (AtomOf formula -> formula
forall formula. IsFormula formula => AtomOf formula -> formula
atomic AtomOf formula
AtomOf (PFormula atom)
a :: formula)) Set v
s) PFormula atom
pf (Set v
forall a. Set a
Set.empty :: Set v)
      pf :: PFormula atom
pf = SkolemT Identity function (PFormula atom) -> PFormula atom
forall function a.
IsFunction function =>
SkolemT Identity function a -> a
runSkolem ((AtomOf formula -> AtomOf (PFormula atom))
-> formula -> SkolemT Identity function (PFormula atom)
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 atom -> atom
AtomOf formula -> AtomOf (PFormula atom)
forall a. a -> a
id (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.)(formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
generalize formula
fm))) :: PFormula atom

-- -------------------------------------------------------------------------
-- Examples.
-- -------------------------------------------------------------------------

p20 :: Test
p20 :: Test
p20 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ [Char] -> Int -> Int -> Assertion
forall a.
(?loc::CallStack, Eq a, Pretty a) =>
[Char] -> a -> a -> Assertion
assertEqual' [Char]
"p20 - prawitz (p. 175)" Int
forall {a}. Num a => a
expected Int
input
    where fm :: Formula
          fm :: Formula
fm = (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"x" (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"y" (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"z" (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"w" (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)
"P" [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"x"] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> 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
PredOf (FOL Predicate SkTerm)
"Q" [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"y"] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> 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
PredOf (FOL Predicate SkTerm)
"R" [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"z"] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> 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
PredOf (FOL Predicate SkTerm)
"U" [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"w"]))))) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>.
               (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"x" (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"y" (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)
"P" [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"x"] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> 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
PredOf (FOL Predicate SkTerm)
"Q" [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"y"]))) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"z" (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)
"R" [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"z"]))
          input :: Int
input = Formula -> Int
forall formula atom term function v.
(IsFirstOrder formula, Ord formula, Unify Failing (atom, atom),
 term ~ UTermOf (atom, atom), HasSkolem function, Show formula,
 atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
 v ~ TVarOf term, v ~ SVarOf function) =>
formula -> Int
prawitz Formula
fm
          expected :: a
expected = a
2

-- -------------------------------------------------------------------------
-- Comparison of number of ground instances.
-- -------------------------------------------------------------------------

compare :: (IsFirstOrder formula, Ord formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), HasSkolem function, Show formula,
            atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
            v ~ TVarOf term, v ~ SVarOf function) =>
           formula -> (Int, Int)
compare :: forall formula atom term function v.
(IsFirstOrder formula, Ord formula, Unify Failing (atom, atom),
 term ~ UTermOf (atom, atom), HasSkolem function, Show formula,
 atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
 v ~ TVarOf term, v ~ SVarOf function) =>
formula -> (Int, Int)
compare formula
fm = (formula -> Int
forall formula atom term function v.
(IsFirstOrder formula, Ord formula, Unify Failing (atom, atom),
 term ~ UTermOf (atom, atom), HasSkolem function, Show formula,
 atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
 v ~ TVarOf term, v ~ SVarOf function) =>
formula -> Int
prawitz formula
fm, formula -> Int
forall formula atom term v function.
(IsFirstOrder formula, Ord formula, HasSkolem function,
 atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
 v ~ TVarOf term, v ~ SVarOf function) =>
formula -> Int
davisputnam formula
fm)

p19 :: Test
p19 :: Test
p19 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ [Char] -> (Int, Int) -> (Int, Int) -> Assertion
forall a.
(?loc::CallStack, Eq a, Pretty a) =>
[Char] -> a -> a -> Assertion
assertEqual' [Char]
"p19" (Int, Int)
forall {a} {b}. (Num a, Num b) => (a, b)
expected (Int, Int)
input
    where
      fm :: Formula
      fm :: Formula
fm = VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"x" (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"y" (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"z" ((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)
"P" [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"y"] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> 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
PredOf (FOL Predicate SkTerm)
"Q" [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"z"]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> 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
PredOf (FOL Predicate SkTerm)
"P" [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"x"] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> 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
PredOf (FOL Predicate SkTerm)
"Q" [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"x"])))
      input :: (Int, Int)
input = Formula -> (Int, Int)
forall formula atom term function v.
(IsFirstOrder formula, Ord formula, Unify Failing (atom, atom),
 term ~ UTermOf (atom, atom), HasSkolem function, Show formula,
 atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
 v ~ TVarOf term, v ~ SVarOf function) =>
formula -> (Int, Int)
compare Formula
fm
      expected :: (a, b)
expected = (a
3, b
3)

{-
START_INTERACTIVE;;
let p20 = compare
 <<(for_all x y. exists z. for_all w. P[vt "x"] .&. Q[vt "y"] .=>. R[vt "z"] .&. U[vt "w"])
   .=>. (exists x y. P[vt "x"] .&. Q[vt "y"]) .=>. (exists z. R[vt "z"])>>;;

let p24 = compare
 <<~(exists x. U[vt "x"] .&. Q[vt "x"]) .&.
   (for_all x. P[vt "x"] .=>. Q[vt "x"] .|. R[vt "x"]) .&.
   ~(exists x. P[vt "x"] .=>. (exists x. Q[vt "x"])) .&.
   (for_all x. Q[vt "x"] .&. R[vt "x"] .=>. U[vt "x"])
   .=>. (exists x. P[vt "x"] .&. R[vt "x"])>>;;

let p39 = compare
 <<~(exists x. for_all y. P(y,x) .<=>. ~P(y,y))>>;;

let p42 = compare
 <<~(exists y. for_all x. P(x,y) .<=>. ~(exists z. P(x,z) .&. P(z,x)))>>;;

{- **** Too slow?

let p43 = compare
 <<(for_all x y. Q(x,y) .<=>. for_all z. P(z,x) .<=>. P(z,y))
   .=>. for_all x y. Q(x,y) .<=>. Q(y,x)>>;;

 ***** -}

let p44 = compare
 <<(for_all x. P[vt "x"] .=>. (exists y. G[vt "y"] .&. H(x,y)) .&.
   (exists y. G[vt "y"] .&. ~H(x,y))) .&.
   (exists x. J[vt "x"] .&. (for_all y. G[vt "y"] .=>. H(x,y)))
   .=>. (exists x. J[vt "x"] .&. ~P[vt "x"])>>;;

let p59 = compare
 <<(for_all x. P[vt "x"] .<=>. ~P(f[vt "x"])) .=>. (exists x. P[vt "x"] .&. ~P(f[vt "x"]))>>;;

let p60 = compare
 <<for_all x. P(x,f[vt "x"]) .<=>.
             exists y. (for_all z. P(z,y) .=>. P(z,f[vt "x"])) .&. P(x,y)>>;;

END_INTERACTIVE;;
-}

newtype K = K Int deriving (K -> K -> Bool
(K -> K -> Bool) -> (K -> K -> Bool) -> Eq K
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: K -> K -> Bool
== :: K -> K -> Bool
$c/= :: K -> K -> Bool
/= :: K -> K -> Bool
Eq, Eq K
Eq K =>
(K -> K -> Ordering)
-> (K -> K -> Bool)
-> (K -> K -> Bool)
-> (K -> K -> Bool)
-> (K -> K -> Bool)
-> (K -> K -> K)
-> (K -> K -> K)
-> Ord K
K -> K -> Bool
K -> K -> Ordering
K -> K -> K
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: K -> K -> Ordering
compare :: K -> K -> Ordering
$c< :: K -> K -> Bool
< :: K -> K -> Bool
$c<= :: K -> K -> Bool
<= :: K -> K -> Bool
$c> :: K -> K -> Bool
> :: K -> K -> Bool
$c>= :: K -> K -> Bool
>= :: K -> K -> Bool
$cmax :: K -> K -> K
max :: K -> K -> K
$cmin :: K -> K -> K
min :: K -> K -> K
Ord, Int -> K -> [Char] -> [Char]
[K] -> [Char] -> [Char]
K -> [Char]
(Int -> K -> [Char] -> [Char])
-> (K -> [Char]) -> ([K] -> [Char] -> [Char]) -> Show K
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> K -> [Char] -> [Char]
showsPrec :: Int -> K -> [Char] -> [Char]
$cshow :: K -> [Char]
show :: K -> [Char]
$cshowList :: [K] -> [Char] -> [Char]
showList :: [K] -> [Char] -> [Char]
Show)

instance Enum K where
    toEnum :: Int -> K
toEnum = Int -> K
K
    fromEnum :: K -> Int
fromEnum (K Int
n) = Int
n

instance Pretty K where
    pPrint :: K -> Doc
pPrint (K Int
n) = [Char] -> Doc
text ([Char]
"K" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
n)

-- | More standard tableau procedure, effectively doing DNF incrementally.  (p. 177)
tableau :: forall formula atom term v function.
           (IsFirstOrder formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
            atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term) =>
           [formula] -> Depth -> RWS () () () (Failing (K, Map v term))
tableau :: forall formula atom term v function.
(IsFirstOrder formula, Unify Failing (atom, atom),
 term ~ UTermOf (atom, atom), atom ~ AtomOf formula,
 term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term) =>
[formula] -> Depth -> RWS () () () (Failing (K, Map v term))
tableau [formula]
fms Depth
n0 =
    ([formula], [JL formula], Depth)
-> ((K, Map v term) -> RWS () () () (Failing (K, Map v term)))
-> (K, Map v term)
-> RWS () () () (Failing (K, Map v term))
go ([formula]
fms, [], Depth
n0) (Failing (K, Map v term) -> RWS () () () (Failing (K, Map v term))
forall a. a -> RWST () () () Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Failing (K, Map v term) -> RWS () () () (Failing (K, Map v term)))
-> ((K, Map v term) -> Failing (K, Map v term))
-> (K, Map v term)
-> RWS () () () (Failing (K, Map v term))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (K, Map v term) -> Failing (K, Map v term)
forall a. a -> Failing a
Success) (Int -> K
K Int
0, Map v term
forall k a. Map k a
Map.empty)
    where
      go :: ([formula], [JL formula], Depth)
         -> ((K, Map v term) -> RWS () () () (Failing (K, Map v term)))
         -> (K, Map v term)
         -> RWS () () () (Failing (K, Map v term))
      go :: ([formula], [JL formula], Depth)
-> ((K, Map v term) -> RWS () () () (Failing (K, Map v term)))
-> (K, Map v term)
-> RWS () () () (Failing (K, Map v term))
go ([formula]
_, [JL formula]
_, Depth
n) (K, Map v term) -> RWS () () () (Failing (K, Map v term))
_ (K
_, Map v term
_) | Depth
n Depth -> Depth -> Bool
forall a. Ord a => a -> a -> Bool
< Int -> Depth
Depth Int
0 = Failing (K, Map v term) -> RWS () () () (Failing (K, Map v term))
forall a. a -> RWST () () () Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Failing (K, Map v term) -> RWS () () () (Failing (K, Map v term)))
-> Failing (K, Map v term)
-> RWS () () () (Failing (K, Map v term))
forall a b. (a -> b) -> a -> b
$ [[Char]] -> Failing (K, Map v term)
forall a. [[Char]] -> Failing a
Failure [[Char]
"no proof at this level"]
      go ([], [JL formula]
_, Depth
_) (K, Map v term) -> RWS () () () (Failing (K, Map v term))
_ (K
_, Map v term
_) =  Failing (K, Map v term) -> RWS () () () (Failing (K, Map v term))
forall a. a -> RWST () () () Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Failing (K, Map v term) -> RWS () () () (Failing (K, Map v term)))
-> Failing (K, Map v term)
-> RWS () () () (Failing (K, Map v term))
forall a b. (a -> b) -> a -> b
$ [[Char]] -> Failing (K, Map v term)
forall a. [[Char]] -> Failing a
Failure [[Char]
"tableau: no proof"]
      go (formula
fm : [formula]
unexp, [JL formula]
lits, Depth
n) (K, Map v term) -> RWS () () () (Failing (K, Map v term))
cont (K
k, Map v term
env) =
          (Quant
 -> VarOf formula
 -> formula
 -> RWS () () () (Failing (K, Map v term)))
-> (formula
    -> BinOp -> formula -> RWS () () () (Failing (K, Map v term)))
-> (formula -> RWS () () () (Failing (K, Map v term)))
-> (Bool -> RWS () () () (Failing (K, Map v term)))
-> (AtomOf formula -> RWS () () () (Failing (K, Map v term)))
-> formula
-> RWS () () () (Failing (K, Map v term))
forall formula r.
IsQuantified formula =>
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
foldQuantified Quant -> v -> formula -> RWS () () () (Failing (K, Map v term))
Quant
-> VarOf formula
-> formula
-> RWS () () () (Failing (K, Map v term))
qu formula
-> BinOp -> formula -> RWS () () () (Failing (K, Map v term))
co (\formula
_ -> formula -> [formula] -> RWS () () () (Failing (K, Map v term))
go2 formula
fm [formula]
unexp) (\Bool
_ -> formula -> [formula] -> RWS () () () (Failing (K, Map v term))
go2 formula
fm [formula]
unexp) (\AtomOf formula
_ -> formula -> [formula] -> RWS () () () (Failing (K, Map v term))
go2 formula
fm [formula]
unexp) formula
fm
          where
            qu :: Quant -> v -> formula -> RWS () () () (Failing (K, Map v term))
            qu :: Quant -> v -> formula -> RWS () () () (Failing (K, Map v term))
qu Quant
(:!:) v
x formula
p =
                let y :: term
y = TVarOf term -> term
forall term. IsTerm term => TVarOf term -> term
vt ([Char] -> TVarOf term
forall a. IsString a => [Char] -> a
fromString (K -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow K
k))
                    p' :: formula
p' = Map v term -> formula -> formula
forall formula term v.
(IsFirstOrder formula, term ~ TermOf (AtomOf formula),
 v ~ VarOf formula) =>
Map v term -> formula -> formula
subst (v
x v -> term -> Map v term
forall k a. Ord k => k -> a -> Map k a
|=> term
y) formula
p in
                ([formula], [JL formula], Depth)
-> ((K, Map v term) -> RWS () () () (Failing (K, Map v term)))
-> (K, Map v term)
-> RWS () () () (Failing (K, Map v term))
go ([formula
p'] [formula] -> [formula] -> [formula]
forall a. [a] -> [a] -> [a]
++ [formula]
unexp [formula] -> [formula] -> [formula]
forall a. [a] -> [a] -> [a]
++ [VarOf formula -> formula -> formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all v
VarOf formula
x formula
p],[JL formula]
lits,Depth -> Depth
forall a. Enum a => a -> a
pred Depth
n) (K, Map v term) -> RWS () () () (Failing (K, Map v term))
cont (K -> K
forall a. Enum a => a -> a
succ K
k, Map v term
env)
            qu Quant
_ v
_ formula
_ = formula -> [formula] -> RWS () () () (Failing (K, Map v term))
go2 formula
fm [formula]
unexp
            co :: formula
-> BinOp -> formula -> RWS () () () (Failing (K, Map v term))
co formula
p BinOp
(:&:) formula
q =
                ([formula], [JL formula], Depth)
-> ((K, Map v term) -> RWS () () () (Failing (K, Map v term)))
-> (K, Map v term)
-> RWS () () () (Failing (K, Map v term))
go (formula
p formula -> [formula] -> [formula]
forall a. a -> [a] -> [a]
: formula
q formula -> [formula] -> [formula]
forall a. a -> [a] -> [a]
: [formula]
unexp,[JL formula]
lits,Depth
n) (K, Map v term) -> RWS () () () (Failing (K, Map v term))
cont (K
k, Map v term
env)
            co formula
p BinOp
(:|:) formula
q =
                ([formula], [JL formula], Depth)
-> ((K, Map v term) -> RWS () () () (Failing (K, Map v term)))
-> (K, Map v term)
-> RWS () () () (Failing (K, Map v term))
go (formula
p formula -> [formula] -> [formula]
forall a. a -> [a] -> [a]
: [formula]
unexp,[JL formula]
lits,Depth
n) (([formula], [JL formula], Depth)
-> ((K, Map v term) -> RWS () () () (Failing (K, Map v term)))
-> (K, Map v term)
-> RWS () () () (Failing (K, Map v term))
go (formula
q formula -> [formula] -> [formula]
forall a. a -> [a] -> [a]
: [formula]
unexp,[JL formula]
lits,Depth
n) (K, Map v term) -> RWS () () () (Failing (K, Map v term))
cont) (K
k, Map v term
env)
            co formula
_ BinOp
_ formula
_ = formula -> [formula] -> RWS () () () (Failing (K, Map v term))
go2 formula
fm [formula]
unexp

            go2 :: formula -> [formula] -> RWS () () () (Failing (K, Map v term))
            go2 :: formula -> [formula] -> RWS () () () (Failing (K, Map v term))
go2 formula
fm' [formula]
unexp' =
                let (JL formula
fm'' :: JL formula) = (formula -> JL formula)
-> (AtomOf formula -> AtomOf (JL formula)) -> formula -> JL formula
forall formula lit.
(IsLiteral formula, JustLiteral lit) =>
(formula -> lit)
-> (AtomOf formula -> AtomOf lit) -> formula -> lit
convertToLiteral ([Char] -> formula -> JL formula
forall a. HasCallStack => [Char] -> a
error [Char]
"expected JustLiteral") atom -> atom
AtomOf formula -> AtomOf (JL formula)
forall a. a -> a
id formula
fm' in
                (JL formula -> RWS () () () (Failing (K, Map v term)))
-> [JL formula] -> RWS () () () (Failing (K, Map v term))
forall (m :: * -> *) t a.
Monad m =>
(t -> m (Failing a)) -> [t] -> m (Failing a)
tryfindM (JL formula -> JL formula -> RWS () () () (Failing (K, Map v term))
tryLit JL formula
fm'') [JL formula]
lits RWS () () () (Failing (K, Map v term))
-> (Failing (K, Map v term)
    -> RWS () () () (Failing (K, Map v term)))
-> RWS () () () (Failing (K, Map v term))
forall a b.
RWST () () () Identity a
-> (a -> RWST () () () Identity b) -> RWST () () () Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
                ([[Char]] -> RWS () () () (Failing (K, Map v term)))
-> ((K, Map v term) -> RWS () () () (Failing (K, Map v term)))
-> Failing (K, Map v term)
-> RWS () () () (Failing (K, Map v term))
forall b a. ([[Char]] -> b) -> (a -> b) -> Failing a -> b
failing (\[[Char]]
_ -> ([formula], [JL formula], Depth)
-> ((K, Map v term) -> RWS () () () (Failing (K, Map v term)))
-> (K, Map v term)
-> RWS () () () (Failing (K, Map v term))
go ([formula]
unexp', JL formula
fm'' JL formula -> [JL formula] -> [JL formula]
forall a. a -> [a] -> [a]
: [JL formula]
lits, Depth
n) (K, Map v term) -> RWS () () () (Failing (K, Map v term))
cont (K
k, Map v term
env))
                        (Failing (K, Map v term) -> RWS () () () (Failing (K, Map v term))
forall a. a -> RWST () () () Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Failing (K, Map v term) -> RWS () () () (Failing (K, Map v term)))
-> ((K, Map v term) -> Failing (K, Map v term))
-> (K, Map v term)
-> RWS () () () (Failing (K, Map v term))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (K, Map v term) -> Failing (K, Map v term)
forall a. a -> Failing a
Success)
            tryLit :: JL formula -> JL formula -> RWS () () () (Failing (K, Map v term))
            tryLit :: JL formula -> JL formula -> RWS () () () (Failing (K, Map v term))
tryLit JL formula
fm' JL formula
l = ([[Char]] -> RWS () () () (Failing (K, Map v term)))
-> (Map v term -> RWS () () () (Failing (K, Map v term)))
-> Failing (Map v term)
-> RWS () () () (Failing (K, Map v term))
forall b a. ([[Char]] -> b) -> (a -> b) -> Failing a -> b
failing (Failing (K, Map v term) -> RWS () () () (Failing (K, Map v term))
forall a. a -> RWST () () () Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Failing (K, Map v term) -> RWS () () () (Failing (K, Map v term)))
-> ([[Char]] -> Failing (K, Map v term))
-> [[Char]]
-> RWS () () () (Failing (K, Map v term))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Char]] -> Failing (K, Map v term)
forall a. [[Char]] -> Failing a
Failure) (\Map v term
env' -> (K, Map v term) -> RWS () () () (Failing (K, Map v term))
cont (K
k, Map v term
env')) (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 (JL formula -> JL formula -> StateT (Map v term) Failing ()
forall lit1 lit2 atom1 atom2 (m :: * -> *) term v.
(IsLiteral lit1, JustLiteral lit2, HasApply atom1, HasApply atom2,
 Unify m (atom1, atom2), term ~ UTermOf (atom1, atom2),
 v ~ TVarOf term, atom1 ~ AtomOf lit1, term ~ TermOf atom1,
 atom2 ~ AtomOf lit2, term ~ TermOf atom2, MonadFail m) =>
lit1 -> lit2 -> StateT (Map v term) m ()
unify_complements JL formula
fm' JL formula
l) Map v term
env)

tabrefute :: (IsFirstOrder formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
              atom ~ AtomOf formula, term ~ TermOf atom, v ~ TVarOf term) =>
             Maybe Depth -> [formula] -> Failing ((K, Map v term), Depth)
tabrefute :: forall formula atom term v.
(IsFirstOrder formula, Unify Failing (atom, atom),
 term ~ UTermOf (atom, atom), atom ~ AtomOf formula,
 term ~ TermOf atom, v ~ TVarOf term) =>
Maybe Depth -> [formula] -> Failing ((K, Map v term), Depth)
tabrefute Maybe Depth
limit [formula]
fms =
    let r :: Failing (((K, Map v term), Depth), Depth)
r = (Depth -> Failing ((K, Map v term), Depth))
-> Depth
-> Maybe Depth
-> Failing (((K, Map v term), Depth), Depth)
forall t.
(Depth -> Failing t) -> Depth -> Maybe Depth -> Failing (t, Depth)
deepen (\Depth
n -> (,Depth
n) ((K, Map v term) -> ((K, Map v term), Depth))
-> Failing (K, Map v term) -> Failing ((K, Map v term), Depth)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RWS () () () (Failing (K, Map v term))
-> () -> () -> Failing (K, Map v term)
forall r s a. RWS r () s a -> r -> s -> a
evalRS ([formula] -> Depth -> RWS () () () (Failing (K, Map v term))
forall formula atom term v function.
(IsFirstOrder formula, Unify Failing (atom, atom),
 term ~ UTermOf (atom, atom), atom ~ AtomOf formula,
 term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term) =>
[formula] -> Depth -> RWS () () () (Failing (K, Map v term))
tableau [formula]
fms Depth
n) () ()) (Int -> Depth
Depth Int
0) Maybe Depth
limit in
    ([[Char]] -> Failing ((K, Map v term), Depth))
-> ((((K, Map v term), Depth), Depth)
    -> Failing ((K, Map v term), Depth))
-> Failing (((K, Map v term), Depth), Depth)
-> Failing ((K, Map v term), Depth)
forall b a. ([[Char]] -> b) -> (a -> b) -> Failing a -> b
failing [[Char]] -> Failing ((K, Map v term), Depth)
forall a. [[Char]] -> Failing a
Failure (((K, Map v term), Depth) -> Failing ((K, Map v term), Depth)
forall a. a -> Failing a
Success (((K, Map v term), Depth) -> Failing ((K, Map v term), Depth))
-> ((((K, Map v term), Depth), Depth) -> ((K, Map v term), Depth))
-> (((K, Map v term), Depth), Depth)
-> Failing ((K, Map v term), Depth)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((K, Map v term), Depth), Depth) -> ((K, Map v term), Depth)
forall a b. (a, b) -> a
fst) Failing (((K, Map v term), Depth), Depth)
r

tab :: (IsFirstOrder formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Pretty formula, HasSkolem function,
        atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
        v ~ TVarOf term, v ~ SVarOf function) =>
       Maybe Depth -> formula -> Failing ((K, Map v term), Depth)
tab :: forall formula atom term function v.
(IsFirstOrder formula, Unify Failing (atom, atom),
 term ~ UTermOf (atom, atom), Pretty formula, HasSkolem function,
 atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
 v ~ TVarOf term, v ~ SVarOf function) =>
Maybe Depth -> formula -> Failing ((K, Map v term), Depth)
tab Maybe Depth
limit formula
fm =
  let sfm :: formula
sfm = SkolemT Identity function formula -> formula
forall function a.
IsFunction function =>
SkolemT Identity function a -> a
runSkolem (formula -> SkolemT Identity function formula
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(formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.)(formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
generalize formula
fm))) in
  if formula -> Maybe Bool
forall formula. IsFormula formula => formula -> Maybe Bool
asBool formula
sfm Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False then ([Char] -> Failing ((K, Map v term), Depth)
forall a. HasCallStack => [Char] -> a
error [Char]
"Tableaux.tab") else Maybe Depth -> [formula] -> Failing ((K, Map v term), Depth)
forall formula atom term v.
(IsFirstOrder formula, Unify Failing (atom, atom),
 term ~ UTermOf (atom, atom), atom ~ AtomOf formula,
 term ~ TermOf atom, v ~ TVarOf term) =>
Maybe Depth -> [formula] -> Failing ((K, Map v term), Depth)
tabrefute Maybe Depth
limit [formula
sfm]

p38 :: Test
p38 :: Test
p38 =
    let [[SkTerm] -> Formula
p, [SkTerm] -> Formula
r] = [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)
"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 Predicate
PredOf (FOL Predicate SkTerm)
"R"] :: [[SkTerm] -> Formula]
        [SkTerm
a, SkTerm
w, SkTerm
x, SkTerm
y, SkTerm
z] = [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"a", TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"w", 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]
        fm :: Formula
fm = (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"x"
               ([SkTerm] -> Formula
p[SkTerm
a] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. ([SkTerm] -> Formula
p[SkTerm
x] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"y" ([SkTerm] -> Formula
p[SkTerm
y] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. [SkTerm] -> Formula
r[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
exists V
VarOf Formula
"z" (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"w" ([SkTerm] -> Formula
p[SkTerm
z] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. [SkTerm] -> Formula
r[SkTerm
x,SkTerm
w] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. [SkTerm] -> Formula
r[SkTerm
w,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
forall formula. IsLiteral formula => formula -> formula
(.~.)([SkTerm] -> Formula
p[SkTerm
a]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. [SkTerm] -> Formula
p[SkTerm
x] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"z" (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"w" ([SkTerm] -> Formula
p[SkTerm
z] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. [SkTerm] -> Formula
r[SkTerm
x,SkTerm
w] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. [SkTerm] -> Formula
r[SkTerm
w,SkTerm
z])))) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&.
               (Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)([SkTerm] -> Formula
p[SkTerm
a]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)(VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"y" ([SkTerm] -> Formula
p[SkTerm
y] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. [SkTerm] -> Formula
r[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
exists V
VarOf Formula
"z" (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"w" ([SkTerm] -> Formula
p[SkTerm
z] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. [SkTerm] -> Formula
r[SkTerm
x,SkTerm
w] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. [SkTerm] -> Formula
r[SkTerm
w,SkTerm
z]))))))
        expected :: Failing ((K, Map k a), Depth)
expected = ((K, Map k a), Depth) -> Failing ((K, Map k a), Depth)
forall a. a -> Failing a
Success ((Int -> K
K Int
22,
                             [(k, a)] -> Map k a
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
                                      [(k
"K0",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"x" Int
1))[]),
                                       (k
"K1",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"y" Int
1))[]),
                                       (k
"K10",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"x" Int
2))[]),
                                       (k
"K11",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"z" Int
3))[a
"K13"]),
                                       (k
"K12",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"w" Int
3))[a
"K16"]),
                                       (k
"K13",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"x" Int
2))[]),
                                       (k
"K14",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"y" Int
2))[]),
                                       (k
"K15",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"y" Int
2))[]),
                                       (k
"K16",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"x" Int
2))[]),
                                       (k
"K17",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"y" Int
2))[]),
                                       (k
"K18",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"y" Int
2))[]),
                                       (k
"K19",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"x" Int
2))[]),
                                       (k
"K2",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"z" Int
1))[a
"K0"]),
                                       (k
"K20",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"y" Int
2))[]),
                                       (k
"K21",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"y" Int
2))[]),
                                       (k
"K3",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"w" Int
1))[a
"K0"]),
                                       (k
"K4",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"z" Int
1))[a
"K0"]),
                                       (k
"K5",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"w" Int
1))[a
"K0"]),
                                       (k
"K6",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"z" Int
2))[a
"K8"]),
                                       (k
"K7",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"w" Int
2))[a
"K9"]),
                                       (k
"K8",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"x" Int
2))[]),
                                       (k
"K9",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"x" Int
2))[])]
                                      ),
                            Int -> Depth
Depth Int
4) in
    Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ [Char]
-> Failing
     ((K, Map V (UTermOf (FOL Predicate SkTerm, FOL Predicate SkTerm))),
      Depth)
-> Failing
     ((K, Map V (UTermOf (FOL Predicate SkTerm, FOL Predicate SkTerm))),
      Depth)
-> Assertion
forall a.
(?loc::CallStack, Eq a, Pretty a) =>
[Char] -> a -> a -> Assertion
assertEqual' [Char]
"p38, p. 178" Failing
  ((K, Map V (UTermOf (FOL Predicate SkTerm, FOL Predicate SkTerm))),
   Depth)
forall {a} {k}.
(IsTerm a, HasSkolem (FunOf a), IsString k, Ord k) =>
Failing ((K, Map k a), Depth)
expected (Maybe Depth
-> Formula
-> Failing
     ((K, Map V (UTermOf (FOL Predicate SkTerm, FOL Predicate SkTerm))),
      Depth)
forall formula atom term function v.
(IsFirstOrder formula, Unify Failing (atom, atom),
 term ~ UTermOf (atom, atom), Pretty formula, HasSkolem function,
 atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
 v ~ TVarOf term, v ~ SVarOf function) =>
Maybe Depth -> formula -> Failing ((K, Map v term), Depth)
tab Maybe Depth
forall a. Maybe a
Nothing Formula
fm)
{-
-- -------------------------------------------------------------------------
-- Example.
-- -------------------------------------------------------------------------

START_INTERACTIVE;;
let p38 = tab
 <<(for_all x.
     P[vt "a"] .&. (P[vt "x"] .=>. (exists y. P[vt "y"] .&. R(x,y))) .=>.
     (exists z w. P[vt "z"] .&. R(x,w) .&. R(w,z))) .<=>.
   (for_all x.
     (~P[vt "a"] .|. P[vt "x"] .|. (exists z w. P[vt "z"] .&. R(x,w) .&. R(w,z))) .&.
     (~P[vt "a"] .|. ~(exists y. P[vt "y"] .&. R(x,y)) .|.
     (exists z w. P[vt "z"] .&. R(x,w) .&. R(w,z))))>>;;
END_INTERACTIVE;;
-}

-- -------------------------------------------------------------------------
-- Try to split up the initial formula first; often a big improvement.
-- -------------------------------------------------------------------------
splittab :: forall formula atom term v function.
            (IsFirstOrder formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Ord formula, Pretty formula, HasSkolem function,
             atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
             v ~ TVarOf term, v ~ SVarOf function) =>
            formula -> [Failing ((K, Map v term), Depth)]
splittab :: forall formula atom term v function.
(IsFirstOrder formula, Unify Failing (atom, atom),
 term ~ UTermOf (atom, atom), Ord formula, Pretty formula,
 HasSkolem function, atom ~ AtomOf formula, term ~ TermOf atom,
 function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) =>
formula -> [Failing ((K, Map v term), Depth)]
splittab formula
fm =
    (([formula] -> Failing ((K, Map v term), Depth))
-> [[formula]] -> [Failing ((K, Map v term), Depth)]
forall a b. (a -> b) -> [a] -> [b]
List.map (Maybe Depth -> [formula] -> Failing ((K, Map v term), Depth)
forall formula atom term v.
(IsFirstOrder formula, Unify Failing (atom, atom),
 term ~ UTermOf (atom, atom), atom ~ AtomOf formula,
 term ~ TermOf atom, v ~ TVarOf term) =>
Maybe Depth -> [formula] -> Failing ((K, Map v term), Depth)
tabrefute Maybe Depth
forall a. Maybe a
Nothing) ([[formula]] -> [Failing ((K, Map v term), Depth)])
-> (formula -> [[formula]])
-> formula
-> [Failing ((K, Map v term), Depth)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (Set formula) -> [[formula]]
forall {a}. Set (Set a) -> [[a]]
ssll (Set (Set formula) -> [[formula]])
-> (formula -> Set (Set formula)) -> formula -> [[formula]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. formula -> Set (Set formula)
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' (formula -> Set (Set formula))
-> (formula -> formula) -> formula -> Set (Set formula)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SkolemT Identity function formula -> formula
forall function a.
IsFunction function =>
SkolemT Identity function a -> a
runSkolem (SkolemT Identity function formula -> formula)
-> (formula -> SkolemT Identity function formula)
-> formula
-> formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. formula -> SkolemT Identity function formula
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 (formula -> SkolemT Identity function formula)
-> (formula -> formula)
-> formula
-> SkolemT Identity function formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) (formula -> formula) -> (formula -> formula) -> formula -> formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
generalize) formula
fm
    where ssll :: Set (Set a) -> [[a]]
ssll = (Set a -> [a]) -> [Set a] -> [[a]]
forall a b. (a -> b) -> [a] -> [b]
List.map Set a -> [a]
forall a. Set a -> [a]
Set.toList ([Set a] -> [[a]])
-> (Set (Set a) -> [Set a]) -> Set (Set a) -> [[a]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (Set a) -> [Set a]
forall a. Set a -> [a]
Set.toList
          -- simpdnf' :: PFormula atom -> Set (Set (LFormula atom))
          -- simpdnf' = simpdnf id

{-
-- -------------------------------------------------------------------------
-- Example: the Andrews challenge.
-- -------------------------------------------------------------------------

START_INTERACTIVE;;
let p34 = splittab
 <<((exists x. for_all y. P[vt "x"] .<=>. P[vt "y"]) .<=>.
    ((exists x. Q[vt "x"]) .<=>. (for_all y. Q[vt "y"]))) .<=>.
   ((exists x. for_all y. Q[vt "x"] .<=>. Q[vt "y"]) .<=>.
    ((exists x. P[vt "x"]) .<=>. (for_all y. P[vt "y"])))>>;;

-- -------------------------------------------------------------------------
-- Another nice example from EWD 1602.
-- -------------------------------------------------------------------------

let ewd1062 = splittab
 <<(for_all x. x <= x) .&.
   (for_all x y z. x <= y .&. y <= z .=>. x <= z) .&.
   (for_all x y. f[vt "x"] <= y .<=>. x <= g[vt "y"])
   .=>. (for_all x y. x <= y .=>. f[vt "x"] <= f[vt "y"]) .&.
       (for_all x y. x <= y .=>. g[vt "x"] <= g[vt "y"])>>;;
END_INTERACTIVE;;

-- -------------------------------------------------------------------------
-- Do all the equality-free Pelletier problems, and more, as examples.
-- -------------------------------------------------------------------------

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

let p1 = time splittab
 <<p .=>. q .<=>. ~q .=>. ~p>>;;

let p2 = time splittab
 <<~ ~p .<=>. p>>;;

let p3 = time splittab
 <<~(p .=>. q) .=>. q .=>. p>>;;

let p4 = time splittab
 <<~p .=>. q .<=>. ~q .=>. p>>;;

let p5 = time splittab
 <<(p .|. q .=>. p .|. r) .=>. p .|. (q .=>. r)>>;;

let p6 = time splittab
 <<p .|. ~p>>;;

let p7 = time splittab
 <<p .|. ~ ~ ~p>>;;

let p8 = time splittab
 <<((p .=>. q) .=>. p) .=>. p>>;;

let p9 = time splittab
 <<(p .|. q) .&. (~p .|. q) .&. (p .|. ~q) .=>. ~(~q .|. ~q)>>;;

let p10 = time splittab
 <<(q .=>. r) .&. (r .=>. p .&. q) .&. (p .=>. q .&. r) .=>. (p .<=>. q)>>;;

let p11 = time splittab
 <<p .<=>. p>>;;

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

let p13 = time splittab
 <<p .|. q .&. r .<=>. (p .|. q) .&. (p .|. r)>>;;

let p14 = time splittab
 <<(p .<=>. q) .<=>. (q .|. ~p) .&. (~q .|. p)>>;;

let p15 = time splittab
 <<p .=>. q .<=>. ~p .|. q>>;;

let p16 = time splittab
 <<(p .=>. q) .|. (q .=>. p)>>;;

let p17 = time splittab
 <<p .&. (q .=>. r) .=>. s .<=>. (~p .|. q .|. s) .&. (~p .|. ~r .|. s)>>;;

-- -------------------------------------------------------------------------
-- Pelletier problems: monadic predicate logic.
-- -------------------------------------------------------------------------

let p18 = time splittab
 <<exists y. for_all x. P[vt "y"] .=>. P[vt "x"]>>;;

let p19 = time splittab
 <<exists x. for_all y z. (P[vt "y"] .=>. Q[vt "z"]) .=>. P[vt "x"] .=>. Q[vt "x"]>>;;

let p20 = time splittab
 <<(for_all x y. exists z. for_all w. P[vt "x"] .&. Q[vt "y"] .=>. R[vt "z"] .&. U[vt "w"])
   .=>. (exists x y. P[vt "x"] .&. Q[vt "y"]) .=>. (exists z. R[vt "z"])>>;;

let p21 = time splittab
 <<(exists x. P .=>. Q[vt "x"]) .&. (exists x. Q[vt "x"] .=>. P)
   .=>. (exists x. P .<=>. Q[vt "x"])>>;;

let p22 = time splittab
 <<(for_all x. P .<=>. Q[vt "x"]) .=>. (P .<=>. (for_all x. Q[vt "x"]))>>;;

let p23 = time splittab
 <<(for_all x. P .|. Q[vt "x"]) .<=>. P .|. (for_all x. Q[vt "x"])>>;;

let p24 = time splittab
 <<~(exists x. U[vt "x"] .&. Q[vt "x"]) .&.
   (for_all x. P[vt "x"] .=>. Q[vt "x"] .|. R[vt "x"]) .&.
   ~(exists x. P[vt "x"] .=>. (exists x. Q[vt "x"])) .&.
   (for_all x. Q[vt "x"] .&. R[vt "x"] .=>. U[vt "x"]) .=>.
   (exists x. P[vt "x"] .&. R[vt "x"])>>;;

let p25 = time splittab
 <<(exists x. P[vt "x"]) .&.
   (for_all x. U[vt "x"] .=>. ~G[vt "x"] .&. R[vt "x"]) .&.
   (for_all x. P[vt "x"] .=>. G[vt "x"] .&. U[vt "x"]) .&.
   ((for_all x. P[vt "x"] .=>. Q[vt "x"]) .|. (exists x. Q[vt "x"] .&. P[vt "x"]))
   .=>. (exists x. Q[vt "x"] .&. P[vt "x"])>>;;

let p26 = time splittab
 <<((exists x. P[vt "x"]) .<=>. (exists x. Q[vt "x"])) .&.
   (for_all x y. P[vt "x"] .&. Q[vt "y"] .=>. (R[vt "x"] .<=>. U[vt "y"]))
   .=>. ((for_all x. P[vt "x"] .=>. R[vt "x"]) .<=>. (for_all x. Q[vt "x"] .=>. U[vt "x"]))>>;;

let p27 = time splittab
 <<(exists x. P[vt "x"] .&. ~Q[vt "x"]) .&.
   (for_all x. P[vt "x"] .=>. R[vt "x"]) .&.
   (for_all x. U[vt "x"] .&. V[vt "x"] .=>. P[vt "x"]) .&.
   (exists x. R[vt "x"] .&. ~Q[vt "x"])
   .=>. (for_all x. U[vt "x"] .=>. ~R[vt "x"])
       .=>. (for_all x. U[vt "x"] .=>. ~V[vt "x"])>>;;

let p28 = time splittab
 <<(for_all x. P[vt "x"] .=>. (for_all x. Q[vt "x"])) .&.
   ((for_all x. Q[vt "x"] .|. R[vt "x"]) .=>. (exists x. Q[vt "x"] .&. R[vt "x"])) .&.
   ((exists x. R[vt "x"]) .=>. (for_all x. L[vt "x"] .=>. M[vt "x"])) .=>.
   (for_all x. P[vt "x"] .&. L[vt "x"] .=>. M[vt "x"])>>;;

let p29 = time splittab
 <<(exists x. P[vt "x"]) .&. (exists x. G[vt "x"]) .=>.
   ((for_all x. P[vt "x"] .=>. H[vt "x"]) .&. (for_all x. G[vt "x"] .=>. J[vt "x"]) .<=>.
    (for_all x y. P[vt "x"] .&. G[vt "y"] .=>. H[vt "x"] .&. J[vt "y"]))>>;;

let p30 = time splittab
 <<(for_all x. P[vt "x"] .|. G[vt "x"] .=>. ~H[vt "x"]) .&.
   (for_all x. (G[vt "x"] .=>. ~U[vt "x"]) .=>. P[vt "x"] .&. H[vt "x"])
   .=>. (for_all x. U[vt "x"])>>;;

let p31 = time splittab
 <<~(exists x. P[vt "x"] .&. (G[vt "x"] .|. H[vt "x"])) .&.
   (exists x. Q[vt "x"] .&. P[vt "x"]) .&.
   (for_all x. ~H[vt "x"] .=>. J[vt "x"])
   .=>. (exists x. Q[vt "x"] .&. J[vt "x"])>>;;

let p32 = time splittab
 <<(for_all x. P[vt "x"] .&. (G[vt "x"] .|. H[vt "x"]) .=>. Q[vt "x"]) .&.
   (for_all x. Q[vt "x"] .&. H[vt "x"] .=>. J[vt "x"]) .&.
   (for_all x. R[vt "x"] .=>. H[vt "x"])
   .=>. (for_all x. P[vt "x"] .&. R[vt "x"] .=>. J[vt "x"])>>;;

let p33 = time splittab
 <<(for_all x. P[vt "a"] .&. (P[vt "x"] .=>. P[vt "b"]) .=>. P[vt "c"]) .<=>.
   (for_all x. P[vt "a"] .=>. P[vt "x"] .|. P[vt "c"]) .&. (P[vt "a"] .=>. P[vt "b"] .=>. P[vt "c"])>>;;

let p34 = time splittab
 <<((exists x. for_all y. P[vt "x"] .<=>. P[vt "y"]) .<=>.
    ((exists x. Q[vt "x"]) .<=>. (for_all y. Q[vt "y"]))) .<=>.
   ((exists x. for_all y. Q[vt "x"] .<=>. Q[vt "y"]) .<=>.
    ((exists x. P[vt "x"]) .<=>. (for_all y. P[vt "y"])))>>;;

let p35 = time splittab
 <<exists x y. P(x,y) .=>. (for_all x y. P(x,y))>>;;

-- -------------------------------------------------------------------------
-- Full predicate logic (without identity and functions).
-- -------------------------------------------------------------------------

let p36 = time splittab
 <<(for_all x. exists y. P(x,y)) .&.
   (for_all x. exists y. G(x,y)) .&.
   (for_all x y. P(x,y) .|. G(x,y)
   .=>. (for_all z. P(y,z) .|. G(y,z) .=>. H(x,z)))
       .=>. (for_all x. exists y. H(x,y))>>;;

let p37 = time splittab
 <<(for_all z.
     exists w. for_all x. exists y. (P(x,z) .=>. P(y,w)) .&. P(y,z) .&.
     (P(y,w) .=>. (exists u. Q(u,w)))) .&.
   (for_all x z. ~P(x,z) .=>. (exists y. Q(y,z))) .&.
   ((exists x y. Q(x,y)) .=>. (for_all x. R(x,x))) .=>.
   (for_all x. exists y. R(x,y))>>;;

let p38 = time splittab
 <<(for_all x.
     P[vt "a"] .&. (P[vt "x"] .=>. (exists y. P[vt "y"] .&. R(x,y))) .=>.
     (exists z w. P[vt "z"] .&. R(x,w) .&. R(w,z))) .<=>.
   (for_all x.
     (~P[vt "a"] .|. P[vt "x"] .|. (exists z w. P[vt "z"] .&. R(x,w) .&. R(w,z))) .&.
     (~P[vt "a"] .|. ~(exists y. P[vt "y"] .&. R(x,y)) .|.
     (exists z w. P[vt "z"] .&. R(x,w) .&. R(w,z))))>>;;

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

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

let p41 = time splittab
 <<(for_all z. exists y. for_all x. P(x,y) .<=>. P(x,z) .&. ~P(x,x))
  .=>. ~(exists z. for_all x. P(x,z))>>;;

let p42 = time splittab
 <<~(exists y. for_all x. P(x,y) .<=>. ~(exists z. P(x,z) .&. P(z,x)))>>;;

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

let p44 = time splittab
 <<(for_all x. P[vt "x"] .=>. (exists y. G[vt "y"] .&. H(x,y)) .&.
   (exists y. G[vt "y"] .&. ~H(x,y))) .&.
   (exists x. J[vt "x"] .&. (for_all y. G[vt "y"] .=>. H(x,y))) .=>.
   (exists x. J[vt "x"] .&. ~P[vt "x"])>>;;

let p45 = time splittab
 <<(for_all x.
     P[vt "x"] .&. (for_all y. G[vt "y"] .&. H(x,y) .=>. J(x,y)) .=>.
       (for_all y. G[vt "y"] .&. H(x,y) .=>. R[vt "y"])) .&.
   ~(exists y. L[vt "y"] .&. R[vt "y"]) .&.
   (exists x. P[vt "x"] .&. (for_all y. H(x,y) .=>.
     L[vt "y"]) .&. (for_all y. G[vt "y"] .&. H(x,y) .=>. J(x,y))) .=>.
   (exists x. P[vt "x"] .&. ~(exists y. G[vt "y"] .&. H(x,y)))>>;;

let p46 = time splittab
 <<(for_all x. P[vt "x"] .&. (for_all y. P[vt "y"] .&. H(y,x) .=>. G[vt "y"]) .=>. G[vt "x"]) .&.
   ((exists x. P[vt "x"] .&. ~G[vt "x"]) .=>.
    (exists x. P[vt "x"] .&. ~G[vt "x"] .&.
               (for_all y. P[vt "y"] .&. ~G[vt "y"] .=>. J(x,y)))) .&.
   (for_all x y. P[vt "x"] .&. P[vt "y"] .&. H(x,y) .=>. ~J(y,x)) .=>.
   (for_all x. P[vt "x"] .=>. G[vt "x"])>>;;

-- -------------------------------------------------------------------------
-- Well-known "Agatha" example; cf. Manthey and Bry, CADE-9.
-- -------------------------------------------------------------------------

let p55 = time splittab
 <<lives(agatha) .&. lives(butler) .&. lives(charles) .&.
   (killed(agatha,agatha) .|. killed(butler,agatha) .|.
    killed(charles,agatha)) .&.
   (for_all x y. killed(x,y) .=>. hates(x,y) .&. ~richer(x,y)) .&.
   (for_all x. hates(agatha,x) .=>. ~hates(charles,x)) .&.
   (hates(agatha,agatha) .&. hates(agatha,charles)) .&.
   (for_all x. lives[vt "x"] .&. ~richer(x,agatha) .=>. hates(butler,x)) .&.
   (for_all x. hates(agatha,x) .=>. hates(butler,x)) .&.
   (for_all x. ~hates(x,agatha) .|. ~hates(x,butler) .|. ~hates(x,charles))
   .=>. killed(agatha,agatha) .&.
       ~killed(butler,agatha) .&.
       ~killed(charles,agatha)>>;;

let p57 = time splittab
 <<P(f([vt "a"],b),f(b,c)) .&.
   P(f(b,c),f(a,c)) .&.
   (for_all [vt "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 splittab
 <<for_all P Q R. for_all x. exists v. exists w. for_all y. for_all z.
    ((P[vt "x"] .&. Q[vt "y"]) .=>. ((P[vt "v"] .|. R[vt "w"])  .&. (R[vt "z"] .=>. Q[vt "v"])))>>;;

let p59 = time splittab
 <<(for_all x. P[vt "x"] .<=>. ~P(f[vt "x"])) .=>. (exists x. P[vt "x"] .&. ~P(f[vt "x"]))>>;;

let p60 = time splittab
 <<for_all x. P(x,f[vt "x"]) .<=>.
            exists y. (for_all z. P(z,y) .=>. P(z,f[vt "x"])) .&. P(x,y)>>;;

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

{- **** This is still too hard for us! Amazing...

let gilmore_1 = time splittab
 <<exists x. for_all y z.
      ((F[vt "y"] .=>. G[vt "y"]) .<=>. F[vt "x"]) .&.
      ((F[vt "y"] .=>. H[vt "y"]) .<=>. G[vt "x"]) .&.
      (((F[vt "y"] .=>. G[vt "y"]) .=>. H[vt "y"]) .<=>. H[vt "x"])
      .=>. F[vt "z"] .&. G[vt "z"] .&. H[vt "z"]>>;;

 ***** -}

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

let gilmore_2 = time splittab
 <<exists x y. for_all 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 splittab
 <<exists x. for_all y z.
        ((F(y,z) .=>. (G[vt "y"] .=>. H[vt "x"])) .=>. F(x,x)) .&.
        ((F(z,x) .=>. G[vt "x"]) .=>. H[vt "z"]) .&.
        F(x,y)
        .=>. F(z,z)>>;;

let gilmore_4 = time splittab
 <<exists x 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))>>;;

let gilmore_5 = time splittab
 <<(for_all x. exists y. F(x,y) .|. F(y,x)) .&.
   (for_all x y. F(y,x) .=>. F(y,y))
   .=>. exists z. F(z,z)>>;;

let gilmore_6 = time splittab
 <<for_all x. exists y.
        (exists u. for_all v. F(u,x) .=>. G(v,u) .&. G(u,x))
        .=>. (exists u. for_all v. F(u,y) .=>. G(v,u) .&. G(u,y)) .|.
            (for_all u v. exists w. G(v,u) .|. H(w,y,u) .=>. G(u,w))>>;;

let gilmore_7 = time splittab
 <<(for_all x. K[vt "x"] .=>. exists y. L[vt "y"] .&. (F(x,y) .=>. G(x,y))) .&.
   (exists z. K[vt "z"] .&. for_all u. L[vt "u"] .=>. F(z,u))
   .=>. exists v w. K[vt "v"] .&. L[vt "w"] .&. G(v,w)>>;;

let gilmore_8 = time splittab
 <<exists x. for_all y z.
        ((F(y,z) .=>. (G[vt "y"] .=>. (for_all u. exists v. H(u,v,x)))) .=>. F(x,x)) .&.
        ((F(z,x) .=>. G[vt "x"]) .=>. (for_all u. exists v. H(u,v,z))) .&.
        F(x,y)
        .=>. F(z,z)>>;;

let gilmore_9 = time splittab
 <<for_all x. exists y. for_all z.
        ((for_all u. exists v. F(y,u,v) .&. G(y,u) .&. ~H(y,x))
          .=>. (for_all u. exists v. F(x,u,v) .&. G(z,u) .&. ~H(x,z))
          .=>. (for_all u. exists v. F(x,u,v) .&. G(y,u) .&. ~H(x,y))) .&.
        ((for_all u. exists v. F(x,u,v) .&. G(y,u) .&. ~H(x,y))
         .=>. ~(for_all u. exists v. F(x,u,v) .&. G(z,u) .&. ~H(x,z))
         .=>. (for_all u. exists v. F(y,u,v) .&. G(y,u) .&. ~H(y,x)) .&.
             (for_all 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 splittab
 <<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)))>>;;

************ -}

-}

testTableaux :: Test
testTableaux :: Test
testTableaux = [Char] -> Test -> Test
TestLabel [Char]
"Tableaux" ([Test] -> Test
TestList [Test
p20, Test
p19, Test
p38])