-- | Model elimination procedure (MESON version, based on Stickel's PTTP).
--
-- Copyright (c) 2003-2007, John Harrison. (See "LICENSE.txt" for details.)

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -Wall #-}

module Data.Logic.ATP.Meson
    ( meson1
    , meson2
    , meson
    , testMeson
    ) where

import Control.Monad.State (execStateT)
import Data.Logic.ATP.Apply (HasApply(TermOf, PredOf), pApp)
import Data.Logic.ATP.FOL (generalize, IsFirstOrder)
import Data.Logic.ATP.Formulas (false, IsFormula(AtomOf))
import Data.Logic.ATP.Lib (Depth(Depth), deepen, Failing(Failure, Success), setAll, settryfind)
import Data.Logic.ATP.Lit ((.~.), JustLiteral, LFormula, negative)
import Data.Logic.ATP.Parser (fof)
import Data.Logic.ATP.Pretty (assertEqual', prettyShow, testEquals)
import Data.Logic.ATP.Prolog (PrologRule(Prolog), renamerule)
import Data.Logic.ATP.Prop ((.&.), (.|.), (.=>.), list_conj, PFormula, simpcnf)
import Data.Logic.ATP.Quantified (exists, for_all, IsQuantified(VarOf))
import Data.Logic.ATP.Resolution (davis_putnam_example_formula)
import Data.Logic.ATP.Skolem (askolemize, Formula, HasSkolem(SVarOf), pnf, runSkolem, SkolemT, simpdnf', specialize, toSkolem)
import Data.Logic.ATP.Tableaux (K(K), tab)
import Data.Logic.ATP.Term (fApp, IsTerm(FunOf, TVarOf), vt)
import Data.Logic.ATP.Unif (Unify(UTermOf), unify_literals)
import Data.Map.Strict as Map
import Data.Set as Set
import Test.HUnit

test03 :: Test
test03 :: Test
test03 = let fm :: Formula
fm = [fof| ∀a. ¬(P(a)∧(∀y. (∀z. Q(y)∨R(z))∧¬P(a))) |] in
         $(testEquals "TAB 1") (((K, Map V (UTermOf (FOL Predicate SkTerm, FOL Predicate SkTerm))),
 Depth)
-> Failing
     ((K, Map V (UTermOf (FOL Predicate SkTerm, FOL Predicate SkTerm))),
      Depth)
forall a. a -> Failing a
Success ((Int -> K
K Int
2, Map V (UTermOf (FOL Predicate SkTerm, FOL Predicate SkTerm))
forall k a. Map k a
Map.empty),Int -> Depth
Depth Int
2)) (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)

test04 :: Test
test04 :: Test
test04 = let fm :: Formula
fm = [fof| ∀a. ¬(P(a)∧¬P(a)∧(∀y z. Q(y)∨R(z))) |] in
         $(testEquals "TAB 2") (((K, Map V (UTermOf (FOL Predicate SkTerm, FOL Predicate SkTerm))),
 Depth)
-> Failing
     ((K, Map V (UTermOf (FOL Predicate SkTerm, FOL Predicate SkTerm))),
      Depth)
forall a. a -> Failing a
Success ((Int -> K
K Int
0, Map V (UTermOf (FOL Predicate SkTerm, FOL Predicate SkTerm))
forall k a. Map k a
Map.empty),Int -> Depth
Depth Int
0)) (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)

        {- fm3 = [fof| ¬p ∧ (p ∨ q) ∧ (r ∨ s) ∧ (¬q ∨ t ∨ u) ∧
                    (¬r ∨ ¬t) ∧ (¬r ∨ ¬u) ∧ (¬q ∨ v ∨ w) ∧
               (¬s ∨ ¬v) ∧ (¬s ∨ ¬w) |] -}

{-
START_INTERACTIVE;;
tab <<forall a. ~(P(a) /\ (forall y z. Q(y) \/ R(z)) /\ ~P(a))>>;;

tab <<forall a. ~(P(a) /\ ~P(a) /\ (forall y z. Q(y) \/ R(z)))>>;;

(* ------------------------------------------------------------------------- *)
(* The interesting example where tableaux connections make the proof longer. *)
(* Unfortuntely this gets hammered by normalization first...                 *)
(* ------------------------------------------------------------------------- *)

tab <<~p /\ (p \/ q) /\ (r \/ s) /\ (~q \/ t \/ u) /\
      (~r \/ ~t) /\ (~r \/ ~u) /\ (~q \/ v \/ w) /\
      (~s \/ ~v) /\ (~s \/ ~w) ==> false>>;;
END_INTERACTIVE;;
-}
-- -------------------------------------------------------------------------
-- Example of naivety of tableau prover.
-- -------------------------------------------------------------------------

test05 :: Test
test05 :: Test
test05 = $(testEquals "test001") (((K, Map V (UTermOf (FOL Predicate SkTerm, FOL Predicate SkTerm))),
 Depth)
-> Failing
     ((K, Map V (UTermOf (FOL Predicate SkTerm, FOL Predicate SkTerm))),
      Depth)
forall a. a -> Failing a
Success ((Int -> K
K Int
0, Map V (UTermOf (FOL Predicate SkTerm, FOL Predicate SkTerm))
forall k a. Map k a
Map.empty), Int -> Depth
Depth Int
0))
         (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 [fof| ¬p∧(p∨q)∧(r∨s)∧(¬q∨t∨u)∧(¬r∨¬t)∧(¬r∨¬u)∧(¬q∨v∨w)∧(¬s∨¬v)∧(¬s∨¬w)⇒⊥|])

test01 :: Test
test01 :: Test
test01 = String -> Test -> Test
TestLabel String
"Meson 1" (Test -> Test) -> Test -> Test
forall a b. (a -> b) -> a -> b
$ Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ String -> Set (Failing Depth) -> Set (Failing Depth) -> Assertion
forall a.
(?loc::CallStack, Eq a, Pretty a) =>
String -> a -> a -> Assertion
assertEqual' String
"meson dp example (p. 220)" Set (Failing Depth)
expected Set (Failing Depth)
input
    where input :: Set (Failing Depth)
input = SkolemT Identity Function (Set (Failing Depth))
-> Set (Failing Depth)
forall function a.
IsFunction function =>
SkolemT Identity function a -> a
runSkolem (Maybe Depth
-> Formula -> SkolemT Identity Function (Set (Failing Depth))
forall fof atom term function (m :: * -> *) v.
(IsFirstOrder fof, Unify Failing (atom, atom),
 term ~ UTermOf (atom, atom), HasSkolem function, Monad m, Ord fof,
 atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term,
 v ~ VarOf fof, v ~ SVarOf function) =>
Maybe Depth -> fof -> SkolemT m function (Set (Failing Depth))
meson (Depth -> Maybe Depth
forall a. a -> Maybe a
Just (Int -> Depth
Depth Int
10)) (Formula
davis_putnam_example_formula :: Formula))
          expected :: Set (Failing Depth)
          expected :: Set (Failing Depth)
expected = Failing Depth -> Set (Failing Depth)
forall a. a -> Set a
Set.singleton (Depth -> Failing Depth
forall a. a -> Failing a
Success (Int -> Depth
Depth Int
8))

test06 :: Test
test06 :: Test
test06 = $(testEquals "meson dp example, step 1 (p. 220)") [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))) |]
           Formula
