gregorbednov/tern_solver
gregorbednov/tern_solver
Watch
1
1
Fork
You've already forked tern_solver
 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Compare commits

base: gregorbednov:main
Branches Tags
gregorbednov:main
gregorbednov:codex/edit-readme.md-and-fix-typo
gregorbednov:initial
..
compare: gregorbednov:initial
Branches Tags
gregorbednov:main
gregorbednov:codex/edit-readme.md-and-fix-typo
gregorbednov:initial
6 changed files with 205 additions and 314 deletions
Download patch file Download diff file Expand all files Collapse all files

118
Main.hs
View file

@ -1,99 +1,51 @@
module Main (main) where module Main (main) where
import Prelude (IO, String, getContents, lines, map, print,
import Data.Foldable (Foldable, any) otherwise, Bool(..), filter, id, unlines,
import Data.List (head, tail) mapM_, ($), elem, notElem, (||), putStrLn, read, (.))
import Data.Maybe (isNothing) import Ternary.Statement (Statement (..), st)
import GHC.Base (Maybe (..), (==)) import Ternary.Universum (Universum (..), universum)
import Ternary.Vee (cleared, think)
import System.Environment (getArgs) import System.Environment (getArgs)
import Ternary.Statement (Statement (..), st) import Data.Foldable (Foldable)
import Ternary.Term (Item (..), Term (..))
import Ternary.Universum (Universum (..), universum)
import Ternary.Vee (cleared, hasContradiction, think)
import Prelude
( Bool (..),
IO,
String,
elem,
filter,
getContents,
id,
lines,
map,
mapM_,
notElem,
otherwise,
print,
putStrLn,
read,
unlines,
($),
(.),
(||),
)
mainSolve :: Universum -> Bool -> IO () main2 :: Universum -> Bool -> IO ()
mainSolve u onlyNew = do main2 u onlyNew = do
strs <- getContents strs <- getContents
let statements = map str2vee . lines $ strs let statements = map str2vee . lines $ strs
str2vee x = st (read x :: Statement String) str2vee x = st (read x :: Statement String)
mapM_ print mapM_ print
. (if onlyNew then filter (`notElem` statements) else id) . (if onlyNew then filter (`notElem` statements) else id)
. cleared . cleared
. think (universum u) . think (universum u) $ statements
$ statements
mainProve :: Universum -> Bool -> IO ()
mainProve u onlyNew = do
strs <- getContents
let statements = map str2vee . tail . lines $ strs
proveThis = str2vee . head . lines $ strs
str2vee x = st (read x :: Statement String)
results = cleared . think (universum u) $ statements
anyContradictions = any (hasContradiction proveThis) results
proof = swapNothingJF $ if anyContradictions then Nothing else Just (Item recalc == Item results)
recalc = cleared . think (universum u) $ proveThis : statements
swapNothingJF x
| isNothing x = Just False
| x == Just False = Nothing
| x == Just True = Just True
print recalc
putStrLn ""
print results
putStrLn ""
print proof
withArgs :: (String -> Bool) -> IO () withArgs :: (String -> Bool) -> IO ()
withArgs a withArgs a
| a "-h" || a "--help" = | a "-h" || a "--help" = putStrLn . unlines $
putStrLn . unlines $ ["Logical statement solver",
[ "Logical statement solver", "Usage: solver [PARAMETERS]",
"Usage: solver [PARAMETERS]", "",
"", "Designed according to N.P.Brousentsov works",
"Designed according to N.P.Brousentsov works", "and Lewis Carrol diagram. PARAMETERS:",
"and Lewis Carrol diagram. PARAMETERS:", "",
"", "--aristotle, -A\tuse Aristotle logical universum VxVx' for each x",
"--aristotle, -A\tuse Aristotle logical universum VxVx' for each x", "--new, -n\tfilters only 'new' facts, excluding defined",
"--new, -n\tfilters only 'new' facts, excluding defined", "--help, -h\tshows this help",
"--help, -h\tshows this help", "--version, -v\tshows this version",
"--version, -v\tshows this version", "",
"", "Takes statement \"Socrates is a human\" in such format, e.g.",
"Takes statement \"Socrates is a human\" in such format, e.g.", "",
"", "A \"Socrates\" \"human\"",
"A \"Socrates\" \"human\"", "",
"", "There are A, E, O, I traditional statements exist.",
"There are A, E, O, I traditional statements.", "Also there are A~, E~, O~, I~ with negated first part"
"Also there are A~, E~, O~, I~ with negated first part" ]
]
| a "--version" || a "-v" = putStrLn "v1.0.2" | a "--version" || a "-v" = putStrLn "v1.0.2"
| a "--prove" = mainProve Aristotle False | otherwise = main2 uni onlyNew where
| otherwise = mainSolve uni onlyNew onlyNew = a "--new" || a "-n"
where uni =
onlyNew = a "--new" || a "-n" if a "-A" || a "--aristotle"
uni = then Aristotle
if a "-A" || a "--aristotle" else Empty
then Aristotle
else Empty
main :: IO () main :: IO ()
main = do main = do

