> 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))]]