davis_putnam_example_formula

test02 :: Test
test02 :: Test
test02 =
    String -> Test -> Test
TestLabel String
"Meson 2" (Test -> Test) -> Test -> Test
forall a b. (a -> b) -> a -> b
$
    [Test] -> Test
TestList [Assertion -> Test
TestCase (String -> Formula -> Formula -> Assertion
forall a.
(?loc::CallStack, Eq a, Pretty a) =>
String -> a -> a -> Assertion
assertEqual' String
"meson dp example, step 2 (p. 220)"
                                    (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" (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"z" ((([TermOf (AtomOf Formula)] -> Formula
f [SkTerm
TermOf (AtomOf Formula)
x,SkTerm
TermOf (AtomOf Formula)
y]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. (([TermOf (AtomOf Formula)] -> Formula
f [SkTerm
TermOf (AtomOf Formula)
y,SkTerm
TermOf (AtomOf Formula)
z]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. ([TermOf (AtomOf Formula)] -> Formula
f [SkTerm
TermOf (AtomOf Formula)
z,SkTerm
TermOf (AtomOf Formula)
z]))) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&.
                                                                                  ((([TermOf (AtomOf Formula)] -> Formula
f [SkTerm
TermOf (AtomOf Formula)
x,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,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,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,SkTerm
TermOf (AtomOf Formula)
z])))))))
                                    (Formula -> Formula
forall formula. IsFirstOrder formula => formula -> formula
generalize Formula
davis_putnam_example_formula)),
              Assertion -> Test
TestCase (String -> Formula -> Formula -> Assertion
forall a.
(?loc::CallStack, Eq a, Pretty a) =>
String -> a -> a -> Assertion
assertEqual' String
"meson dp example, step 3 (p. 220)"
                                    (Formula -> Formula
forall formula. IsLiteral 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" (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"z" ((([TermOf (AtomOf Formula)] -> Formula
f [SkTerm
TermOf (AtomOf Formula)
x,SkTerm
TermOf (AtomOf Formula)
y]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. (([TermOf (AtomOf Formula)] -> Formula
f [SkTerm
TermOf (AtomOf Formula)
y,SkTerm
TermOf (AtomOf Formula)
z]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. ([TermOf (AtomOf Formula)] -> Formula
f [SkTerm
TermOf (AtomOf Formula)
z,SkTerm
TermOf (AtomOf Formula)
z]))) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&.
                                                                                        ((([TermOf (AtomOf Formula)] -> Formula
f [SkTerm
TermOf (AtomOf Formula)
x,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,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,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,SkTerm
TermOf (AtomOf Formula)
z]))))))) :: Formula)
                                    (Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.) (Formula -> Formula
forall formula. IsFirstOrder formula => formula -> formula
generalize Formula
davis_putnam_example_formula))),
              Assertion -> Test
TestCase (String -> Formula -> Formula -> Assertion
forall a.
(?loc::CallStack, Eq a, Pretty a) =>
String -> a -> a -> Assertion
assertEqual' String
"meson dp example, step 4 (p. 220)"
                                    (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all 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
forall a b. (a -> b) -> a -> b
$
                                             [TermOf (AtomOf Formula)] -> Formula
f[SkTerm
TermOf (AtomOf Formula)
x,SkTerm
TermOf (AtomOf Formula)
y] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&.
                                             (Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)([TermOf (AtomOf Formula)] -> Formula
f[SkTerm
TermOf (AtomOf Formula)
y, [SkTerm] -> SkTerm
sk1[SkTerm
x, SkTerm
y]]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)([TermOf (AtomOf Formula)] -> Formula
f[[SkTerm] -> SkTerm
sk1[SkTerm
x,SkTerm
y], [SkTerm] -> SkTerm
sk1[SkTerm
x, SkTerm
y]]))) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                                             ([TermOf (AtomOf Formula)] -> Formula
f[SkTerm
TermOf (AtomOf Formula)
x,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,SkTerm
TermOf (AtomOf Formula)
y]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&.
                                             ((Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)([TermOf (AtomOf Formula)] -> Formula
g[SkTerm
TermOf (AtomOf Formula)
x,[SkTerm] -> SkTerm
sk1[SkTerm
x,SkTerm
y]])) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)([TermOf (AtomOf Formula)] -> Formula
g[[SkTerm] -> SkTerm
sk1[SkTerm
x,SkTerm
y], [SkTerm] -> SkTerm
sk1[SkTerm
x,SkTerm
y]]))))
                                    (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
davis_putnam_example_formula))) :: Formula)),
              Assertion -> Test
TestCase (String -> Set (Set String) -> Set (Set String) -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"meson dp example, step 5 (p. 220)"
                                    ((Set Formula -> Set String)
-> Set (Set Formula) -> Set (Set String)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((Formula -> String) -> Set Formula -> Set String
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Formula -> String
forall a. Pretty a => a -> String
prettyShow)
                                     ([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 [VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all 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
forall a b. (a -> b) -> a -> b
$
                                                     [TermOf (AtomOf Formula)] -> Formula
f[SkTerm
TermOf (AtomOf Formula)
x,SkTerm
TermOf (AtomOf Formula)
y] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&.
                                                     (Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)([TermOf (AtomOf Formula)] -> Formula
f[SkTerm
TermOf (AtomOf Formula)
y, [SkTerm] -> SkTerm
sk1[SkTerm
x, SkTerm
y]]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)([TermOf (AtomOf Formula)] -> Formula
f[[SkTerm] -> SkTerm
sk1[SkTerm
x,SkTerm
y], [SkTerm] -> SkTerm
sk1[SkTerm
x, SkTerm
y]]))) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                                                     ([TermOf (AtomOf Formula)] -> Formula
f[SkTerm
TermOf (AtomOf Formula)
x,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,SkTerm
TermOf (AtomOf Formula)
y]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&.
                                                     ((Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)([TermOf (AtomOf Formula)] -> Formula
g[SkTerm
TermOf (AtomOf Formula)
x,[SkTerm] -> SkTerm
sk1[SkTerm
x,SkTerm
y]])) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)([TermOf (AtomOf Formula)] -> Formula
g[[SkTerm] -> SkTerm
sk1[SkTerm
x,SkTerm
y], [SkTerm] -> SkTerm
sk1[SkTerm
x,SkTerm
y]])))]]))
{-
[[<<forall x y.
      F(x,y) /\
      (~F(y,f_z(x,y)) \/ ~F(f_z(x,y),f_z(x,y))) \/
      (F(x,y) /\ G(x,y)) /\
      (~G(x,f_z(x,y)) \/ ~G(f_z(x,y),f_z(x,y))) >>]]
-}
                                    ((Set Formula -> Set String)
-> Set (Set Formula) -> Set (Set String)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((Formula -> String) -> Set Formula -> Set String
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Formula -> String
forall a. Pretty a => a -> String
prettyShow) (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' (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
davis_putnam_example_formula))) :: Formula) :: Set (Set Formula)))),
              Assertion -> Test
