{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wall #-}
module Data.Logic.ATP.Tableaux
( prawitz
, K(K)
, tab
, testTableaux
) where
import Data.Logic.ATP.Apply (HasApply(TermOf), pApp)
import Control.Monad.Fail
import Control.Monad.RWS (RWS)
import Control.Monad.State (execStateT, StateT)
import Data.List as List (map)
import Data.Logic.ATP.FOL (asubst, fv, generalize, IsFirstOrder, subst)
import Data.Logic.ATP.Formulas (atomic, IsFormula(asBool, AtomOf), onatoms, overatoms)
import Data.Logic.ATP.Herbrand (davisputnam)
import Data.Logic.ATP.Lib ((|=>), allpairs, deepen, Depth(Depth), distrib, evalRS, Failing(Success, Failure), failing, settryfind, tryfindM)
import Data.Logic.ATP.Lit ((.~.), convertToLiteral, IsLiteral, JustLiteral, LFormula, positive)
import Data.Logic.ATP.LitWrapper (JL)
import Data.Logic.ATP.Pretty (assertEqual', Pretty(pPrint), prettyShow, text)
import Data.Logic.ATP.Prop ( (.&.), (.=>.), (.<=>.), (.|.), BinOp((:&:), (:|:)), PFormula, simpdnf)
import Data.Logic.ATP.Quantified (exists, foldQuantified, for_all, Quant((:!:)))
import Data.Logic.ATP.Skolem (askolemize, Formula, HasSkolem(SVarOf, toSkolem), runSkolem, simpdnf', skolemize, SkTerm)
import Data.Logic.ATP.Term (fApp, IsTerm(TVarOf, FunOf), vt)
import Data.Logic.ATP.Unif (Unify(UTermOf), unify_literals)
import Data.Map.Strict as Map
import Data.Set as Set
import Data.String (IsString(..))
import Prelude hiding (compare)
import Test.HUnit hiding (State)
unify_complements :: (IsLiteral lit1, JustLiteral lit2, HasApply atom1, HasApply atom2,
Unify m (atom1, atom2), term ~ UTermOf (atom1, atom2), v ~ TVarOf term,
atom1 ~ AtomOf lit1, term ~ TermOf atom1,
atom2 ~ AtomOf lit2, term ~ TermOf atom2, MonadFail m) =>
lit1 -> lit2 -> StateT (Map v term) m ()
unify_complements :: forall lit1 lit2 atom1 atom2 (m :: * -> *) term v.
(IsLiteral lit1, JustLiteral lit2, HasApply atom1, HasApply atom2,
Unify m (atom1, atom2), term ~ UTermOf (atom1, atom2),
v ~ TVarOf term, atom1 ~ AtomOf lit1, term ~ TermOf atom1,
atom2 ~ AtomOf lit2, term ~ TermOf atom2, MonadFail m) =>
lit1 -> lit2 -> StateT (Map v term) m ()
unify_complements lit1
p lit2
q = lit1 -> lit2 -> StateT (Map v term) m ()
forall lit1 lit2 atom1 atom2 v term (m :: * -> *).
(IsLiteral lit1, HasApply atom1, atom1 ~ AtomOf lit1,
term ~ TermOf atom1, JustLiteral lit2, HasApply atom2,
atom2 ~ AtomOf lit2, term ~ TermOf atom2, Unify m (atom1, atom2),
term ~ UTermOf (atom1, atom2), v ~ TVarOf term, MonadFail m) =>
lit1 -> lit2 -> StateT (Map v term) m ()
unify_literals lit1
p (lit2 -> lit2
forall formula. IsLiteral formula => formula -> formula
(.~.) lit2
q)
unify_refute :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term,
Unify Failing (atom, atom), term ~ UTermOf (atom, atom), v ~ TVarOf term,
atom ~ AtomOf lit, term ~ TermOf atom) =>
Set (Set lit) -> Map v term -> Failing (Map v term)
unify_refute :: forall lit atom term v.
(JustLiteral lit, Ord lit, HasApply atom, IsTerm term,
Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
v ~ TVarOf term, atom ~ AtomOf lit, term ~ TermOf atom) =>
Set (Set lit) -> Map v term -> Failing (Map v term)
unify_refute Set (Set lit)
djs Map v term
env =
case Set (Set lit) -> Maybe (Set lit, Set (Set lit))
forall a. Set a -> Maybe (a, Set a)
Set.minView Set (Set lit)
djs of
Maybe (Set lit, Set (Set lit))
Nothing -> Map v term -> Failing (Map v term)
forall a. a -> Failing a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Map v term
env
Just (Set lit
d, Set (Set lit)
odjs) ->
((lit, lit) -> Failing (Map v term))
-> Set (lit, lit) -> Failing (Map v term)
forall t a. (t -> Failing a) -> Set t -> Failing a
settryfind (\ (lit
p, lit
n) -> StateT (Map v term) Failing ()
-> Map v term -> Failing (Map v term)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT (lit -> lit -> StateT (Map v term) Failing ()
forall lit1 lit2 atom1 atom2 (m :: * -> *) term v.
(IsLiteral lit1, JustLiteral lit2, HasApply atom1, HasApply atom2,
Unify m (atom1, atom2), term ~ UTermOf (atom1, atom2),
v ~ TVarOf term, atom1 ~ AtomOf lit1, term ~ TermOf atom1,
atom2 ~ AtomOf lit2, term ~ TermOf atom2, MonadFail m) =>
lit1 -> lit2 -> StateT (Map v term) m ()
unify_complements lit
p lit
n) Map v term
env Failing (Map v term)
-> (Map v term -> Failing (Map v term)) -> Failing (Map v term)
forall a b. Failing a -> (a -> Failing b) -> Failing b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Set (Set lit) -> Map v term -> Failing (Map v term)
forall lit atom term v.
(JustLiteral lit, Ord lit, HasApply atom, IsTerm term,
Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
v ~ TVarOf term, atom ~ AtomOf lit, term ~ TermOf atom) =>
Set (Set lit) -> Map v term -> Failing (Map v term)
unify_refute Set (Set lit)
odjs) Set (lit, lit)
pairs
where
pairs :: Set (lit, lit)
pairs = (lit -> lit -> (lit, lit)) -> Set lit -> Set lit -> Set (lit, lit)
forall a b c (set :: * -> *).
(SetLike set, Ord c) =>
(a -> b -> c) -> set a -> set b -> set c
allpairs (,) Set lit
pos Set lit
neg
(Set lit
pos,Set lit
neg) = (lit -> Bool) -> Set lit -> (Set lit, Set lit)
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition lit -> Bool
forall formula. IsLiteral formula => formula -> Bool
positive Set lit
d
prawitz_loop :: forall lit atom v term.
(JustLiteral lit, Ord lit, HasApply atom, Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
Set (Set lit) -> [v] -> Set (Set lit) -> Int -> (Map v term, Int)
prawitz_loop :: forall lit atom v term.
(JustLiteral lit, Ord lit, HasApply atom,
Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
Set (Set lit) -> [v] -> Set (Set lit) -> Int -> (Map v term, Int)
prawitz_loop Set (Set lit)
djs0 [v]
fvs Set (Set lit)
djs Int
n =
let inst :: Map v (TermOf atom)
inst = [(v, TermOf atom)] -> Map v (TermOf atom)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([v] -> [TermOf atom] -> [(v, TermOf atom)]
forall a b. [a] -> [b] -> [(a, b)]
zip [v]
fvs ((Int -> TermOf atom) -> [Int] -> [TermOf atom]
forall a b. (a -> b) -> [a] -> [b]
List.map Int -> TermOf atom
newvar [Int
1..]))
djs1 :: Set (Set lit)
djs1 = Set (Set lit) -> Set (Set lit) -> Set (Set lit)
forall a. Ord a => Set (Set a) -> Set (Set a) -> Set (Set a)
distrib ((Set lit -> Set lit) -> Set (Set lit) -> Set (Set lit)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((lit -> lit) -> Set lit -> Set lit
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((AtomOf lit -> AtomOf lit) -> lit -> lit
forall formula.
IsFormula formula =>
(AtomOf formula -> AtomOf formula) -> formula -> formula
onatoms (Map v (TermOf atom) -> atom -> atom
forall atom term v.
(HasApply atom, IsTerm term, term ~ TermOf atom,
v ~ TVarOf term) =>
Map v term -> atom -> atom
asubst Map v (TermOf atom)
inst))) Set (Set lit)
djs0) Set (Set lit)
djs in
case Set (Set lit) -> Map v term -> Failing (Map v term)
forall lit atom term v.
(JustLiteral lit, Ord lit, HasApply atom, IsTerm term,
Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
v ~ TVarOf term, atom ~ AtomOf lit, term ~ TermOf atom) =>
Set (Set lit) -> Map v term -> Failing (Map v term)
unify_refute Set (Set lit)
djs1 Map v term
forall k a. Map k a
Map.empty of
Failure [[Char]]
_ -> Set (Set lit) -> [v] -> Set (Set lit) -> Int -> (Map v term, Int)
forall lit atom v term.
(JustLiteral lit, Ord lit, HasApply atom,
Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
Set (Set lit) -> [v] -> Set (Set lit) -> Int -> (Map v term, Int)
prawitz_loop Set (Set lit)
djs0 [v]
fvs Set (Set lit)
djs1 (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
Success Map v term
env -> (Map v term
env, Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
where
newvar :: Int -> TermOf atom
newvar Int
k = TVarOf (TermOf atom) -> TermOf atom
forall term. IsTerm term => TVarOf term -> term
vt ([Char] -> TVarOf (TermOf atom)
forall a. IsString a => [Char] -> a
fromString ([Char]
"_" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
* [v] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [v]
fvs Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
k)))
prawitz :: forall formula atom term function v.
(IsFirstOrder formula, Ord formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), HasSkolem function, Show formula,
atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
v ~ TVarOf term, v ~ SVarOf function) =>
formula -> Int
prawitz :: forall formula atom term function v.
(IsFirstOrder formula, Ord formula, Unify Failing (atom, atom),
term ~ UTermOf (atom, atom), HasSkolem function, Show formula,
atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
v ~ TVarOf term, v ~ SVarOf function) =>
formula -> Int
prawitz formula
fm =
(Map v (UTermOf (atom, atom)), Int) -> Int
forall a b. (a, b) -> b
snd (Set (Set (LFormula atom))
-> [v]
-> Set (Set (LFormula atom))
-> Int
-> (Map v (UTermOf (atom, atom)), Int)
forall lit atom v term.
(JustLiteral lit, Ord lit, HasApply atom,
Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) =>
Set (Set lit) -> [v] -> Set (Set lit) -> Int -> (Map v term, Int)
prawitz_loop Set (Set (LFormula atom))
dnf (Set v -> [v]
forall a. Set a -> [a]
Set.toList Set v
fvs) Set (Set (LFormula atom))
forall {a}. Set (Set a)
dnf0 Int
0)
where
dnf0 :: Set (Set a)
dnf0 = Set a -> Set (Set a)
forall a. a -> Set a
Set.singleton Set a
forall a. Set a
Set.empty
dnf :: Set (Set (LFormula atom))
dnf = ((AtomOf (PFormula atom) -> AtomOf (LFormula atom))
-> PFormula atom -> Set (Set (LFormula atom))
forall pf lit.
(JustPropositional pf, IsLiteral lit, JustLiteral lit, Ord lit) =>
(AtomOf pf -> AtomOf lit) -> pf -> Set (Set lit)
simpdnf atom -> atom
AtomOf (PFormula atom) -> AtomOf (LFormula atom)
forall a. a -> a
id PFormula atom
pf :: Set (Set (LFormula atom)))
fvs :: Set v
fvs = (AtomOf (PFormula atom) -> Set v -> Set v)
-> PFormula atom -> Set v -> Set v
forall formula r.
IsFormula formula =>
(AtomOf formula -> r -> r) -> formula -> r -> r
forall r.
(AtomOf (PFormula atom) -> r -> r) -> PFormula atom -> r -> r
overatoms (\ AtomOf (PFormula atom)
a Set v
s -> Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
Set.union (formula -> Set v
forall formula v.
(IsFirstOrder formula, v ~ VarOf formula) =>
formula -> Set v
fv (AtomOf formula -> formula
forall formula. IsFormula formula => AtomOf formula -> formula
atomic AtomOf formula
AtomOf (PFormula atom)
a :: formula)) Set v
s) PFormula atom
pf (Set v
forall a. Set a
Set.empty :: Set v)
pf :: PFormula atom
pf = SkolemT Identity function (PFormula atom) -> PFormula atom
forall function a.
IsFunction function =>
SkolemT Identity function a -> a
runSkolem ((AtomOf formula -> AtomOf (PFormula atom))
-> formula -> SkolemT Identity function (PFormula atom)
forall formula pf function (m :: * -> *) atom term.
(IsFirstOrder formula, JustPropositional pf, HasSkolem function,
Monad m, atom ~ AtomOf formula, term ~ TermOf atom,
function ~ FunOf term, VarOf formula ~ SVarOf function) =>
(AtomOf formula -> AtomOf pf)
-> formula -> StateT (SkolemState function) m pf
skolemize atom -> atom
AtomOf formula -> AtomOf (PFormula atom)
forall a. a -> a
id (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.)(formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
generalize formula
fm))) :: PFormula atom
p20 :: Test
p20 :: Test
p20 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ [Char] -> Int -> Int -> Assertion
forall a.
(?loc::CallStack, Eq a, Pretty a) =>
[Char] -> a -> a -> Assertion
assertEqual' [Char]
"p20 - prawitz (p. 175)" Int
forall {a}. Num a => a
expected Int
input
where fm :: Formula
fm :: Formula
fm = (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"x" (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"y" (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"z" (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"w" (PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
"P" [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"x"] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
"Q" [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"y"] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>.
PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
"R" [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"z"] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
"U" [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"w"]))))) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>.
(VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"x" (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"y" (PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
"P" [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"x"] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
"Q" [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"y"]))) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"z" (PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
"R" [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"z"]))
input :: Int
input = Formula -> Int
forall formula atom term function v.
(IsFirstOrder formula, Ord formula, Unify Failing (atom, atom),
term ~ UTermOf (atom, atom), HasSkolem function, Show formula,
atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
v ~ TVarOf term, v ~ SVarOf function) =>
formula -> Int
prawitz Formula
fm
expected :: a
expected = a
2
compare :: (IsFirstOrder formula, Ord formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), HasSkolem function, Show formula,
atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
v ~ TVarOf term, v ~ SVarOf function) =>
formula -> (Int, Int)
compare :: forall formula atom term function v.
(IsFirstOrder formula, Ord formula, Unify Failing (atom, atom),
term ~ UTermOf (atom, atom), HasSkolem function, Show formula,
atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
v ~ TVarOf term, v ~ SVarOf function) =>
formula -> (Int, Int)
compare formula
fm = (formula -> Int
forall formula atom term function v.
(IsFirstOrder formula, Ord formula, Unify Failing (atom, atom),
term ~ UTermOf (atom, atom), HasSkolem function, Show formula,
atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
v ~ TVarOf term, v ~ SVarOf function) =>
formula -> Int
prawitz formula
fm, formula -> Int
forall formula atom term v function.
(IsFirstOrder formula, Ord formula, HasSkolem function,
atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
v ~ TVarOf term, v ~ SVarOf function) =>
formula -> Int
davisputnam formula
fm)
p19 :: Test
p19 :: Test
p19 = Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ [Char] -> (Int, Int) -> (Int, Int) -> Assertion
forall a.
(?loc::CallStack, Eq a, Pretty a) =>
[Char] -> a -> a -> Assertion
assertEqual' [Char]
"p19" (Int, Int)
forall {a} {b}. (Num a, Num b) => (a, b)
expected (Int, Int)
input
where
fm :: Formula
fm :: Formula
fm = VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"x" (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"y" (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"z" ((PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
"P" [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"y"] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
"Q" [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"z"]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
"P" [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"x"] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
"Q" [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"x"])))
input :: (Int, Int)
input = Formula -> (Int, Int)
forall formula atom term function v.
(IsFirstOrder formula, Ord formula, Unify Failing (atom, atom),
term ~ UTermOf (atom, atom), HasSkolem function, Show formula,
atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
v ~ TVarOf term, v ~ SVarOf function) =>
formula -> (Int, Int)
compare Formula
fm
expected :: (a, b)
expected = (a
3, b
3)
newtype K = K Int deriving (K -> K -> Bool
(K -> K -> Bool) -> (K -> K -> Bool) -> Eq K
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: K -> K -> Bool
== :: K -> K -> Bool
$c/= :: K -> K -> Bool
/= :: K -> K -> Bool
Eq, Eq K
Eq K =>
(K -> K -> Ordering)
-> (K -> K -> Bool)
-> (K -> K -> Bool)
-> (K -> K -> Bool)
-> (K -> K -> Bool)
-> (K -> K -> K)
-> (K -> K -> K)
-> Ord K
K -> K -> Bool
K -> K -> Ordering
K -> K -> K
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: K -> K -> Ordering
compare :: K -> K -> Ordering
$c< :: K -> K -> Bool
< :: K -> K -> Bool
$c<= :: K -> K -> Bool
<= :: K -> K -> Bool
$c> :: K -> K -> Bool
> :: K -> K -> Bool
$c>= :: K -> K -> Bool
>= :: K -> K -> Bool
$cmax :: K -> K -> K
max :: K -> K -> K
$cmin :: K -> K -> K
min :: K -> K -> K
Ord, Int -> K -> [Char] -> [Char]
[K] -> [Char] -> [Char]
K -> [Char]
(Int -> K -> [Char] -> [Char])
-> (K -> [Char]) -> ([K] -> [Char] -> [Char]) -> Show K
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: Int -> K -> [Char] -> [Char]
showsPrec :: Int -> K -> [Char] -> [Char]
$cshow :: K -> [Char]
show :: K -> [Char]
$cshowList :: [K] -> [Char] -> [Char]
showList :: [K] -> [Char] -> [Char]
Show)
instance Enum K where
toEnum :: Int -> K
toEnum = Int -> K
K
fromEnum :: K -> Int
fromEnum (K Int
n) = Int
n
instance Pretty K where
pPrint :: K -> Doc
pPrint (K Int
n) = [Char] -> Doc
text ([Char]
"K" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
n)
tableau :: forall formula atom term v function.
(IsFirstOrder formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term) =>
[formula] -> Depth -> RWS () () () (Failing (K, Map v term))
tableau :: forall formula atom term v function.
(IsFirstOrder formula, Unify Failing (atom, atom),
term ~ UTermOf (atom, atom), atom ~ AtomOf formula,
term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term) =>
[formula] -> Depth -> RWS () () () (Failing (K, Map v term))
tableau [formula]
fms Depth
n0 =
([formula], [JL formula], Depth)
-> ((K, Map v term) -> RWS () () () (Failing (K, Map v term)))
-> (K, Map v term)
-> RWS () () () (Failing (K, Map v term))
go ([formula]
fms, [], Depth
n0) (Failing (K, Map v term) -> RWS () () () (Failing (K, Map v term))
forall a. a -> RWST () () () Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Failing (K, Map v term) -> RWS () () () (Failing (K, Map v term)))
-> ((K, Map v term) -> Failing (K, Map v term))
-> (K, Map v term)
-> RWS () () () (Failing (K, Map v term))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (K, Map v term) -> Failing (K, Map v term)
forall a. a -> Failing a
Success) (Int -> K
K Int
0, Map v term
forall k a. Map k a
Map.empty)
where
go :: ([formula], [JL formula], Depth)
-> ((K, Map v term) -> RWS () () () (Failing (K, Map v term)))
-> (K, Map v term)
-> RWS () () () (Failing (K, Map v term))
go :: ([formula], [JL formula], Depth)
-> ((K, Map v term) -> RWS () () () (Failing (K, Map v term)))
-> (K, Map v term)
-> RWS () () () (Failing (K, Map v term))
go ([formula]
_, [JL formula]
_, Depth
n) (K, Map v term) -> RWS () () () (Failing (K, Map v term))
_ (K
_, Map v term
_) | Depth
n Depth -> Depth -> Bool
forall a. Ord a => a -> a -> Bool
< Int -> Depth
Depth Int
0 = Failing (K, Map v term) -> RWS () () () (Failing (K, Map v term))
forall a. a -> RWST () () () Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Failing (K, Map v term) -> RWS () () () (Failing (K, Map v term)))
-> Failing (K, Map v term)
-> RWS () () () (Failing (K, Map v term))
forall a b. (a -> b) -> a -> b
$ [[Char]] -> Failing (K, Map v term)
forall a. [[Char]] -> Failing a
Failure [[Char]
"no proof at this level"]
go ([], [JL formula]
_, Depth
_) (K, Map v term) -> RWS () () () (Failing (K, Map v term))
_ (K
_, Map v term
_) = Failing (K, Map v term) -> RWS () () () (Failing (K, Map v term))
forall a. a -> RWST () () () Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Failing (K, Map v term) -> RWS () () () (Failing (K, Map v term)))
-> Failing (K, Map v term)
-> RWS () () () (Failing (K, Map v term))
forall a b. (a -> b) -> a -> b
$ [[Char]] -> Failing (K, Map v term)
forall a. [[Char]] -> Failing a
Failure [[Char]
"tableau: no proof"]
go (formula
fm : [formula]
unexp, [JL formula]
lits, Depth
n) (K, Map v term) -> RWS () () () (Failing (K, Map v term))
cont (K
k, Map v term
env) =
(Quant
-> VarOf formula
-> formula
-> RWS () () () (Failing (K, Map v term)))
-> (formula
-> BinOp -> formula -> RWS () () () (Failing (K, Map v term)))
-> (formula -> RWS () () () (Failing (K, Map v term)))
-> (Bool -> RWS () () () (Failing (K, Map v term)))
-> (AtomOf formula -> RWS () () () (Failing (K, Map v term)))
-> formula
-> RWS () () () (Failing (K, Map v term))
forall formula r.
IsQuantified formula =>
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
forall r.
(Quant -> VarOf formula -> formula -> r)
-> (formula -> BinOp -> formula -> r)
-> (formula -> r)
-> (Bool -> r)
-> (AtomOf formula -> r)
-> formula
-> r
foldQuantified Quant -> v -> formula -> RWS () () () (Failing (K, Map v term))
Quant
-> VarOf formula
-> formula
-> RWS () () () (Failing (K, Map v term))
qu formula
-> BinOp -> formula -> RWS () () () (Failing (K, Map v term))
co (\formula
_ -> formula -> [formula] -> RWS () () () (Failing (K, Map v term))
go2 formula
fm [formula]
unexp) (\Bool
_ -> formula -> [formula] -> RWS () () () (Failing (K, Map v term))
go2 formula
fm [formula]
unexp) (\AtomOf formula
_ -> formula -> [formula] -> RWS () () () (Failing (K, Map v term))
go2 formula
fm [formula]
unexp) formula
fm
where
qu :: Quant -> v -> formula -> RWS () () () (Failing (K, Map v term))
qu :: Quant -> v -> formula -> RWS () () () (Failing (K, Map v term))
qu Quant
(:!:) v
x formula
p =
let y :: term
y = TVarOf term -> term
forall term. IsTerm term => TVarOf term -> term
vt ([Char] -> TVarOf term
forall a. IsString a => [Char] -> a
fromString (K -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow K
k))
p' :: formula
p' = Map v term -> formula -> formula
forall formula term v.
(IsFirstOrder formula, term ~ TermOf (AtomOf formula),
v ~ VarOf formula) =>
Map v term -> formula -> formula
subst (v
x v -> term -> Map v term
forall k a. Ord k => k -> a -> Map k a
|=> term
y) formula
p in
([formula], [JL formula], Depth)
-> ((K, Map v term) -> RWS () () () (Failing (K, Map v term)))
-> (K, Map v term)
-> RWS () () () (Failing (K, Map v term))
go ([formula
p'] [formula] -> [formula] -> [formula]
forall a. [a] -> [a] -> [a]
++ [formula]
unexp [formula] -> [formula] -> [formula]
forall a. [a] -> [a] -> [a]
++ [VarOf formula -> formula -> formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all v
VarOf formula
x formula
p],[JL formula]
lits,Depth -> Depth
forall a. Enum a => a -> a
pred Depth
n) (K, Map v term) -> RWS () () () (Failing (K, Map v term))
cont (K -> K
forall a. Enum a => a -> a
succ K
k, Map v term
env)
qu Quant
_ v
_ formula
_ = formula -> [formula] -> RWS () () () (Failing (K, Map v term))
go2 formula
fm [formula]
unexp
co :: formula
-> BinOp -> formula -> RWS () () () (Failing (K, Map v term))
co formula
p BinOp
(:&:) formula
q =
([formula], [JL formula], Depth)
-> ((K, Map v term) -> RWS () () () (Failing (K, Map v term)))
-> (K, Map v term)
-> RWS () () () (Failing (K, Map v term))
go (formula
p formula -> [formula] -> [formula]
forall a. a -> [a] -> [a]
: formula
q formula -> [formula] -> [formula]
forall a. a -> [a] -> [a]
: [formula]
unexp,[JL formula]
lits,Depth
n) (K, Map v term) -> RWS () () () (Failing (K, Map v term))
cont (K
k, Map v term
env)
co formula
p BinOp
(:|:) formula
q =
([formula], [JL formula], Depth)
-> ((K, Map v term) -> RWS () () () (Failing (K, Map v term)))
-> (K, Map v term)
-> RWS () () () (Failing (K, Map v term))
go (formula
p formula -> [formula] -> [formula]
forall a. a -> [a] -> [a]
: [formula]
unexp,[JL formula]
lits,Depth
n) (([formula], [JL formula], Depth)
-> ((K, Map v term) -> RWS () () () (Failing (K, Map v term)))
-> (K, Map v term)
-> RWS () () () (Failing (K, Map v term))
go (formula
q formula -> [formula] -> [formula]
forall a. a -> [a] -> [a]
: [formula]
unexp,[JL formula]
lits,Depth
n) (K, Map v term) -> RWS () () () (Failing (K, Map v term))
cont) (K
k, Map v term
env)
co formula
_ BinOp
_ formula
_ = formula -> [formula] -> RWS () () () (Failing (K, Map v term))
go2 formula
fm [formula]
unexp
go2 :: formula -> [formula] -> RWS () () () (Failing (K, Map v term))
go2 :: formula -> [formula] -> RWS () () () (Failing (K, Map v term))
go2 formula
fm' [formula]
unexp' =
let (JL formula
fm'' :: JL formula) = (formula -> JL formula)
-> (AtomOf formula -> AtomOf (JL formula)) -> formula -> JL formula
forall formula lit.
(IsLiteral formula, JustLiteral lit) =>
(formula -> lit)
-> (AtomOf formula -> AtomOf lit) -> formula -> lit
convertToLiteral ([Char] -> formula -> JL formula
forall a. HasCallStack => [Char] -> a
error [Char]
"expected JustLiteral") atom -> atom
AtomOf formula -> AtomOf (JL formula)
forall a. a -> a
id formula
fm' in
(JL formula -> RWS () () () (Failing (K, Map v term)))
-> [JL formula] -> RWS () () () (Failing (K, Map v term))
forall (m :: * -> *) t a.
Monad m =>
(t -> m (Failing a)) -> [t] -> m (Failing a)
tryfindM (JL formula -> JL formula -> RWS () () () (Failing (K, Map v term))
tryLit JL formula
fm'') [JL formula]
lits RWS () () () (Failing (K, Map v term))
-> (Failing (K, Map v term)
-> RWS () () () (Failing (K, Map v term)))
-> RWS () () () (Failing (K, Map v term))
forall a b.
RWST () () () Identity a
-> (a -> RWST () () () Identity b) -> RWST () () () Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
([[Char]] -> RWS () () () (Failing (K, Map v term)))
-> ((K, Map v term) -> RWS () () () (Failing (K, Map v term)))
-> Failing (K, Map v term)
-> RWS () () () (Failing (K, Map v term))
forall b a. ([[Char]] -> b) -> (a -> b) -> Failing a -> b
failing (\[[Char]]
_ -> ([formula], [JL formula], Depth)
-> ((K, Map v term) -> RWS () () () (Failing (K, Map v term)))
-> (K, Map v term)
-> RWS () () () (Failing (K, Map v term))
go ([formula]
unexp', JL formula
fm'' JL formula -> [JL formula] -> [JL formula]
forall a. a -> [a] -> [a]
: [JL formula]
lits, Depth
n) (K, Map v term) -> RWS () () () (Failing (K, Map v term))
cont (K
k, Map v term
env))
(Failing (K, Map v term) -> RWS () () () (Failing (K, Map v term))
forall a. a -> RWST () () () Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Failing (K, Map v term) -> RWS () () () (Failing (K, Map v term)))
-> ((K, Map v term) -> Failing (K, Map v term))
-> (K, Map v term)
-> RWS () () () (Failing (K, Map v term))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (K, Map v term) -> Failing (K, Map v term)
forall a. a -> Failing a
Success)
tryLit :: JL formula -> JL formula -> RWS () () () (Failing (K, Map v term))
tryLit :: JL formula -> JL formula -> RWS () () () (Failing (K, Map v term))
tryLit JL formula
fm' JL formula
l = ([[Char]] -> RWS () () () (Failing (K, Map v term)))
-> (Map v term -> RWS () () () (Failing (K, Map v term)))
-> Failing (Map v term)
-> RWS () () () (Failing (K, Map v term))
forall b a. ([[Char]] -> b) -> (a -> b) -> Failing a -> b
failing (Failing (K, Map v term) -> RWS () () () (Failing (K, Map v term))
forall a. a -> RWST () () () Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Failing (K, Map v term) -> RWS () () () (Failing (K, Map v term)))
-> ([[Char]] -> Failing (K, Map v term))
-> [[Char]]
-> RWS () () () (Failing (K, Map v term))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Char]] -> Failing (K, Map v term)
forall a. [[Char]] -> Failing a
Failure) (\Map v term
env' -> (K, Map v term) -> RWS () () () (Failing (K, Map v term))
cont (K
k, Map v term
env')) (StateT (Map v term) Failing ()
-> Map v term -> Failing (Map v term)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT (JL formula -> JL formula -> StateT (Map v term) Failing ()
forall lit1 lit2 atom1 atom2 (m :: * -> *) term v.
(IsLiteral lit1, JustLiteral lit2, HasApply atom1, HasApply atom2,
Unify m (atom1, atom2), term ~ UTermOf (atom1, atom2),
v ~ TVarOf term, atom1 ~ AtomOf lit1, term ~ TermOf atom1,
atom2 ~ AtomOf lit2, term ~ TermOf atom2, MonadFail m) =>
lit1 -> lit2 -> StateT (Map v term) m ()
unify_complements JL formula
fm' JL formula
l) Map v term
env)
tabrefute :: (IsFirstOrder formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom),
atom ~ AtomOf formula, term ~ TermOf atom, v ~ TVarOf term) =>
Maybe Depth -> [formula] -> Failing ((K, Map v term), Depth)
tabrefute :: forall formula atom term v.
(IsFirstOrder formula, Unify Failing (atom, atom),
term ~ UTermOf (atom, atom), atom ~ AtomOf formula,
term ~ TermOf atom, v ~ TVarOf term) =>
Maybe Depth -> [formula] -> Failing ((K, Map v term), Depth)
tabrefute Maybe Depth
limit [formula]
fms =
let r :: Failing (((K, Map v term), Depth), Depth)
r = (Depth -> Failing ((K, Map v term), Depth))
-> Depth
-> Maybe Depth
-> Failing (((K, Map v term), Depth), Depth)
forall t.
(Depth -> Failing t) -> Depth -> Maybe Depth -> Failing (t, Depth)
deepen (\Depth
n -> (,Depth
n) ((K, Map v term) -> ((K, Map v term), Depth))
-> Failing (K, Map v term) -> Failing ((K, Map v term), Depth)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RWS () () () (Failing (K, Map v term))
-> () -> () -> Failing (K, Map v term)
forall r s a. RWS r () s a -> r -> s -> a
evalRS ([formula] -> Depth -> RWS () () () (Failing (K, Map v term))
forall formula atom term v function.
(IsFirstOrder formula, Unify Failing (atom, atom),
term ~ UTermOf (atom, atom), atom ~ AtomOf formula,
term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term) =>
[formula] -> Depth -> RWS () () () (Failing (K, Map v term))
tableau [formula]
fms Depth
n) () ()) (Int -> Depth
Depth Int
0) Maybe Depth
limit in
([[Char]] -> Failing ((K, Map v term), Depth))
-> ((((K, Map v term), Depth), Depth)
-> Failing ((K, Map v term), Depth))
-> Failing (((K, Map v term), Depth), Depth)
-> Failing ((K, Map v term), Depth)
forall b a. ([[Char]] -> b) -> (a -> b) -> Failing a -> b
failing [[Char]] -> Failing ((K, Map v term), Depth)
forall a. [[Char]] -> Failing a
Failure (((K, Map v term), Depth) -> Failing ((K, Map v term), Depth)
forall a. a -> Failing a
Success (((K, Map v term), Depth) -> Failing ((K, Map v term), Depth))
-> ((((K, Map v term), Depth), Depth) -> ((K, Map v term), Depth))
-> (((K, Map v term), Depth), Depth)
-> Failing ((K, Map v term), Depth)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((K, Map v term), Depth), Depth) -> ((K, Map v term), Depth)
forall a b. (a, b) -> a
fst) Failing (((K, Map v term), Depth), Depth)
r
tab :: (IsFirstOrder formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Pretty formula, HasSkolem function,
atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
v ~ TVarOf term, v ~ SVarOf function) =>
Maybe Depth -> formula -> Failing ((K, Map v term), Depth)
tab :: forall formula atom term function v.
(IsFirstOrder formula, Unify Failing (atom, atom),
term ~ UTermOf (atom, atom), Pretty formula, HasSkolem function,
atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
v ~ TVarOf term, v ~ SVarOf function) =>
Maybe Depth -> formula -> Failing ((K, Map v term), Depth)
tab Maybe Depth
limit formula
fm =
let sfm :: formula
sfm = SkolemT Identity function formula -> formula
forall function a.
IsFunction function =>
SkolemT Identity function a -> a
runSkolem (formula -> SkolemT Identity function formula
forall formula function (m :: * -> *) atom term.
(IsFirstOrder formula, HasSkolem function, Monad m,
atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
VarOf formula ~ SVarOf function) =>
formula -> SkolemT m function formula
askolemize(formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.)(formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
generalize formula
fm))) in
if formula -> Maybe Bool
forall formula. IsFormula formula => formula -> Maybe Bool
asBool formula
sfm Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False then ([Char] -> Failing ((K, Map v term), Depth)
forall a. HasCallStack => [Char] -> a
error [Char]
"Tableaux.tab") else Maybe Depth -> [formula] -> Failing ((K, Map v term), Depth)
forall formula atom term v.
(IsFirstOrder formula, Unify Failing (atom, atom),
term ~ UTermOf (atom, atom), atom ~ AtomOf formula,
term ~ TermOf atom, v ~ TVarOf term) =>
Maybe Depth -> [formula] -> Failing ((K, Map v term), Depth)
tabrefute Maybe Depth
limit [formula
sfm]
p38 :: Test
p38 :: Test
p38 =
let [[SkTerm] -> Formula
p, [SkTerm] -> Formula
r] = [PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
"P", PredOf (FOL Predicate SkTerm)
-> [TermOf (FOL Predicate SkTerm)] -> Formula
forall formula atom.
(IsFormula formula, HasApply atom, atom ~ AtomOf formula) =>
PredOf atom -> [TermOf atom] -> formula
pApp Predicate
PredOf (FOL Predicate SkTerm)
"R"] :: [[SkTerm] -> Formula]
[SkTerm
a, SkTerm
w, SkTerm
x, SkTerm
y, SkTerm
z] = [TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"a", TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"w", TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"x", TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"y", TVarOf SkTerm -> SkTerm
forall term. IsTerm term => TVarOf term -> term
vt TVarOf SkTerm
V
"z"] :: [SkTerm]
fm :: Formula
fm = (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"x"
([SkTerm] -> Formula
p[SkTerm
a] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. ([SkTerm] -> Formula
p[SkTerm
x] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"y" ([SkTerm] -> Formula
p[SkTerm
y] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. [SkTerm] -> Formula
r[SkTerm
x,SkTerm
y]))) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>.
(VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"z" (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"w" ([SkTerm] -> Formula
p[SkTerm
z] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. [SkTerm] -> Formula
r[SkTerm
x,SkTerm
w] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. [SkTerm] -> Formula
r[SkTerm
w,SkTerm
z]))))) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>.
(VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
for_all V
VarOf Formula
"x"
((Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)([SkTerm] -> Formula
p[SkTerm
a]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. [SkTerm] -> Formula
p[SkTerm
x] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"z" (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"w" ([SkTerm] -> Formula
p[SkTerm
z] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. [SkTerm] -> Formula
r[SkTerm
x,SkTerm
w] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. [SkTerm] -> Formula
r[SkTerm
w,SkTerm
z])))) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&.
(Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)([SkTerm] -> Formula
p[SkTerm
a]) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. Formula -> Formula
forall formula. IsLiteral formula => formula -> formula
(.~.)(VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"y" ([SkTerm] -> Formula
p[SkTerm
y] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. [SkTerm] -> Formula
r[SkTerm
x,SkTerm
y])) Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|.
(VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"z" (VarOf Formula -> Formula -> Formula
forall formula.
IsQuantified formula =>
VarOf formula -> formula -> formula
exists V
VarOf Formula
"w" ([SkTerm] -> Formula
p[SkTerm
z] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. [SkTerm] -> Formula
r[SkTerm
x,SkTerm
w] Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. [SkTerm] -> Formula
r[SkTerm
w,SkTerm
z]))))))
expected :: Failing ((K, Map k a), Depth)
expected = ((K, Map k a), Depth) -> Failing ((K, Map k a), Depth)
forall a. a -> Failing a
Success ((Int -> K
K Int
22,
[(k, a)] -> Map k a
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
[(k
"K0",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"x" Int
1))[]),
(k
"K1",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"y" Int
1))[]),
(k
"K10",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"x" Int
2))[]),
(k
"K11",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"z" Int
3))[a
"K13"]),
(k
"K12",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"w" Int
3))[a
"K16"]),
(k
"K13",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"x" Int
2))[]),
(k
"K14",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"y" Int
2))[]),
(k
"K15",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"y" Int
2))[]),
(k
"K16",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"x" Int
2))[]),
(k
"K17",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"y" Int
2))[]),
(k
"K18",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"y" Int
2))[]),
(k
"K19",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"x" Int
2))[]),
(k
"K2",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"z" Int
1))[a
"K0"]),
(k
"K20",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"y" Int
2))[]),
(k
"K21",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"y" Int
2))[]),
(k
"K3",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"w" Int
1))[a
"K0"]),
(k
"K4",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"z" Int
1))[a
"K0"]),
(k
"K5",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"w" Int
1))[a
"K0"]),
(k
"K6",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"z" Int
2))[a
"K8"]),
(k
"K7",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"w" Int
2))[a
"K9"]),
(k
"K8",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"x" Int
2))[]),
(k
"K9",FunOf a -> [a] -> a
forall term. IsTerm term => FunOf term -> [term] -> term
fApp ((SVarOf (FunOf a) -> Int -> FunOf a
forall function.
HasSkolem function =>
SVarOf function -> Int -> function
toSkolem SVarOf (FunOf a)
"x" Int
2))[])]
),
Int -> Depth
Depth Int
4) in
Assertion -> Test
TestCase (Assertion -> Test) -> Assertion -> Test
forall a b. (a -> b) -> a -> b
$ [Char]
-> Failing
((K, Map V (UTermOf (FOL Predicate SkTerm, FOL Predicate SkTerm))),
Depth)
-> Failing
((K, Map V (UTermOf (FOL Predicate SkTerm, FOL Predicate SkTerm))),
Depth)
-> Assertion
forall a.
(?loc::CallStack, Eq a, Pretty a) =>
[Char] -> a -> a -> Assertion
assertEqual' [Char]
"p38, p. 178" Failing
((K, Map V (UTermOf (FOL Predicate SkTerm, FOL Predicate SkTerm))),
Depth)
forall {a} {k}.
(IsTerm a, HasSkolem (FunOf a), IsString k, Ord k) =>
Failing ((K, Map k a), Depth)
expected (Maybe Depth
-> Formula
-> Failing
((K, Map V (UTermOf (FOL Predicate SkTerm, FOL Predicate SkTerm))),
Depth)
forall formula atom term function v.
(IsFirstOrder formula, Unify Failing (atom, atom),
term ~ UTermOf (atom, atom), Pretty formula, HasSkolem function,
atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
v ~ TVarOf term, v ~ SVarOf function) =>
Maybe Depth -> formula -> Failing ((K, Map v term), Depth)
tab Maybe Depth
forall a. Maybe a
Nothing Formula
fm)
splittab :: forall formula atom term v function.
(IsFirstOrder formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Ord formula, Pretty formula, HasSkolem function,
atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
v ~ TVarOf term, v ~ SVarOf function) =>
formula -> [Failing ((K, Map v term), Depth)]
splittab :: forall formula atom term v function.
(IsFirstOrder formula, Unify Failing (atom, atom),
term ~ UTermOf (atom, atom), Ord formula, Pretty formula,
HasSkolem function, atom ~ AtomOf formula, term ~ TermOf atom,
function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) =>
formula -> [Failing ((K, Map v term), Depth)]
splittab formula
fm =
(([formula] -> Failing ((K, Map v term), Depth))
-> [[formula]] -> [Failing ((K, Map v term), Depth)]
forall a b. (a -> b) -> [a] -> [b]
List.map (Maybe Depth -> [formula] -> Failing ((K, Map v term), Depth)
forall formula atom term v.
(IsFirstOrder formula, Unify Failing (atom, atom),
term ~ UTermOf (atom, atom), atom ~ AtomOf formula,
term ~ TermOf atom, v ~ TVarOf term) =>
Maybe Depth -> [formula] -> Failing ((K, Map v term), Depth)
tabrefute Maybe Depth
forall a. Maybe a
Nothing) ([[formula]] -> [Failing ((K, Map v term), Depth)])
-> (formula -> [[formula]])
-> formula
-> [Failing ((K, Map v term), Depth)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (Set formula) -> [[formula]]
forall {a}. Set (Set a) -> [[a]]
ssll (Set (Set formula) -> [[formula]])
-> (formula -> Set (Set formula)) -> formula -> [[formula]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. formula -> Set (Set formula)
forall fof atom term function v.
(IsFirstOrder fof, Ord fof, atom ~ AtomOf fof, term ~ TermOf atom,
function ~ FunOf term, v ~ VarOf fof, v ~ TVarOf term) =>
fof -> Set (Set fof)
simpdnf' (formula -> Set (Set formula))
-> (formula -> formula) -> formula -> Set (Set formula)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SkolemT Identity function formula -> formula
forall function a.
IsFunction function =>
SkolemT Identity function a -> a
runSkolem (SkolemT Identity function formula -> formula)
-> (formula -> SkolemT Identity function formula)
-> formula
-> formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. formula -> SkolemT Identity function formula
forall formula function (m :: * -> *) atom term.
(IsFirstOrder formula, HasSkolem function, Monad m,
atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term,
VarOf formula ~ SVarOf function) =>
formula -> SkolemT m function formula
askolemize (formula -> SkolemT Identity function formula)
-> (formula -> formula)
-> formula
-> SkolemT Identity function formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) (formula -> formula) -> (formula -> formula) -> formula -> formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. formula -> formula
forall formula. IsFirstOrder formula => formula -> formula
generalize) formula
fm
where ssll :: Set (Set a) -> [[a]]
ssll = (Set a -> [a]) -> [Set a] -> [[a]]
forall a b. (a -> b) -> [a] -> [b]
List.map Set a -> [a]
forall a. Set a -> [a]
Set.toList ([Set a] -> [[a]])
-> (Set (Set a) -> [Set a]) -> Set (Set a) -> [[a]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (Set a) -> [Set a]
forall a. Set a -> [a]
Set.toList
testTableaux :: Test
testTableaux :: Test
testTableaux = [Char] -> Test -> Test
TestLabel [Char]
"Tableaux" ([Test] -> Test
TestList [Test
p20, Test
p19, Test
p38])