2
README.md
View file

@ -6,7 +6,7 @@
Как справедливо отмечает польская математическая традиция с одной стороны и Н.П.Брусенцов с другой стороны, символ "существования" некоторого предмета, записываемый как ∀, на самом деле имеет тесную связь с дизъюнкцией: ∨. Конкретно, это "интегральная" дизъюнкция, дизъюнкция по множеству: Vx значит, что мы пытаемся перебрать все предметы на предмет соответствия x, и если хотя бы один из них подходит, то дизъюнкция по множеству так же существует на всём множестве. Как справедливо отмечает польская математическая традиция с одной стороны и Н.П.Брусенцов с другой стороны, символ "существования" некоторого предмета, записываемый как ∀, на самом деле имеет тесную связь с дизъюнкцией: ∨. Конкретно, это "интегральная" дизъюнкция, дизъюнкция по множеству: Vx значит, что мы пытаемся перебрать все предметы на предмет соответствия x, и если хотя бы один из них подходит, то дизъюнкция по множеству так же существует на всём множестве.
Расширяя множества до нечётких (в которых элементы могут достоверно присутствовать, достоверно отсутствовать и быть свободными), мы можем рассматривать логические понятия во всех их соотношениях. Расширяя множества до нечётких (в которых элементы могут достоверно присутствовать, достоверно отсуствовать и быть свободными), мы можем рассматривать логические понятия во всех их соотношениях.
Современная математическая логика, как правило, работает совмещением признаков (или анти-признаки, то есть несоответстветствия признакам) предметов булевской алгеброй, без нечётких множеств. Такой подход позволяет достичь больших успехов в описании отдельно взятого предмета в заранее определённой системе понятий. В то же время, такой подход плохо подходит для описания **систем**, точнее, он требует описывать системы как единые предметы, что чаще всего крайне неестественно. Современная математическая логика, как правило, работает совмещением признаков (или анти-признаки, то есть несоответстветствия признакам) предметов булевской алгеброй, без нечётких множеств. Такой подход позволяет достичь больших успехов в описании отдельно взятого предмета в заранее определённой системе понятий. В то же время, такой подход плохо подходит для описания **систем**, точнее, он требует описывать системы как единые предметы, что чаще всего крайне неестественно.

38
Ternary/Statement.hs
View file