TestCase (String -> Set String -> Set String -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"meson dp example, step 6 (p. 220)"
                                    ((Formula -> String) -> Set Formula -> Set String
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Formula -> String
forall a. Pretty a => a -> String
prettyShow
                                     ([Formula] -> Set Formula
forall a. Ord a => [a] -> Set a
Set.fromList [VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all 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
forall a b. (a -> b) -> a -> b
$
                                                    [TermOf (AtomOf Formula)] -> Formula
f[SkTerm
TermOf (AtomOf Formula)
x,SkTerm
TermOf (AtomOf Formula)
y] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&.
                                                    (Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)([TermOf (AtomOf Formula)] -> Formula
f[SkTerm
TermOf (AtomOf Formula)
y, [SkTerm] -> SkTerm
sk1[SkTerm
x, SkTerm
y]]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)([TermOf (AtomOf Formula)] -> Formula
f[[SkTerm] -> SkTerm
sk1[SkTerm
x,SkTerm
y], [SkTerm] -> SkTerm
sk1[SkTerm
x, SkTerm
y]]))) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
                                                    ([TermOf (AtomOf Formula)] -> Formula
f[SkTerm
TermOf (AtomOf Formula)
x,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,SkTerm
TermOf (AtomOf Formula)
y]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&.
                                                    ((Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)([TermOf (AtomOf Formula)] -> Formula
g[SkTerm
TermOf (AtomOf Formula)
x,[SkTerm] -> SkTerm
sk1[SkTerm
x,SkTerm
y]])) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)([TermOf (AtomOf Formula)] -> Formula
g[[SkTerm] -> SkTerm
sk1[SkTerm
x,SkTerm
y], [SkTerm] -> SkTerm
sk1[SkTerm
x,SkTerm
y]])))]))
{-
[<<forall x y.
     F(x,y) /\
     (~F(y,f_z(x,y)) \/ ~F(f_z(x,y),f_z(x,y))) \/
     (F(x,y) /\ G(x,y)) &
     (~G(x,f_z(x,y)) \/ ~G(f_z(x,y),f_z(x,y)))>>]
-}
                                    ((Formula -> String) -> Set Formula -> Set String
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Formula -> String
forall a. Pretty a => a -> String
prettyShow (((Set Formula -> Formula) -> Set (Set Formula) -> Set Formula
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Set Formula -> Formula
forall (t :: * -> *) formula.
(Foldable t, IsFormula formula, IsPropositional formula) =>
t formula -> formula
list_conj (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' (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
davis_putnam_example_formula)))))) :: Set (Formula))))]
    where f :: [TermOf (AtomOf Formula)] -> 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)
"F"
          g :: [TermOf (AtomOf Formula)] -> 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)
"G"
          sk1 :: [SkTerm] -> SkTerm
sk1 = FunOf SkTerm -> [SkTerm] -> SkTerm
forall term. IsTerm term => FunOf term -> [term] -> term
fApp (SVarOf (FunOf SkTerm) -> Int -> FunOf SkTerm
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf SkTerm)
"z" Int
1)
          x :: SkTerm
x = TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
"x"
          y :: SkTerm
y = TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
"y"
          z :: SkTerm
z = TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
"z"

{-
askolemize (simpdnf (generalize davis_putnam_example_formula)) ->
 <<forall x y. F(x,y) /\ (~F(y,f_z(x,y)) \/ ~F(f_z(x,y), f_z(x,y))) \/ (F(x,y) /\ G(x,y)) /\ (~G(x,f_z(x,y)) \/ ~G(f_z(x,y),f_z(x,y)))>>
-}

{-
START_INTERACTIVE;;
tab <<forall a. ~(P(a) /\ (forall y z. Q(y) \/ R(z)) /\ ~P(a))>>;;

tab <<forall a. ~(P(a) /\ ~P(a) /\ (forall y z. Q(y) \/ R(z)))>>;;

-- -------------------------------------------------------------------------
-- The interesting example where tableaux connections make the proof longer.
-- Unfortuntely this gets hammered by normalization first...
-- -------------------------------------------------------------------------

tab <<~p /\ (p \/ q) /\ (r \/ s) /\ (~q \/ t \/ u) /\
      (~r \/ ~t) /\ (~r \/ ~u) /\ (~q \/ v \/ w) /\
      (~s \/ ~v) /\ (~s \/ ~w) ==> false>>;;
END_INTERACTIVE;;
-}

-- -------------------------------------------------------------------------
-- Generation of contrapositives.
-- -------------------------------------------------------------------------

contrapositives :: (JustLiteral lit, Ord lit) => Set lit -> Set (PrologRule lit)
contrapositives :: forall lit.
(JustLiteral lit, Ord lit) =>
Set lit -> Set (PrologRule lit)
contrapositives Set lit
cls =
    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
negative Set lit
cls then PrologRule lit -> Set (PrologRule lit) -> Set (PrologRule lit)
forall a. Ord a => a -> Set a -> Set a
Set.insert (Set lit -> lit -> PrologRule lit
forall lit. Set lit -> lit -> PrologRule lit
Prolog ((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
cls) lit
forall formula. IsFormula formula => formula
false) Set (PrologRule lit)
base else Set (PrologRule lit)
base
    where base :: Set (PrologRule lit)
base = (lit -> PrologRule lit) -> Set lit -> Set (PrologRule lit)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\ lit
c -> (Set lit -> lit -> PrologRule lit
forall lit. Set lit -> lit -> PrologRule lit
Prolog ((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
(.~.) (lit -> Set lit -> Set lit
forall a. Ord a => a -> Set a -> Set a
Set.delete lit
c Set lit
cls)) lit
c)) Set lit
cls

-- -------------------------------------------------------------------------
-- The core of MESON: ancestor unification or Prolog-style extension.
-- -------------------------------------------------------------------------

mexpand1 :: (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 (PrologRule lit)
        -> Set lit
        -> lit
        -> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int))
        -> (Map v term, Int, Int)
        -> Failing (Map v term, Int, Int)
