>   import List

--- Defining the Data type Prop and creating the show function for it

This is the structure of the data type of our proposition.  It determines the ways that 
a Prop can be consructed, beging TRUE/FALSE (these arn't actually implomented, but can be
implomented if required), or a variable (eg A,B,C etc..), or type of compound formula (ie
AND, OR, NOT, IMPLIES and IFF).  This data type also needs to have equality tested on it

>   type Variable = Char
>   data Prop = TRUE | FALSE |
>               VAR Variable |
>               NOT Prop |
>               AND Prop Prop |
>               OR Prop Prop |
>               IMPLIES Prop Prop |
>               IFF Prop Prop
>               deriving (Eq)

This is the Show function that outputs the propositions as readable sentences.  Whenever a
Prop is outputed, it shows it in the style created in the Show.

>   instance Show Prop where
>       show TRUE = "TRUE"
>       show FALSE = "FALSE"
>       show (VAR c) = [c]
>       show (NOT p) = "(¬" ++ show p ++ ")"
>       show (AND p q) = "(" ++ show p ++ "&" ++ show q ++ ")"
>       show (OR p q) = "(" ++ show p ++ "|" ++ show q ++ ")"
>       show (IMPLIES p q) = "(" ++ show p ++ "=>" ++ show q ++ ")"
>       show (IFF p q) = "(" ++ show p ++ "<=>" ++ show q ++ ")"

The next 3 functions are the ones that control the output to the screen of the tableaux.

This function is the main function you use when you want to find the result.  The syntax 
is "Main> tableaux [prop]" (ie "tableaux box" will give you the tableaux result for 
the box problem).

>   tableaux :: [[Prop]] -> IO ()
>   tableaux x = putStr (displayAll (calculateProp x))

This function displays one branch of the tableaux results, it puts every variable on a
new line to make it easy to look at and understand.

>   display :: [Prop] -> String
>   display [] = []
>   display (x:xs) = (show x) ++ "\n" ++ display xs

This function displays all the branches of the tableaux, by calling the above function.
It then seperates each branch with a space, to make the final output clear.

>   displayAll :: [[Prop]] -> String
>   displayAll [] = []
>   displayAll (x:xs) = display x ++ "\n" ++ displayAll xs

This function is the main function that brings all the seperate parts of calculating a
tableaux together.

>   calculateProp :: [[Prop]] -> [[Prop]]
>   calculateProp x = removeBranch (removeDup (removeConts (reduceRoot x)))

This function finds any identical branches and removes the duplicates.  This is just here
to make the output simplier, because somtimes different branches give the same results as
others, and this just makes the output look more complex.

>   removeBranch :: [[Prop]] -> [[Prop]]
>   removeBranch [] = []
>   removeBranch (x:xs)
>       | x == findBranch x xs = [] ++ removeBranch xs
>       | otherwise = [x] ++ removeBranch xs

This function works in conjunction with the above function to find and remove any 
duplicate braches.

>   findBranch :: [Prop] -> [[Prop]] -> [Prop]
>   findBranch z [] = []
>   findBranch z (x:xs)
>       | z == x    = x
>       | otherwise = findBranch z xs

This function any identical variables and removes the duplicates.  This is just here to
make the output simplier, by removing any unnessary duplicates of variables.

>   removeDup :: [[Prop]] -> [[Prop]]
>   removeDup [] = []
>   removeDup (x:xs) = [(remove x)] ++ removeDup xs

This function is part of the above function, this one works on single lists of Props, 
where as the above one works of lists of lists of Props.

>   remove :: [Prop] -> [Prop]
>   remove [] = []
>   remove (x:xs)
>       | x == findP x xs = [] ++ remove xs
>       | otherwise = [x] ++ remove xs

This function works in conjunction with the above two functions to find and remove 
any duplicate variables.

>   findP :: Prop -> [Prop] -> Prop
>   findP z [] = FALSE
>   findP z (x:xs)
>       | z == x    = x
>       | otherwise = findP z xs

Functions to split the Props

combine takes a list of Props and a list of Prop lists and adds all the values in the
single list of Props to all the lists in the list of Prop lists

>   combine :: [Prop] -> [[Prop]] -> [[Prop]]
>   combine ps pls = [ps ++ pl | pl<-pls ]

For each of the semantic tableaux rules there have been three functions created,
a split, a remove and a solve function

The split functions take a list of Props and splits the first occurence of the
relative rule into its simpler form by combing the result of the remove function
and the result of the solve function

The remove function scans the list of Props and removes the first occurence of
the relative rule from the list and returns the list