@ -1,18 +1,14 @@
module Ternary.Statement (Statement(..), st) where module Ternary.Statement (Statement(..), st) where
import Ternary.Term (Vee, Term(..), Item(..)) import Ternary.Term (Vee, Term(..), Item(..))
data Statement a = A a a -- Affirmo (general affirmative)
data StatementKind = A | I | E | O | A' | I' | E' | O' deriving (Eq, Show, Read) | I a a -- affIrmo (private affirmative)
data Statement a = Statement StatementKind a a deriving (Eq, Read) | E a a -- nEgo (general negative)
| O a a -- negO (private negative)
instance Show a => Show (Statement a) where | A' a a
show (Statement A x y) = "Every " ++ show x ++ " is " ++ show y | I' a a
show (Statement I x y) = "Some of " ++ show x ++ " is " ++ show y | E' a a
show (Statement E x y) = "None of " ++ show x ++ " is " ++ show y | O' a a
show (Statement O x y) = "Some of " ++ show x ++ " isn't " ++ show y deriving (Eq, Show, Read)
show (Statement A' x y) = "Every non-" ++ show x ++ " is " ++ show y
show (Statement I' x y) = "Some of non-" ++ show x ++ " is " ++ show y
show (Statement E' x y) = "None of non-" ++ show x ++ " is " ++ show y
show (Statement O' x y) = "Some of non-" ++ show x ++ " isn't " ++ show y
inv :: (Eq a) => Term a -> Term a inv :: (Eq a) => Term a -> Term a
inv (Term p x) = Term (not p) x inv (Term p x) = Term (not p) x
@ -24,11 +20,11 @@ i v x y
| x == y = Term v . Item $ [x] | x == y = Term v . Item $ [x]
st :: (Eq a) => Statement a -> Vee a st :: (Eq a) => Statement a -> Vee a
st (Statement A x y) = i False (Term True x) (Term False y) st (A x y) = i False (Term True x) (Term False y)
st (Statement I x y) = i True (Term True x) (Term True y) st (I x y) = i True (Term True x) (Term True y)
st (Statement E x y) = i False (Term True x) (Term True y) st (E x y) = i False (Term True x) (Term True y)
st (Statement O x y) = i True (Term True x) (Term False y) st (O x y) = i True (Term True x) (Term False y)
st (Statement A' x y) = i False (Term False x) (Term False y) st (A' x y) = i False (Term False x) (Term False y)
st (Statement I' x y) = i True (Term False x) (Term True y) st (I' x y) = i True (Term False x) (Term True y)
st (Statement E' x y) = i False (Term False x) (Term True y) st (E' x y) = i False (Term False x) (Term True y)
st (Statement O' x y) = i True (Term False x) (Term False y) st (O' x y) = i True (Term False x) (Term False y)

160
Ternary/Vee.hs
View file

@ -1,118 +1,68 @@
module Ternary.Vee (isObvious, hasContradiction, newFact, cleared, think) where module Ternary.Vee (isObvious, newFact, cleared, think) where
import Data.List (head, intersect, length, nub, null, union, (\\))
import Data.Foldable (concatMap) import Data.Maybe (Maybe (Nothing), mapMaybe)
import Data.List import Prelude (Bool (False, True), Eq, any, foldr, fst, map,
( elem, not, notElem, otherwise, return, snd, ($), (&&),
filter, (.), (/=), (<$>), (<*>), (=<<), (==))
head, import Ternary.Term (Item (..), Term (..), Vee)
intersect,
iterate,
length,
nub,
null,
union,
(\\),
)
import Data.Maybe (Maybe (Nothing), mapMaybe)
import GHC.Base ((<), (>))
import GHC.Maybe (Maybe (..))
import Ternary.Term (Item (..), Term (..), Vee)
import Prelude
( Bool (False, True),
Eq,
any,
foldr,
fst,
map,
not,
notElem,
otherwise,
return,
snd,
($),
(&&),
(.),
(/=),
(<$>),
(<*>),
(=<<),
(==),
)
type Knowledge a = [Vee a]
type InferenceRule a = Vee a -> Vee a -> (Knowledge a, Maybe (Vee a))
isSubsetOf :: (Eq a) => [a] -> [a] -> Bool isSubsetOf :: (Eq a) => [a] -> [a] -> Bool
a `isSubsetOf` b = nda && not ndb a `isSubsetOf` b = nda && not ndb
where where
nda = null $ a \\ b nda = null $ a \\ b
ndb = null $ b \\ a ndb = null $ b \\ a
isObvious :: (Eq a) => Vee a -> Vee a -> Bool isObvious :: (Eq a) => Vee a -> Vee a -> Bool
isObvious (Term x (Item a)) (Term y (Item b)) isObvious (Term x (Item a)) (Term y (Item b))
| x /= y = False | x /= y = False
| x = a `isSubsetOf` b | x = a `isSubsetOf` b
| not x = b `isSubsetOf` a | not x = b `isSubsetOf` a
hasContradiction :: (Eq a) => Vee a -> Vee a -> Bool newFact :: (Eq a) => Vee a -> Vee a -> ([Vee a], Maybe (Vee a))
hasContradiction (Term x (Item a)) (Term y (Item b))
| a == b && x /= y = True
| a `isSubsetOf` b && x < y = True
| b `isSubsetOf` a && x > y = True
| otherwise = False
notT :: Term a -> Term a
notT (Term x v) = Term (not x) v
rulePosFromNeg :: (Eq a) => InferenceRule a
rulePosFromNeg (Term False (Item negSet)) positive@(Term True (Item posSet))
| length diff /= 1 = ([], Nothing)
| missing `elem` posSet = ([], Nothing)
| otherwise = ([positive], Just (Term True (Item (missing : posSet))))
where
diff = negSet \\ posSet
missing = notT (head diff)
ruleNegFromNeg :: (Eq a) => InferenceRule a
ruleNegFromNeg (Term False (Item i0)) (Term False (Item i1))
| length evidence /= 1 = ([], Nothing)
| null diff0 && null diff1 = (map (Term False . Item) [i0, i1], Just (Term False (Item result)))
| otherwise = ([], Just (Term False (Item result)))
where
evidence = map notT i0 `intersect` i1
diff0 = (i0 \\ i1) \\ map notT evidence
diff1 = (i1 \\ i0) \\ evidence
result = (i0 `intersect` i1) `union` diff0 `union` diff1
newFact :: (Eq a) => InferenceRule a
newFact a@(Term True _) b@(Term False _) = newFact b a newFact a@(Term True _) b@(Term False _) = newFact b a
newFact a@(Term False _) b@(Term True _) = rulePosFromNeg a b newFact (Term False (Item iF)) tT@(Term True (Item iT))
newFact a@(Term False _) b@(Term False _) = ruleNegFromNeg a b | length ldF /= 1 = ([], Nothing)
| otherwise =
if d'F `notElem` iT
then (return tT, return (Term True (Item (d'F:iT))))
else ([], Nothing)
where
ldF = iF \\ iT
d'F = notT . head $ ldF
notT (Term x v) = Term (not x) v
newFact (Term False (Item i0)) (Term False (Item i1))
| length e /= 1 = ([], Nothing)
| otherwise =
if null d0 && null d1
then (map (Term False . Item) [i0, i1], vee0)
else ([], vee0)
where
notT (Term x v) = Term (not x) v
terms = (i0 `intersect` i1) `union` d0 `union` d1
e = map notT i0 `intersect` i1
d0 = (i0 \\ i1) \\ map notT e
d1 = (i1 \\ i0) \\ e
vee0 = return (Term False (Item terms))
newFact _ _ = ([], Nothing) newFact _ _ = ([], Nothing)
next :: (Eq a) => (Knowledge a, Knowledge a) -> (Knowledge a, Knowledge a) pseudofix :: (Eq a) => (a -> a) -> a -> a
next (old, new) = (old `union` new \\ used, added) pseudofix f x0
where | y == y' = y
results = [newFact o n | o <- old, n <- new] | otherwise = y'
used = concatMap fst results where
added = mapMaybe snd results y = f x0
y' = f y
applyFacts :: (Eq a) => Knowledge a -> Knowledge a -> Knowledge a next :: (Eq a) => ([Vee a], [Vee a]) -> ([Vee a], [Vee a])
applyFacts old new = next (o,n) = (o `union` n \\ (fst =<< r), mapMaybe snd r)
fst . head . dropStable $ iterate next (old, new) where
where r = newFact <$> o <*> n
dropStable (x : y : xs)
| x == y = [x]
| otherwise = dropStable (y : xs)
dropStable _ = []
cleared :: (Eq a) => Knowledge a -> Knowledge a applyFacts :: (Eq a) => [Vee a] -> [Vee a] -> [Vee a]
cleared vees = nub $ filter (not . isRedundant) vees applyFacts old new = fst $ pseudofix next (old, new)
where
isRedundant v = any (isObvious v) vees
think :: (Eq a) => (Knowledge a -> Knowledge a) -> Knowledge a -> Knowledge a cleared :: (Eq a) => [Vee a] -> [Vee a]
think addition = foldr (applyFacts . withUni . return) [] cleared vees = nub [vee | vee <- vees, not $ any (isObvious vee) vees]
where
think :: (Eq a) => ([Vee a]->[Vee a]) -> [Vee a] -> [Vee a]
think addition = foldr (applyFacts . withUni . return) [] where
withUni vees = applyFacts (addition vees) vees withUni vees = applyFacts (addition vees) vees

192
Tests/syllotest
View file

@ -1,96 +1,96 @@
(Statement A "y" "z", Statement A "x" "y", Statement A "x" "z") (A "y" "z", A "x" "y", A "x" "z")
(Statement A "y" "z", Statement E' "x" "y", Statement E' "x" "z") (A "y" "z", E' "x" "y", E' "x" "z")
(Statement E "y" "z", Statement A "x" "y", Statement E "x" "z") (E "y" "z", A "x" "y", E "x" "z")
(Statement E "y" "z", Statement E' "x" "y", Statement A' "x" "z") (E "y" "z", E' "x" "y", A' "x" "z")
(Statement A "y" "z", Statement A "x" "y", Statement I "x" "z") (A "y" "z", A "x" "y", I "x" "z")
(Statement A "y" "z", Statement A "x" "y", Statement I' "x" "z") (A "y" "z", A "x" "y", I' "x" "z")
(Statement A "y" "z", Statement E' "x" "y", Statement O "x" "z") (A "y" "z", E' "x" "y", O "x" "z")
(Statement A "y" "z", Statement E' "x" "y", Statement O' "x" "z") (A "y" "z", E' "x" "y", O' "x" "z")
(Statement E "y" "z", Statement A "x" "y", Statement O "x" "z") (E "y" "z", A "x" "y", O "x" "z")
(Statement E "y" "z", Statement A "x" "y", Statement O' "x" "z") (E "y" "z", A "x" "y", O' "x" "z")
(Statement E "y" "z", Statement E' "x" "y", Statement I "x" "z") (E "y" "z", E' "x" "y", I "x" "z")
(Statement E "y" "z", Statement E' "x" "y", Statement I' "x" "z") (E "y" "z", E' "x" "y", I' "x" "z")
(Statement A "y" "z", Statement A' "x" "y", Statement I "x" "z") (A "y" "z", A' "x" "y", I "x" "z")
(Statement A "y" "z", Statement E "x" "y", Statement O' "x" "z") (A "y" "z", E "x" "y", O' "x" "z")
(Statement E "y" "z", Statement A' "x" "y", Statement O "x" "z") (E "y" "z", A' "x" "y", O "x" "z")
(Statement E "y" "z", Statement E "x" "y", Statement I' "x" "z") (E "y" "z", E "x" "y", I' "x" "z")
(Statement A "y" "z", Statement I "x" "y", Statement I "x" "z") (A "y" "z", I "x" "y", I "x" "z")
(Statement A "y" "z", Statement O' "x" "y", Statement O' "x" "z") (A "y" "z", O' "x" "y", O' "x" "z")
(Statement E "y" "z", Statement I "x" "y", Statement O "x" "z") (E "y" "z", I "x" "y", O "x" "z")
(Statement E "y" "z", Statement O' "x" "y", Statement I' "x" "z") (E "y" "z", O' "x" "y", I' "x" "z")
(Statement I "y" "z", Statement A' "x" "y", Statement I "x" "z") (I "y" "z", A' "x" "y", I "x" "z")
(Statement I "y" "z", Statement E "x" "y", Statement O' "x" "z") (I "y" "z", E "x" "y", O' "x" "z")
(Statement O "y" "z", Statement A' "x" "y", Statement O "x" "z") (O "y" "z", A' "x" "y", O "x" "z")
(Statement O "y" "z", Statement E "x" "y", Statement I' "x" "z") (O "y" "z", E "x" "y", I' "x" "z")
(Statement A "z" "y", Statement A' "x" "y", Statement A' "x" "z") (A "z" "y", A' "x" "y", A' "x" "z")
(Statement A "z" "y", Statement E "x" "y", Statement E "x" "z") (A "z" "y", E "x" "y", E "x" "z")
(Statement E "z" "y", Statement A "x" "y", Statement E "x" "z") (E "z" "y", A "x" "y", E "x" "z")
(Statement E "z" "y", Statement E' "x" "y", Statement A' "x" "z") (E "z" "y", E' "x" "y", A' "x" "z")
(Statement A "z" "y", Statement A' "x" "y", Statement I "x" "z") (A "z" "y", A' "x" "y", I "x" "z")
(Statement A "z" "y", Statement A' "x" "y", Statement I' "x" "z") (A "z" "y", A' "x" "y", I' "x" "z")
(Statement A "z" "y", Statement E "x" "y", Statement O "x" "z") (A "z" "y", E "x" "y", O "x" "z")
(Statement A "z" "y", Statement E "x" "y", Statement O' "x" "z") (A "z" "y", E "x" "y", O' "x" "z")
(Statement E "z" "y", Statement A "x" "y", Statement O "x" "z") (E "z" "y", A "x" "y", O "x" "z")
(Statement E "z" "y", Statement A "x" "y", Statement O' "x" "z") (E "z" "y", A "x" "y", O' "x" "z")
(Statement E "z" "y", Statement E' "x" "y", Statement I "x" "z") (E "z" "y", E' "x" "y", I "x" "z")
(Statement E "z" "y", Statement E' "x" "y", Statement I' "x" "z") (E "z" "y", E' "x" "y", I' "x" "z")
(Statement A "z" "y", Statement A "x" "y", Statement I' "x" "z") (A "z" "y", A "x" "y", I' "x" "z")
(Statement A "z" "y", Statement E' "x" "y", Statement O "x" "z") (A "z" "y", E' "x" "y", O "x" "z")
(Statement E "z" "y", Statement A' "x" "y", Statement O "x" "z") (E "z" "y", A' "x" "y", O "x" "z")
(Statement E "z" "y", Statement E "x" "y", Statement I' "x" "z") (E "z" "y", E "x" "y", I' "x" "z")
(Statement A "z" "y", Statement I' "x" "y", Statement I' "x" "z") (A "z" "y", I' "x" "y", I' "x" "z")
(Statement A "z" "y", Statement O "x" "y", Statement O "x" "z") (A "z" "y", O "x" "y", O "x" "z")
(Statement E "z" "y", Statement I "x" "y", Statement O "x" "z") (E "z" "y", I "x" "y", O "x" "z")
(Statement E "z" "y", Statement O' "x" "y", Statement I' "x" "z") (E "z" "y", O' "x" "y", I' "x" "z")
(Statement I "z" "y", Statement A' "x" "y", Statement I "x" "z") (I "z" "y", A' "x" "y", I "x" "z")
(Statement I "z" "y", Statement E "x" "y", Statement O' "x" "z") (I "z" "y", E "x" "y", O' "x" "z")
(Statement O "z" "y", Statement A "x" "y", Statement O' "x" "z") (O "z" "y", A "x" "y", O' "x" "z")
(Statement O "z" "y", Statement E' "x" "y", Statement I "x" "z") (O "z" "y", E' "x" "y", I "x" "z")
(Statement A "y" "z", Statement A' "y" "x", Statement A "x" "z") (A "y" "z", A' "y" "x", A "x" "z")
(Statement A "y" "z", Statement E' "y" "x", Statement E' "x" "z") (A "y" "z", E' "y" "x", E' "x" "z")
(Statement E "y" "z", Statement A' "y" "x", Statement E "x" "z") (E "y" "z", A' "y" "x", E "x" "z")
(Statement E "y" "z", Statement E' "y" "x", Statement A' "x" "z") (E "y" "z", E' "y" "x", A' "x" "z")
(Statement A "y" "z", Statement A' "y" "x", Statement I "x" "z") (A "y" "z", A' "y" "x", I "x" "z")
(Statement A "y" "z", Statement A' "y" "x", Statement I' "x" "z") (A "y" "z", A' "y" "x", I' "x" "z")
(Statement A "y" "z", Statement E' "y" "x", Statement O "x" "z") (A "y" "z", E' "y" "x", O "x" "z")
(Statement A "y" "z", Statement E' "y" "x", Statement O' "x" "z") (A "y" "z", E' "y" "x", O' "x" "z")
(Statement E "y" "z", Statement A' "y" "x", Statement O "x" "z") (E "y" "z", A' "y" "x", O "x" "z")
(Statement E "y" "z", Statement A' "y" "x", Statement O' "x" "z") (E "y" "z", A' "y" "x", O' "x" "z")
(Statement E "y" "z", Statement E' "y" "x", Statement I "x" "z") (E "y" "z", E' "y" "x", I "x" "z")
(Statement E "y" "z", Statement E' "y" "x", Statement I' "x" "z") (E "y" "z", E' "y" "x", I' "x" "z")
(Statement A "y" "z", Statement A "y" "x", Statement I "x" "z") (A "y" "z", A "y" "x", I "x" "z")
(Statement A "y" "z", Statement E "y" "x", Statement O' "x" "z") (A "y" "z", E "y" "x", O' "x" "z")
(Statement E "y" "z", Statement A "y" "x", Statement O "x" "z") (E "y" "z", A "y" "x", O "x" "z")
(Statement E "y" "z", Statement E "y" "x", Statement I' "x" "z") (E "y" "z", E "y" "x", I' "x" "z")
(Statement A "y" "z", Statement I "y" "x", Statement I "x" "z") (A "y" "z", I "y" "x", I "x" "z")
(Statement A "y" "z", Statement O "y" "x", Statement O' "x" "z") (A "y" "z", O "y" "x", O' "x" "z")
(Statement E "y" "z", Statement I "y" "x", Statement O "x" "z") (E "y" "z", I "y" "x", O "x" "z")
(Statement E "y" "z", Statement O "y" "x", Statement I' "x" "z") (E "y" "z", O "y" "x", I' "x" "z")
(Statement I "y" "z", Statement A "y" "x", Statement I "x" "z") (I "y" "z", A "y" "x", I "x" "z")
(Statement I "y" "z", Statement E "y" "x", Statement O' "x" "z") (I "y" "z", E "y" "x", O' "x" "z")
(Statement O "y" "z", Statement A "y" "x", Statement O "x" "z") (O "y" "z", A "y" "x", O "x" "z")
(Statement O "y" "z", Statement E "y" "x", Statement I' "x" "z") (O "y" "z", E "y" "x", I' "x" "z")
(Statement A "z" "y", Statement A "y" "x", Statement A' "x" "z") (A "z" "y", A "y" "x", A' "x" "z")
(Statement A "z" "y", Statement E "y" "x", Statement E "x" "z") (A "z" "y", E "y" "x", E "x" "z")
(Statement E "z" "y", Statement A' "y" "x", Statement E "x" "z") (E "z" "y", A' "y" "x", E "x" "z")
(Statement E "z" "y", Statement E' "y" "x", Statement A' "x" "z") (E "z" "y", E' "y" "x", A' "x" "z")
(Statement A "z" "y", Statement A "y" "x", Statement I "x" "z") (A "z" "y", A "y" "x", I "x" "z")
(Statement A "z" "y", Statement A "y" "x", Statement I' "x" "z") (A "z" "y", A "y" "x", I' "x" "z")
(Statement A "z" "y", Statement E "y" "x", Statement O "x" "z") (A "z" "y", E "y" "x", O "x" "z")
(Statement A "z" "y", Statement E "y" "x", Statement O' "x" "z") (A "z" "y", E "y" "x", O' "x" "z")
(Statement E "z" "y", Statement A' "y" "x", Statement O "x" "z") (E "z" "y", A' "y" "x", O "x" "z")
(Statement E "z" "y", Statement A' "y" "x", Statement O' "x" "z") (E "z" "y", A' "y" "x", O' "x" "z")
(Statement E "z" "y", Statement E' "y" "x", Statement I "x" "z") (E "z" "y", E' "y" "x", I "x" "z")
(Statement E "z" "y", Statement E' "y" "x", Statement I' "x" "z") (E "z" "y", E' "y" "x", I' "x" "z")
(Statement A "z" "y", Statement A' "y" "x", Statement I' "x" "z") (A "z" "y", A' "y" "x", I' "x" "z")
(Statement A "z" "y", Statement E' "y" "x", Statement O "x" "z") (A "z" "y", E' "y" "x", O "x" "z")
(Statement E "z" "y", Statement A "y" "x", Statement O "x" "z") (E "z" "y", A "y" "x", O "x" "z")
(Statement E "z" "y", Statement E "y" "x", Statement I' "x" "z") (E "z" "y", E "y" "x", I' "x" "z")
(Statement A "z" "y", Statement I' "y" "x", Statement I' "x" "z") (A "z" "y", I' "y" "x", I' "x" "z")
(Statement A "z" "y", Statement O' "y" "x", Statement O "x" "z") (A "z" "y", O' "y" "x", O "x" "z")
(Statement E "z" "y", Statement I "y" "x", Statement O "x" "z") (E "z" "y", I "y" "x", O "x" "z")
(Statement E "z" "y", Statement O "y" "x", Statement I' "x" "z") (E "z" "y", O "y" "x", I' "x" "z")
(Statement I "z" "y", Statement A "y" "x", Statement I "x" "z") (I "z" "y", A "y" "x", I "x" "z")
(Statement I "z" "y", Statement E "y" "x", Statement O' "x" "z") (I "z" "y", E "y" "x", O' "x" "z")
(Statement O "z" "y", Statement A' "y" "x", Statement O' "x" "z") (O "z" "y", A' "y" "x", O' "x" "z")
(Statement O "z" "y", Statement E' "y" "x", Statement I "x" "z") (O "z" "y", E' "y" "x", I "x" "z")

7
shell.nix
View file

@ -1,7 +0,0 @@
{ pkgs ? import <nixpkgs> {} }:
pkgs.mkShell {
buildInputs = with pkgs; [
ghc
];
}