mexpand1 :: 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 (PrologRule lit)
-> Set lit
-> lit
-> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int))
-> (Map v term, Int, Int)
-> Failing (Map v term, Int, Int)
mexpand1 Set (PrologRule lit)
rules Set lit
ancestors lit
g (Map v term, Int, Int) -> Failing (Map v term, Int, Int)
cont (Map v term
env,Int
n,Int
k) =
    if Int -> Int
forall a. Enum a => a -> Int
fromEnum Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
    then [String] -> Failing (Map v term, Int, Int)
forall a. [String] -> Failing a
Failure [String
"Too deep"]
    else case (lit -> Failing (Map v term, Int, Int))
-> Set lit -> Failing (Map v term, Int, Int)
forall t a. (t -> Failing a) -> Set t -> Failing a
settryfind lit -> Failing (Map v term, Int, Int)
doAncestor Set lit
ancestors of
           Success (Map v term, Int, Int)
a -> (Map v term, Int, Int) -> Failing (Map v term, Int, Int)
forall a. a -> Failing a
Success (Map v term, Int, Int)
a
           Failure [String]
_ -> (PrologRule lit -> Failing (Map v term, Int, Int))
-> Set (PrologRule lit) -> Failing (Map v term, Int, Int)
forall t a. (t -> Failing a) -> Set t -> Failing a
settryfind PrologRule lit -> Failing (Map v term, Int, Int)
doRule Set (PrologRule lit)
rules
    where
      doAncestor :: lit -> Failing (Map v term, Int, Int)
doAncestor lit
a =
          do Map v term
mp <- 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
g (lit -> lit
forall formula. IsLiteral formula => formula -> formula
(.~.) lit
a)) Map v term
env
             (Map v term, Int, Int) -> Failing (Map v term, Int, Int)
cont (Map v term
mp, Int
n, Int
k)
      doRule :: PrologRule lit -> Failing (Map v term, Int, Int)
doRule PrologRule lit
rule =
          do Map v term
mp <- 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
g lit
c) Map v term
env
             (Map v term, Int, Int) -> Failing (Map v term, Int, Int)
mexpand1' (Map v term
mp, Int -> Int
forall a. Enum a => a -> Int
fromEnum Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Set lit -> Int
forall a. Set a -> Int
Set.size Set lit
asm, Int
k')
          where
            mexpand1' :: (Map v term, Int, Int) -> Failing (Map v term, Int, Int)
mexpand1' = (lit
 -> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int))
 -> (Map v term, Int, Int)
 -> Failing (Map v term, Int, Int))
-> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int))
-> Set lit
-> (Map v term, Int, Int)
-> Failing (Map v term, Int, Int)
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Set (PrologRule lit)
-> Set lit
-> lit
-> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int))
-> (Map v term, Int, Int)
-> Failing (Map v term, Int, Int)
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 (PrologRule lit)
-> Set lit
-> lit
-> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int))
-> (Map v term, Int, Int)
-> Failing (Map v term, Int, Int)
mexpand1 Set (PrologRule lit)
rules (lit -> Set lit -> Set lit
forall a. Ord a => a -> Set a -> Set a
Set.insert lit
g Set lit
ancestors)) (Map v term, Int, Int) -> Failing (Map v term, Int, Int)
cont Set lit
asm
            (Prolog Set lit
asm lit
c, Int
k') = Int -> PrologRule lit -> (PrologRule lit, Int)
forall lit atom term v.
(IsLiteral lit, JustLiteral lit, Ord lit, HasApply atom,
 IsTerm term, atom ~ AtomOf lit, term ~ TermOf atom,
 v ~ TVarOf term) =>
Int -> PrologRule lit -> (PrologRule lit, Int)
renamerule Int
k PrologRule lit
rule

-- -------------------------------------------------------------------------
-- Full MESON procedure.
-- -------------------------------------------------------------------------

puremeson1 :: forall fof atom term v function.
              (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Ord fof,
               atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term,
               v ~ VarOf fof, v ~ TVarOf term) =>
              Maybe Depth -> fof -> Failing Depth
puremeson1 :: forall fof atom term v function.
(IsFirstOrder fof, Unify Failing (atom, atom),
 term ~ UTermOf (atom, atom), Ord fof, atom ~ AtomOf fof,
 term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof,
 v ~ TVarOf term) =>
Maybe Depth -> fof -> Failing Depth
puremeson1 Maybe Depth
maxdl fof
fm =
    ((Map v term, Int, Int), Depth) -> Depth
forall a b. (a, b) -> b
snd (((Map v term, Int, Int), Depth) -> Depth)
-> Failing ((Map v term, Int, Int), Depth) -> Failing Depth
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Depth -> Failing (Map v term, Int, Int))
-> Depth -> Maybe Depth -> Failing ((Map v term, Int, Int), Depth)
forall t.
(Depth -> Failing t) -> Depth -> Maybe Depth -> Failing (t, Depth)
deepen Depth -> Failing (Map v term, Int, Int)
f (Int -> Depth
Depth Int
0) Maybe Depth
maxdl
    where
      f :: Depth -> Failing (Map v term, Int, Int)
      f :: Depth -> Failing (Map v term, Int, Int)
f Depth
n = Set (PrologRule (LFormula atom))
-> Set (LFormula atom)
-> LFormula atom
-> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int))
-> (Map v term, Int, Int)
-> Failing (Map v term, Int, Int)
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 (PrologRule lit)
-> Set lit
-> lit
-> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int))
-> (Map v term, Int, Int)
-> Failing (Map v term, Int, Int)
mexpand1 Set (PrologRule (LFormula atom))
rules (Set (LFormula atom)
forall a. Set a
Set.empty :: Set (LFormula atom)) LFormula atom
forall formula. IsFormula formula => formula
false (Map v term, Int, Int) -> Failing (Map v term, Int, Int)
forall a. a -> Failing a
forall (m :: * -> *) a. Monad m => a -> m a
return (Map v term
forall k a. Map k a
Map.empty, Depth -> Int
forall a. Enum a => a -> Int
fromEnum Depth
n, Int
0)
      rules :: Set (PrologRule (LFormula atom))
rules = (Set (LFormula atom)
 -> Set (PrologRule (LFormula atom))
 -> Set (PrologRule (LFormula atom)))
-> Set (PrologRule (LFormula atom))
-> Set (Set (LFormula atom))
-> Set (PrologRule (LFormula atom))
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Set (PrologRule (LFormula atom))
-> Set (PrologRule (LFormula atom))
-> Set (PrologRule (LFormula atom))
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Set (PrologRule (LFormula atom))
 -> Set (PrologRule (LFormula atom))
 -> Set (PrologRule (LFormula atom)))