The solve function finds the first occurence of the relative rule in the list, solves it
according to the relative rule and returns only the simpler form

As there are different rules for Not Not, And, Or, Implies, Iff, Not And, Not Or, Not Implies
and Not Iff there are three functions for each

>   splitNotNot :: [Prop] -> [[Prop]]
>   splitNotNot ps = combine (removeNotNot ps) (solveNotNot ps)

>   removeNotNot :: [Prop] -> [Prop]
>   removeNotNot [] = []
>   removeNotNot ((NOT (NOT _)):ps) = ps
>   removeNotNot (p:ps) = p : removeNotNot ps

>   solveNotNot :: [Prop] -> [[Prop]]
>   solveNotNot [] = [[]]
>   solveNotNot ((NOT (NOT p)):_) = [[p]]
>   solveNotNot (_:ps) = solveNotNot ps

>   splitAnd :: [Prop] -> [[Prop]]
>   splitAnd ps = combine (removeAnd ps) (solveAnd ps)

>   removeAnd :: [Prop] -> [Prop]
>   removeAnd [] = []
>   removeAnd ((AND p q):ps) = ps
>   removeAnd (p:ps) = p : removeAnd ps

>   solveAnd :: [Prop] -> [[Prop]]
>   solveAnd [] = [[]]
>   solveAnd ((AND p q):_) = [[p,q]]
>   solveAnd (_:ps) = solveAnd ps

>   splitOr :: [Prop] -> [[Prop]]
>   splitOr ps = combine (removeOr ps) (solveOr ps)

>   removeOr :: [Prop] -> [Prop]
>   removeOr [] = []
>   removeOr ((OR p q):ps) = ps
>   removeOr (p:ps) = p : removeOr ps

>   solveOr :: [Prop] -> [[Prop]]
>   solveOr [] = [[]]
>   solveOr ((OR p q):_) = [[p],[q]]
>   solveOr (_:ps) = solveOr ps

>   splitImplies :: [Prop] -> [[Prop]]
>   splitImplies ps = combine (removeImplies ps) (solveImplies ps)

>   removeImplies :: [Prop] -> [Prop]
>   removeImplies [] = []
>   removeImplies ((IMPLIES p q):ps) = ps
>   removeImplies (p:ps) = p : removeImplies ps

>   solveImplies :: [Prop] -> [[Prop]]
>   solveImplies [] = [[]]
>   solveImplies ((IMPLIES p q):_) = [[NOT p],[q]]
>   solveImplies (_:ps) = solveImplies ps

>   splitIff :: [Prop] -> [[Prop]]
>   splitIff ps = combine (removeIff ps) (solveIff ps)

>   removeIff :: [Prop] -> [Prop]
>   removeIff [] = []
>   removeIff ((IFF p q):ps) = ps
>   removeIff (p:ps) = p : removeIff ps

>   solveIff :: [Prop] -> [[Prop]]
>   solveIff [] = [[]]
>   solveIff ((IFF p q):_) = [[p,q],[NOT p,NOT q]]
>   solveIff (_:ps) = solveIff ps

>   splitNotAnd :: [Prop] -> [[Prop]]
>   splitNotAnd ps = combine (removeNotAnd ps) (solveNotAnd ps)

>   removeNotAnd :: [Prop] -> [Prop]
>   removeNotAnd [] = []
>   removeNotAnd ((NOT (AND p q)):ps) = ps
>   removeNotAnd (p:ps) = p : removeNotAnd ps

>   solveNotAnd :: [Prop] -> [[Prop]]
>   solveNotAnd [] = [[]]
>   solveNotAnd ((NOT (AND p q)):_) = [[NOT p],[NOT q]]
>   solveNotAnd (_:ps) = solveNotAnd ps

>   splitNotOr :: [Prop] -> [[Prop]]
>   splitNotOr ps = combine (removeNotOr ps) (solveNotOr ps)

>   removeNotOr :: [Prop] -> [Prop]
>   removeNotOr [] = []
>   removeNotOr ((NOT (OR p q)):ps) = ps
>   removeNotOr (p:ps) = p : removeNotOr ps

>   solveNotOr :: [Prop] -> [[Prop]]
>   solveNotOr [] = [[]]
>   solveNotOr ((NOT (OR p q)):_) = [[NOT p,NOT q]]
>   solveNotOr (_:ps) = solveNotOr ps

>   splitNotImplies :: [Prop] -> [[Prop]]
>   splitNotImplies ps = combine (removeNotImplies ps) (solveNotImplies ps)

