{-# 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)
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]])))]]))
((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]])))]))
((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"
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
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
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))
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
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])