-> (Set (LFormula atom) -> Set (PrologRule (LFormula atom)))
-> Set (LFormula atom)
-> Set (PrologRule (LFormula atom))
-> Set (PrologRule (LFormula atom))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (LFormula atom) -> Set (PrologRule (LFormula atom))
forall lit.
(JustLiteral lit, Ord lit) =>
Set lit -> Set (PrologRule lit)
contrapositives) Set (PrologRule (LFormula atom))
forall a. Set a
Set.empty Set (Set (LFormula atom))
cls
      (Set (Set (LFormula atom))
cls :: Set (Set (LFormula atom))) = (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)

meson1 :: forall m fof atom predicate term function v.
          (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Ord fof, HasSkolem function, Monad m,
           atom ~ AtomOf fof, term ~ TermOf atom, predicate ~ PredOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) =>
          Maybe Depth -> fof -> SkolemT m function (Set (Failing Depth))
meson1 :: forall (m :: * -> *) fof atom predicate term function v.
(IsFirstOrder fof, Unify Failing (atom, atom),
 term ~ UTermOf (atom, atom), Ord fof, HasSkolem function, Monad m,
 atom ~ AtomOf fof, term ~ TermOf atom, predicate ~ PredOf atom,
 function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) =>
Maybe Depth -> fof -> SkolemT m function (Set (Failing Depth))
meson1 Maybe Depth
maxdl 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 Depth)))
-> StateT (SkolemState function) m (Set (Failing Depth))
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 Depth)
-> StateT (SkolemState function) m (Set (Failing Depth))
forall a. a -> StateT (SkolemState function) m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Set (Failing Depth)
 -> StateT (SkolemState function) m (Set (Failing Depth)))
-> (fof -> Set (Failing Depth))
-> fof
-> StateT (SkolemState function) m (Set (Failing Depth))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set fof -> Failing Depth) -> Set (Set fof) -> Set (Failing Depth)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Maybe Depth -> fof -> Failing Depth
forall fof atom term v function.
(IsFirstOrder fof, Unify Failing (atom, atom),
 term ~ UTermOf (atom, atom), Ord fof, atom ~ AtomOf fof,
 term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof,
 v ~ TVarOf term) =>
Maybe Depth -> fof -> Failing Depth
puremeson1 Maybe Depth
maxdl (fof -> Failing Depth)
-> (Set fof -> fof) -> Set fof -> Failing Depth
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 Depth))
-> (fof -> Set (Set fof)) -> fof -> Set (Failing Depth)
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))

-- -------------------------------------------------------------------------
-- With repetition checking and divide-and-conquer search.
-- -------------------------------------------------------------------------

equal :: (JustLiteral lit, HasApply atom, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), IsTerm term,
          atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
         Map v term -> lit -> lit -> Bool
equal :: 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) =>
Map v term -> lit -> lit -> Bool
equal Map v term
env lit
fm1 lit
fm2 =
    case 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
fm1 lit
fm2) Map v term
env of
      Success Map v term
env' | Map v term
env Map v term -> Map v term -> Bool
forall a. Eq a => a -> a -> Bool
== Map v term
env' -> Bool
True
      Failing (Map v term)
_ -> Bool
False

expand2 :: (Set lit ->
            ((Map v term, Int, Int) -> Failing (Map v term, Int, Int)) ->
            (Map v term, Int, Int) -> Failing (Map v term, Int, Int))
        -> Set lit
        -> Int
        -> Set lit
        -> Int
        -> Int
        -> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int))
        -> Map v term
        -> Int
        -> Failing (Map v term, Int, Int)
expand2 :: forall lit v term.
(Set lit
 -> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int))
 -> (Map v term, Int, Int)
 -> Failing (Map v term, Int, Int))
-> Set lit
-> Int
-> Set lit
-> Int
-> Int
-> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int))
-> Map v term
-> Int
-> Failing (Map v term, Int, Int)
expand2 Set lit
-> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int))
-> (Map v term, Int, Int)
-> Failing (Map v term, Int, Int)
expfn Set lit
goals1 Int
n1 Set lit
goals2 Int
n2 Int
n3 (Map v term, Int, Int) -> Failing (Map v term, Int, Int)
cont Map v term
env Int
k =
    Set lit
-> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int))
-> (Map v term, Int, Int)
-> Failing (Map v term, Int, Int)
expfn Set lit
goals1 (\(Map v term
e1,Int
r1,Int
k1) ->
                      Set lit
-> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int))
-> (Map v term, Int, Int)
-> Failing (Map v term, Int, Int)
expfn Set lit
goals2 (\(Map v term
e2,Int
r2,Int
k2) ->
                                        if Int
n2 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
n3 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
r2 then [String] -> Failing (Map v term, Int, Int)
forall a. [String] -> Failing a
Failure [String
"pair"] else (Map v term, Int, Int) -> Failing (Map v term, Int, Int)
cont (Map v term
e2,Int
r2,Int
k2))
                                   (Map v term
e1,Int
n2Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
r1,Int
k1))
                 (Map v term
env,Int
n1,Int
k)

mexpand2 :: (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 (PrologRule lit)
        -> Set lit
        -> lit
        -> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int))
        -> (Map v term, Int, Int)
        -> Failing (Map v term, Int, Int)
mexpand2 :: 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 (PrologRule lit)
-> Set lit
-> lit
-> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int))
-> (Map v term, Int, Int)
-> Failing (Map v term, Int, Int)
mexpand2 Set (PrologRule lit)
rules Set lit
ancestors lit
g (Map v term, Int, Int) -> Failing (Map v term, Int, Int)
cont (Map v term
env,Int
n,Int
k) =
    if Int -> Int
forall a. Enum a => a -> Int
fromEnum Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
    then [String] -> Failing (Map v term, Int, Int)
forall a. [String] -> Failing a
Failure [String
"Too deep"]
    else if (lit -> Bool) -> Set lit -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Map v term -> lit -> lit -> Bool
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) =>
Map v term -> lit -> lit -> Bool
equal Map v term
env lit
g) Set lit
ancestors
         then [String] -> Failing (Map v term, Int, Int)
forall a. [String] -> Failing a
Failure [String
"repetition"]
         else case (lit -> Failing (Map v term, Int, Int))
-> Set lit -> Failing (Map v term, Int, Int)
forall t a. (t -> Failing a) -> Set t -> Failing a
settryfind lit -> Failing (Map v term, Int, Int)
doAncestor Set lit
ancestors of
                Success (Map v term, Int, Int)