>   removeNotImplies :: [Prop] -> [Prop]
>   removeNotImplies [] = []
>   removeNotImplies ((NOT (IMPLIES p q)):ps) = ps
>   removeNotImplies (p:ps) = p : removeNotImplies ps

>   solveNotImplies :: [Prop] -> [[Prop]]
>   solveNotImplies [] = [[]]
>   solveNotImplies ((NOT (IMPLIES p q)):_) = [[p,NOT q]]
>   solveNotImplies (_:ps) = solveNotImplies ps

>   splitNotIff :: [Prop] -> [[Prop]]
>   splitNotIff ps = combine (removeNotIff ps) (solveNotIff ps)

>   removeNotIff :: [Prop] -> [Prop]
>   removeNotIff [] = []
>   removeNotIff ((NOT (IFF p q)):ps) = ps
>   removeNotIff (p:ps) = p : removeNotIff ps

>   solveNotIff :: [Prop] -> [[Prop]]
>   solveNotIff [] = [[]]
>   solveNotIff ((NOT (IFF p q)):_) = [[p,NOT q],[NOT p,q]]
>   solveNotIff (_:ps) = solveNotIff ps

The overall split function selects which split function to call dependent on the
integer passed to it

>   split :: Int -> [Prop] -> [[Prop]]
>   split 1 pl = splitNotNot pl
>   split 2 pl = splitAnd pl
>   split 3 pl = splitNotOr pl
>   split 4 pl = splitNotImplies pl
>   split 5 pl = splitOr pl
>   split 6 pl = splitImplies pl
>   split 7 pl = splitNotAnd pl
>   split 8 pl = splitIff pl
>   split 9 pl = splitNotIff pl
>   split x pl = [pl]

reduced takes a list of Props and checks it for all the rules to see if it is
reduced to it's simplest form. If it is the function returns True, if not then
the function returns False

>   reduced :: [Prop] -> Bool
>   reduced [] = True
>   reduced ((NOT (NOT p)):_) = False
>   reduced ((AND p q):_) = False
>   reduced ((OR p q):_) = False
>   reduced ((IMPLIES p q):_) = False
>   reduced ((IFF p q):_) = False
>   reduced ((NOT (AND p q)):_) = False
>   reduced ((NOT (OR p q)):_) = False
>   reduced ((NOT (IMPLIES p q)):_) = False
>   reduced ((NOT (IFF p q)):_) = False
>   reduced (_:pl) = reduced pl

reduceable scans a list of Props for the existance of a specific rule indicated by the
integer value passed to it. If the rule exists the function returns an integer representing
the rule, if the rule doesn't exist then the value 10 is returned

>   reduceable :: Int -> [Prop] -> Int
>   reduceable x [] = 10
>   reduceable 1 ((NOT (NOT p)):_) = 1
>   reduceable 2 ((AND p q):_) = 2
>   reduceable 3 ((NOT (OR p q)):_) = 3
>   reduceable 4 ((NOT (IMPLIES p q)):_) = 4
>   reduceable 5 ((OR p q):_) = 5
>   reduceable 6 ((IMPLIES p q):_) = 6
>   reduceable 7 ((NOT (AND p q)):_) = 7
>   reduceable 8 ((IFF p q):_) = 8
>   reduceable 9 ((NOT (IFF p q)):_) = 9
>   reduceable x (p:pl) = reduceable x pl

reduceAll calls reduceable once for every rule, and returns the lowest integer returned
which represents the prefered rule to reduce next

>   reduceAll :: Int -> [Prop] -> Int
>   reduceAll 10 _ = 10
>   reduceAll x pl = min (reduceable x pl) (reduceAll (x+1) pl)

reduceRoot takes each Prop list in a list of Prop lists and checks to see if it is reduced,
if the Prop list is reduced the the list is returned with the result of reduceRoot on the rest
of the list. If the Prop list is not reduced though the list is reduced and checked for
contradictions, which are removed, and then passed into reduceRoot again. This has the affect
of recursively looping until the first Prop and any branches that may be produced from spliting
are delt with. Then the function returns the simplest form and processes the rest of the list
with reduceRoot

>   reduceRoot :: [[Prop]] -> [[Prop]]
>   reduceRoot [] = [[]]
>   reduceRoot [[]] = [[]]
>   reduceRoot (pl:pls) = (if (reduced pl) then [pl] else (reduceRoot (removeConts (reduce pl)))) ++ (reduceRoot pls)

reduce checks to see which rule needs to be split next and then calls the split function with
this information

>   reduce :: [Prop] -> [[Prop]]
>   reduce pl = split (reduceAll 1 pl) pl

Remove contradictions

Function to remove a list if it contains a contradiction.