a -> (Map v term, Int, Int) -> Failing (Map v term, Int, Int)
forall a. a -> Failing a
Success (Map v term, Int, Int)
a
                Failure [String]
_ -> (PrologRule lit -> Failing (Map v term, Int, Int))
-> Set (PrologRule lit) -> Failing (Map v term, Int, Int)
forall t a. (t -> Failing a) -> Set t -> Failing a
settryfind PrologRule lit -> Failing (Map v term, Int, Int)
doRule Set (PrologRule lit)
rules
    where
      doAncestor :: lit -> Failing (Map v term, Int, Int)
doAncestor lit
a =
          do Map v term
mp <- 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
g (lit -> lit
forall formula. IsLiteral formula => formula -> formula
(.~.) lit
a)) Map v term
env
             (Map v term, Int, Int) -> Failing (Map v term, Int, Int)
cont (Map v term
mp, Int
n, Int
k)
      doRule :: PrologRule lit -> Failing (Map v term, Int, Int)
doRule PrologRule lit
rule =
          do Map v term
mp <- 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
g lit
c) Map v term
env
             (Map v term, Int, Int) -> Failing (Map v term, Int, Int)
mexpand2' (Map v term
mp, Int -> Int
forall a. Enum a => a -> Int
fromEnum Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Set lit -> Int
forall a. Set a -> Int
Set.size Set lit
asm, Int
k')
          where
            mexpand2' :: (Map v term, Int, Int) -> Failing (Map v term, Int, Int)
mexpand2' = Set (PrologRule lit)
-> Set lit
-> Set lit
-> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int))
-> (Map v term, Int, Int)
-> Failing (Map v term, Int, Int)
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 (PrologRule lit)
-> Set lit
-> Set lit
-> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int))
-> (Map v term, Int, Int)
-> Failing (Map v term, Int, Int)
mexpands Set (PrologRule lit)
rules (lit -> Set lit -> Set lit
forall a. Ord a => a -> Set a -> Set a
Set.insert lit
g Set lit
ancestors) Set lit
asm (Map v term, Int, Int) -> Failing (Map v term, Int, Int)
cont
            (Prolog Set lit
asm lit
c, Int
k') = Int -> PrologRule lit -> (PrologRule lit, Int)
forall lit atom term v.
(IsLiteral lit, JustLiteral lit, Ord lit, HasApply atom,
 IsTerm term, atom ~ AtomOf lit, term ~ TermOf atom,
 v ~ TVarOf term) =>
Int -> PrologRule lit -> (PrologRule lit, Int)
renamerule Int
k PrologRule lit
rule

mexpands :: (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 (PrologRule lit)
         -> Set lit
         -> Set lit
         -> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int))
         -> (Map v term, Int, Int)
         -> Failing (Map v term, Int, Int)
mexpands :: 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 (PrologRule lit)
-> Set lit
-> Set lit
-> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int))
-> (Map v term, Int, Int)
-> Failing (Map v term, Int, Int)
mexpands Set (PrologRule lit)
rules Set lit
ancestors Set lit
gs (Map v term, Int, Int) -> Failing (Map v term, Int, Int)
cont (Map v term
env,Int
n,Int
k) =
    if Int -> Int
forall a. Enum a => a -> Int
fromEnum Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
    then [String] -> Failing (Map v term, Int, Int)
forall a. [String] -> Failing a
Failure [String
"Too deep"]
    else let m :: Int
m = Set lit -> Int
forall a. Set a -> Int
Set.size Set lit
gs in
         if Int
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1
         then (lit
 -> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int))
 -> (Map v term, Int, Int)
 -> Failing (Map v term, Int, Int))
-> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int))
-> Set lit
-> (Map v term, Int, Int)
-> Failing (Map v term, Int, Int)
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.foldr (Set (PrologRule lit)
-> Set lit
-> lit
-> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int))
-> (Map v term, Int, Int)
-> Failing (Map v term, Int, Int)
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 (PrologRule lit)
-> Set lit
-> lit
-> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int))
-> (Map v term, Int, Int)
-> Failing (Map v term, Int, Int)
mexpand2 Set (PrologRule lit)
rules Set lit
ancestors) (Map v term, Int, Int) -> Failing (Map v term, Int, Int)
cont Set lit
gs (Map v term
env,Int
n,Int
k)
         else let n1 :: Int
n1 = Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2
                  n2 :: Int
n2 = Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n1 in
              let (Set lit
goals1, Set lit
goals2) = Int -> Set lit -> (Set lit, Set lit)
forall a. Ord a => Int -> Set a -> (Set a, Set a)
setSplitAt (Int
m Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2) Set lit
gs in
              let expfn :: Set lit
-> Int
-> Set lit
-> Int
-> Int
-> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int))
-> Map v term
-> Int
-> Failing (Map v term, Int, Int)
expfn = (Set lit
 -> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int))
 -> (Map v term, Int, Int)
 -> Failing (Map v term, Int, Int))
-> Set lit
-> Int
-> Set lit
-> Int
-> Int
-> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int))
-> Map v term
-> Int
-> Failing (Map v term, Int, Int)
forall lit v term.
(Set lit
 -> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int))
 -> (Map v term, Int, Int)
 -> Failing (Map v term, Int, Int))
-> Set lit
-> Int
-> Set lit
-> Int
-> Int
-> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int))
-> Map v term
-> Int
-> Failing (Map v term, Int, Int)
expand2 (Set (PrologRule lit)
-> Set lit
-> Set lit
-> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int))
-> (Map v term, Int, Int)
-> Failing (Map v term, Int, Int)
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 (PrologRule lit)
-> Set lit
-> Set lit
-> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int))
-> (Map v term, Int, Int)
-> Failing (Map v term, Int, Int)
mexpands Set (PrologRule lit)
rules Set lit
ancestors) in
              case Set lit
-> Int
-> Set lit
-> Int
-> Int
-> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int))
-> Map v term
-> Int
-> Failing (Map v term, Int, Int)
expfn Set lit
goals1 Int
n1 Set lit
goals2 Int
n2 (-Int
1) (Map v term, Int, Int) -> Failing (Map v term, Int, Int)
cont Map v term
env Int
k of
                Success (Map v term, Int, Int)
r -> (Map v term, Int, Int) -> Failing (Map v term, Int, Int)
forall a. a -> Failing a
Success (Map v term, Int, Int)
r
                Failure [String]
_ -> Set lit
-> Int
-> Set lit
-> Int
-> Int
-> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int))
-> Map v term
-> Int
-> Failing (Map v term, Int, Int)
expfn Set lit
goals2 Int
n1 Set lit
goals1 Int
n2 Int
n1 (Map v term, Int, Int) -> Failing (Map v term, Int, Int)
cont Map v term
env Int
k

setSplitAt :: Ord a => Int -> Set a -> (Set a, Set a)
setSplitAt :: forall a. Ord a => Int -> Set a -> (Set a, Set a)
setSplitAt Int
n Set a
s = Int -> (Set a, Set a) -> (Set a, Set a)
forall {t} {a}.
(Num t, Ord a, Eq t) =>
t -> (Set a, Set a) -> (Set a, Set a)
go Int
n (Set a
forall a. Monoid a => a
mempty, Set a
s)
    where
      go :: t -> (Set a, Set a) -> (Set a, Set a)
go t
0 (Set a
s1, Set a
s2) = (Set a
s1, Set a
s2)
      go t
i (Set a
s1, Set a
s2) = case Set a -> Maybe (a, Set a)
forall a. Set a -> Maybe (a, Set a)
Set.minView Set a
s2 of
                         Maybe (a, Set a)
Nothing -> (Set a
s1, Set a
s2)
                         Just (a
x, Set a
s2') -> t -> (Set a, Set a) -> (Set a, Set a)
go (t
i t -> t -> t
forall a. Num a => a -> a -> a
- t
1) (a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
Set.insert a
x Set a
s1, Set a
s2')

puremeson2 :: 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), Ord fof
             ) => Maybe Depth -> fof -> Failing Depth
puremeson2 :: 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), Ord fof) =>
Maybe Depth -> fof -> Failing Depth
puremeson2 Maybe Depth
maxdl fof
fm =
    ((Map v term, Int, Int), Depth) -> Depth
forall a b. (a, b) -> b
snd (((Map v term, Int, Int), Depth) -> Depth)
-> Failing ((Map v term, Int, Int), Depth) -> Failing Depth
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Depth -> Failing (Map v term, Int, Int))
-> Depth -> Maybe Depth -> Failing ((Map v term, Int, Int), Depth)
forall t.
(Depth -> Failing t) -> Depth -> Maybe Depth -> Failing (t, Depth)
deepen Depth -> Failing (Map v term, Int, Int)
f (Int -> Depth
Depth Int
0) Maybe Depth
maxdl
    where
      f :: Depth -> Failing (Map v term, Int, Int)
      f :: Depth -> Failing (Map v term, Int, Int)
f Depth
n = Set (PrologRule (LFormula atom))
-> Set (LFormula atom)
-> LFormula atom
-> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int))
-> (Map v term, Int, Int)
-> Failing (Map v term, Int, Int)
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 (PrologRule lit)
-> Set lit
-> lit
-> ((Map v term, Int, Int) -> Failing (Map v term, Int, Int))
-> (Map v term, Int, Int)
-> Failing (Map v term, Int, Int)
mexpand2 Set (PrologRule (LFormula atom))
rules (Set (LFormula atom)
forall a. Set a
Set.empty :: Set (LFormula atom)) LFormula atom
forall formula. IsFormula formula => formula
false (Map v term, Int, Int) -> Failing (Map v term, Int, Int)
forall a. a -> Failing a
forall (m :: * -> *) a. Monad m => a -> m a
return (Map v term
forall k a. Map k a
Map.empty, Depth -> Int
forall a. Enum a => a -> Int
fromEnum Depth
n, Int
0)
      rules :: Set (PrologRule (LFormula atom))
rules = (Set (LFormula atom)
 -> Set (PrologRule (LFormula atom))
 -> Set (PrologRule (LFormula atom)))
-> Set (PrologRule (LFormula atom))
-> Set (Set (LFormula atom))
-> Set (PrologRule (LFormula atom))
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Set (PrologRule (LFormula atom))
-> Set (PrologRule (LFormula atom))
-> Set (PrologRule (LFormula atom))
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Set (PrologRule (LFormula atom))
 -> Set (PrologRule (LFormula atom))
 -> Set (PrologRule (LFormula atom)))
-> (Set (LFormula atom) -> Set (PrologRule (LFormula atom)))
-> Set (LFormula atom)
-> Set (PrologRule (LFormula atom))
-> Set (PrologRule (LFormula atom))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (LFormula atom) -> Set (PrologRule (LFormula atom))
forall lit.
(JustLiteral lit, Ord lit) =>
Set lit -> Set (PrologRule lit)
contrapositives) Set (PrologRule (LFormula atom))
forall a. Set a
Set.empty Set (Set (LFormula atom))
cls
      (Set (Set (LFormula atom))
cls :: Set (Set (LFormula atom))) = (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)

meson2 :: forall m fof atom term function v.
          (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 ~ VarOf fof, v ~ SVarOf function) =>
          Maybe Depth -> fof -> SkolemT m function (Set (Failing Depth))
meson2 :: forall (m :: * -> *) fof atom term function v.
(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 ~ VarOf fof, v ~ SVarOf function) =>
Maybe Depth -> fof -> SkolemT m function (Set (Failing Depth))
meson2 Maybe Depth
maxdl 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 Depth)))
-> StateT (SkolemState function) m (Set (Failing Depth))
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 Depth)
-> StateT (SkolemState function) m (Set (Failing Depth))
forall a. a -> StateT (SkolemState function) m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Set (Failing Depth)
 -> StateT (SkolemState function) m (Set (Failing Depth)))
-> (fof -> Set (Failing Depth))
-> fof
-> StateT (SkolemState function) m (Set (Failing Depth))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set fof -> Failing Depth) -> Set (Set fof) -> Set (Failing Depth)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Maybe Depth -> fof -> Failing Depth
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), Ord fof) =>
Maybe Depth -> fof -> Failing Depth
puremeson2 Maybe Depth
maxdl (fof -> Failing Depth)
-> (Set fof -> fof) -> Set fof -> Failing Depth
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 Depth))
-> (fof -> Set (Set fof)) -> fof -> Set (Failing Depth)
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))

meson :: (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), HasSkolem function, Monad m, Ord fof,
          atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) =>
         Maybe Depth -> fof -> SkolemT m function (Set (Failing Depth))
meson :: forall fof atom term function (m :: * -> *) v.
(IsFirstOrder fof, Unify Failing (atom, atom),
 term ~ UTermOf (atom, atom), HasSkolem function, Monad m, Ord fof,
 atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term,
 v ~ VarOf fof, v ~ SVarOf function) =>
Maybe Depth -> fof -> SkolemT m function (Set (Failing Depth))
meson = Maybe Depth -> fof -> SkolemT m function (Set (Failing Depth))
forall (m :: * -> *) fof atom term function v.
(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 ~ VarOf fof, v ~ SVarOf function) =>
Maybe Depth -> fof -> SkolemT m function (Set (Failing Depth))
meson2