>   removeConts :: [[Prop]] -> [[Prop]]
>   removeConts x = looseEmptyLists (removeConts1 x)

Recurse through the list of lists, picking out 1 prop list at
a time and pass it to 'foo'

>   removeConts1 :: [[Prop]] -> [[Prop]]
>   removeConts1 [] = []
>   removeConts1 (x:xs) = (foo x):(removeConts1 xs)

Check the list of Props with 'bar'. If the list contains
a contradiction, the value returned by 'bar' will be False
so loose that list (return []).

>   foo :: [Prop] -> [Prop]
>   foo x
>       | bar x = x
>       | otherwise = []

'bar' and comp recurse through the list comparing each prop
with every other one using 'contra'

>   bar :: [Prop] -> Bool
>   bar [] = True
>   bar (p:pl) = (comp p pl) && (bar pl)

>   comp :: Prop -> [Prop] -> Bool
>   comp p pl  = and [contra p pl2 | pl2 <- pl]

Return False if the 2 arguments are contradictions of eachother.

>   contra :: Prop -> Prop -> Bool
>   contra a b = not (((NOT a) == b) || (a == (NOT b)))

Tidy the resulting list of lists by removing all the empty lists.

>   looseEmptyLists :: [[Prop]] -> [[Prop]]
>   looseEmptyLists [] = []
>   looseEmptyLists [[]] = []
>   looseEmptyLists ([]:xs) = looseEmptyLists xs
>   looseEmptyLists (x:[]) = [x]
>   looseEmptyLists (x:xs) = [x] ++ (looseEmptyLists xs)

Some example Props

>   plist1, plist2, plist3, plist4 :: [[Prop]]
>   plist1 = [[VAR 'a', (NOT (NOT (VAR 'c'))), VAR 'b']]
>   plist2 = [[VAR 'a', (AND (VAR 'b') (VAR 'c')), (OR (VAR 'b') (VAR 'c'))]]
>   plist3 = [[(IMPLIES (VAR 'a') (VAR 'b')), (IFF (VAR 'c') (VAR 'a')), (NOT (AND (VAR 'a') (VAR 'b')))]]
>   plist4 = [[(NOT (OR (VAR 'a') (VAR 'b'))), (NOT (IMPLIES (VAR 'c') (VAR 'd'))), (NOT (IFF (VAR 'a') (VAR 'b')))]]

The questions converted into Prop form

>   q1, q2, q3, q4 :: [[Prop]]
>   q1 = [[(IFF (NOT (OR (VAR 'a') (VAR 'b'))) (NOT (AND (NOT (VAR 'a')) (NOT (VAR 'b')))))]]
>   q2 = [[(NOT (IFF (OR (VAR 'a') (VAR 'b')) (NOT (AND (NOT (VAR 'a')) (NOT (VAR 'b'))))))]]
>   q3 = [[(NOT (IMPLIES (IMPLIES (IMPLIES (VAR 'c') (VAR 'b')) (VAR 'c')) (VAR 'c')))]]
>   q4 = [[(IMPLIES (IMPLIES (VAR 'a') (VAR 'b')) (IMPLIES (VAR 'b') (VAR 'a')))]]

>   b1, b2, b3, b4, b5, b6, b7, b8, b9 :: Prop
>   b1 = (IFF (VAR 'f') (NOT (VAR 'c')))
>   b2 = (IFF (VAR 'g') (NOT (VAR 'c')))
>   b3 = (IFF (VAR 'h') (VAR 'd'))
>   b4 = (OR (OR (VAR 'b') (VAR 'c')) (VAR 'd'))
>   b5 = (NOT (AND (VAR 'b') (VAR 'c')))
>   b6 = (NOT (AND (VAR 'c') (VAR 'd')))
>   b7 = (NOT (AND (VAR 'd') (VAR 'b')))
>   b8 = (OR (OR (VAR 'f') (VAR 'g')) (VAR 'h'))
>   b9 = (OR (OR (NOT (VAR 'f')) (NOT (VAR 'g'))) (NOT (VAR 'h')))

box and box1 are virtualy identical, except that they AND the values in a slightly 
different way.  (box1 was only created to work out if another function was working
correctly or not).

>   box, box1 :: [[Prop]]
>   box = [[(AND (AND (AND (b1) (b2)) (AND (b3) (b4))) (AND (AND (b5) (b6)) (AND (b7) (AND (b8) (b9)))))]]
>   box1 = [[(AND (AND (AND (AND (b1) (b2)) (AND (b3) (b4))) (AND (AND (b5) (b6)) (AND (b7) (b8)))) (b9))]]