{-
-- -------------------------------------------------------------------------
-- The Los problem (depth 20) and the Steamroller (depth 53) --- lengthier.
-- -------------------------------------------------------------------------

START_INTERACTIVE;;
{- ***********

let los = meson
 <<(forall x y z. P(x,y) ==> P(y,z) ==> P(x,z)) /\
   (forall x y z. Q(x,y) ==> Q(y,z) ==> Q(x,z)) /\
   (forall x y. Q(x,y) ==> Q(y,x)) /\
   (forall x y. P(x,y) \/ Q(x,y))
   ==> (forall x y. P(x,y)) \/ (forall x y. Q(x,y))>>;;

let steamroller = meson
 <<((forall x. P1(x) ==> P0(x)) /\ (exists x. P1(x))) /\
   ((forall x. P2(x) ==> P0(x)) /\ (exists x. P2(x))) /\
   ((forall x. P3(x) ==> P0(x)) /\ (exists x. P3(x))) /\
   ((forall x. P4(x) ==> P0(x)) /\ (exists x. P4(x))) /\
   ((forall x. P5(x) ==> P0(x)) /\ (exists x. P5(x))) /\
   ((exists x. Q1(x)) /\ (forall x. Q1(x) ==> Q0(x))) /\
   (forall x. P0(x)
              ==> (forall y. Q0(y) ==> R(x,y)) \/
                  ((forall y. P0(y) /\ S0(y,x) /\
                              (exists z. Q0(z) /\ R(y,z))
                              ==> R(x,y)))) /\
   (forall x y. P3(y) /\ (P5(x) \/ P4(x)) ==> S0(x,y)) /\
   (forall x y. P3(x) /\ P2(y) ==> S0(x,y)) /\
   (forall x y. P2(x) /\ P1(y) ==> S0(x,y)) /\
   (forall x y. P1(x) /\ (P2(y) \/ Q1(y)) ==> ~(R(x,y))) /\
   (forall x y. P3(x) /\ P4(y) ==> R(x,y)) /\
   (forall x y. P3(x) /\ P5(y) ==> ~(R(x,y))) /\
   (forall x. (P4(x) \/ P5(x)) ==> exists y. Q0(y) /\ R(x,y))
   ==> exists x y. P0(x) /\ P0(y) /\
                   exists z. Q1(z) /\ R(y,z) /\ R(x,y)>>;;

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


-- -------------------------------------------------------------------------
-- Test it.
-- -------------------------------------------------------------------------

let prop_1 = time meson
 <<p ==> q <=> ~q ==> ~p>>;;

let prop_2 = time meson
 <<~ ~p <=> p>>;;

let prop_3 = time meson
 <<~(p ==> q) ==> q ==> p>>;;

let prop_4 = time meson
 <<~p ==> q <=> ~q ==> p>>;;

let prop_5 = time meson
 <<(p \/ q ==> p \/ r) ==> p \/ (q ==> r)>>;;

let prop_6 = time meson
 <<p \/ ~p>>;;

let prop_7 = time meson
 <<p \/ ~ ~ ~p>>;;

let prop_8 = time meson
 <<((p ==> q) ==> p) ==> p>>;;

let prop_9 = time meson
 <<(p \/ q) /\ (~p \/ q) /\ (p \/ ~q) ==> ~(~q \/ ~q)>>;;

let prop_10 = time meson
 <<(q ==> r) /\ (r ==> p /\ q) /\ (p ==> q /\ r) ==> (p <=> q)>>;;

let prop_11 = time meson
 <<p <=> p>>;;

let prop_12 = time meson
 <<((p <=> q) <=> r) <=> (p <=> (q <=> r))>>;;

let prop_13 = time meson
 <<p \/ q /\ r <=> (p \/ q) /\ (p \/ r)>>;;

let prop_14 = time meson
 <<(p <=> q) <=> (q \/ ~p) /\ (~q \/ p)>>;;

let prop_15 = time meson
 <<p ==> q <=> ~p \/ q>>;;

let prop_16 = time meson
 <<(p ==> q) \/ (q ==> p)>>;;

let prop_17 = time meson
 <<p /\ (q ==> r) ==> s <=> (~p \/ q \/ s) /\ (~p \/ ~r \/ s)>>;;

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

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

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

let p20 = time meson
 <<(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 meson
 <<(exists x. P ==> Q(x)) /\ (exists x. Q(x) ==> P)
   ==> (exists x. P <=> Q(x))>>;;

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

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

let p24 = time meson
 <<~(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 meson
 <<(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 meson
 <<((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 meson
 <<(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 meson
 <<(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 meson
 <<(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 meson
 <<(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 meson
 <<~(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 meson
 <<(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 meson
 <<(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 meson
 <<((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 meson
 <<exists x y. P(x,y) ==> (forall x y. P(x,y))>>;;

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

let p36 = time meson
 <<(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 meson
 <<(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))>>;;

let p38 = time meson
 <<(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 meson
 <<~(exists x. forall y. P(y,x) <=> ~P(y,y))>>;;

let p40 = time meson
 <<(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 meson
 <<(forall z. exists y. forall x. P(x,y) <=> P(x,z) /\ ~P(x,x))
  ==> ~(exists z. forall x. P(x,z))>>;;

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

let p43 = time meson
 <<(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 meson
 <<(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))>>;;

let p45 = time meson
 <<(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)))>>;;

let p46 = time meson
 <<(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 meson
 <<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 meson
 <<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 meson
 <<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 meson
 <<(forall x. P(x) <=> ~P(f(x))) ==> (exists x. P(x) /\ ~P(f(x)))>>;;

let p60 = time meson
 <<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.
-- -------------------------------------------------------------------------

{- ** Amazingly, this still seems non-trivial... in HOL it works at depth 45!

let gilmore_1 = time meson
 <<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 meson
 <<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 meson
 <<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 meson
 <<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 meson
 <<(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 meson
 <<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 meson
 <<(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 meson
 <<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 is still a very hard problem

let gilmore_9 = time meson
 <<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)))>>;;

 ** -}

-- -------------------------------------------------------------------------
-- Translation of Gilmore procedure using separate definitions.
-- -------------------------------------------------------------------------

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

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

let davis_putnam_example = time meson
 <<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 "connections make things worse" example once again.
-- -------------------------------------------------------------------------

meson <<~p /\ (p \/ q) /\ (r \/ s) /\ (~q \/ t \/ u) /\
        (~r \/ ~t) /\ (~r \/ ~u) /\ (~q \/ v \/ w) /\
        (~s \/ ~v) /\ (~s \/ ~w) ==> false>>;;
END_INTERACTIVE;;
-}

testMeson :: Test
testMeson :: Test
testMeson = String -> Test -> Test
TestLabel String
"Meson" ([Test] -> Test
TestList [Test
test03, Test
test04, Test
test05, Test
test01, Test
test06, Test
test02])