-- v1: name types: Tableau and Branch -- v2: change names of functions etc. -- - ensures that the names are appropriate, as well as -- - fitting in with newly named types -- v3: change to non-literate form -- v4: some algorithmic changes: introducing HOFs etc. this is v4-1, -- had to backtrack to accommodate mistake in introducing list -- comprehesions. 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 ++ ")" -- Addition in v1: type Branch = [Prop] type Tableau = [Branch] -- The next 3 functions are the ones that control the output to the screen of the tableau. -- This function is the main function you use when you want to find the result. The syntax -- is "Main> tableauMain [prop]" (ie "tableauMain box" will give you the tableaux result for -- the box problem). tableauMain :: Tableau -> IO () tableauMain x = putStr (displayAllBranches (buildTableau x)) -- This function displays one branch of the tableau results, it puts every variable on a -- new line to make it easy to look at and understand. displayBranch :: Branch -> String displayBranch = concat . map (++"\n") . map show -- This function displays all the branches of the tableau, by calling the above function. -- It then seperates each branch with a space, to make the final output clear. displayAllBranches :: Tableau -> String displayAllBranches = concat . intersperse "\n" . map displayBranch -- This function is the main function that brings all the seperate parts of calculating a -- tableaux together. buildTableau :: Tableau -> Tableau buildTableau = removeDuplicateBranches . removeDuplicatesInBranches . removeConts . reduceRoot -- 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. removeDuplicateBranches :: Tableau -> Tableau removeDuplicateBranches [] = [] removeDuplicateBranches (x:xs) | x == findBranch x xs = [] ++ removeDuplicateBranches xs | otherwise = [x] ++ removeDuplicateBranches xs -- This function works in conjunction with the above function to find and remove any -- duplicate braches: if a branch is present in a Tableau, the Branch is returned; -- otherwise an empty Branch is returned. findBranch :: Branch -> Tableau -> Branch 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. removeDuplicatesInBranches :: Tableau -> Tableau removeDuplicatesInBranches [] = [] removeDuplicatesInBranches (x:xs) = [removeDuplicateProps x] ++ removeDuplicatesInBranches 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. removeDuplicateProps :: Branch -> Branch removeDuplicateProps [] = [] removeDuplicateProps (x:xs) | x == findProp x xs = [] ++ removeDuplicateProps xs | otherwise = [x] ++ removeDuplicateProps xs -- This function works in conjunction with the above two functions to find and remove -- any duplicate Propositions in a single branch. findProp :: Prop -> Branch -> Prop findProp z [] = FALSE findProp z (x:xs) | z == x = x | otherwise = findProp 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 :: Branch -> Tableau -> Tableau combine ps pls = [ps ++ pl | pl<-pls ] -- For each of the semantic tableau 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 :: Branch -> Tableau splitNotNot ps = combine (removeNotNot ps) (solveNotNot ps) removeNotNot :: Branch -> Branch removeNotNot [] = [] removeNotNot ((NOT (NOT _)):ps) = ps removeNotNot (p:ps) = p : removeNotNot ps solveNotNot :: Branch -> Tableau solveNotNot [] = [[]] solveNotNot ((NOT (NOT p)):_) = [[p]] solveNotNot (_:ps) = solveNotNot ps splitAnd :: Branch -> Tableau splitAnd ps = combine (removeAnd ps) (solveAnd ps) removeAnd :: Branch -> Branch removeAnd [] = [] removeAnd ((AND p q):ps) = ps removeAnd (p:ps) = p : removeAnd ps solveAnd :: Branch -> Tableau solveAnd [] = [[]] solveAnd ((AND p q):_) = [[p,q]] solveAnd (_:ps) = solveAnd ps splitOr :: Branch -> Tableau splitOr ps = combine (removeOr ps) (solveOr ps) removeOr :: Branch -> Branch removeOr [] = [] removeOr ((OR p q):ps) = ps removeOr (p:ps) = p : removeOr ps solveOr :: Branch -> Tableau solveOr [] = [[]] solveOr ((OR p q):_) = [[p],[q]] solveOr (_:ps) = solveOr ps splitImplies :: Branch -> Tableau splitImplies ps = combine (removeImplies ps) (solveImplies ps) removeImplies :: Branch -> Branch removeImplies [] = [] removeImplies ((IMPLIES p q):ps) = ps removeImplies (p:ps) = p : removeImplies ps solveImplies :: Branch -> Tableau solveImplies [] = [[]] solveImplies ((IMPLIES p q):_) = [[NOT p],[q]] solveImplies (_:ps) = solveImplies ps splitIff :: Branch -> Tableau splitIff ps = combine (removeIff ps) (solveIff ps) removeIff :: Branch -> Branch removeIff [] = [] removeIff ((IFF p q):ps) = ps removeIff (p:ps) = p : removeIff ps solveIff :: Branch -> Tableau solveIff [] = [[]] solveIff ((IFF p q):_) = [[p,q],[NOT p,NOT q]] solveIff (_:ps) = solveIff ps splitNotAnd :: Branch -> Tableau splitNotAnd ps = combine (removeNotAnd ps) (solveNotAnd ps) removeNotAnd :: Branch -> Branch removeNotAnd [] = [] removeNotAnd ((NOT (AND p q)):ps) = ps removeNotAnd (p:ps) = p : removeNotAnd ps solveNotAnd :: Branch -> Tableau solveNotAnd [] = [[]] solveNotAnd ((NOT (AND p q)):_) = [[NOT p],[NOT q]] solveNotAnd (_:ps) = solveNotAnd ps splitNotOr :: Branch -> Tableau splitNotOr ps = combine (removeNotOr ps) (solveNotOr ps) removeNotOr :: Branch -> Branch removeNotOr [] = [] removeNotOr ((NOT (OR p q)):ps) = ps removeNotOr (p:ps) = p : removeNotOr ps solveNotOr :: Branch -> Tableau solveNotOr [] = [[]] solveNotOr ((NOT (OR p q)):_) = [[NOT p,NOT q]] solveNotOr (_:ps) = solveNotOr ps splitNotImplies :: Branch -> Tableau splitNotImplies ps = combine (removeNotImplies ps) (solveNotImplies ps) removeNotImplies :: Branch -> Branch removeNotImplies [] = [] removeNotImplies ((NOT (IMPLIES p q)):ps) = ps removeNotImplies (p:ps) = p : removeNotImplies ps solveNotImplies :: Branch -> Tableau solveNotImplies [] = [[]] solveNotImplies ((NOT (IMPLIES p q)):_) = [[p,NOT q]] solveNotImplies (_:ps) = solveNotImplies ps splitNotIff :: Branch -> Tableau splitNotIff ps = combine (removeNotIff ps) (solveNotIff ps) removeNotIff :: Branch -> Branch removeNotIff [] = [] removeNotIff ((NOT (IFF p q)):ps) = ps removeNotIff (p:ps) = p : removeNotIff ps solveNotIff :: Branch -> Tableau 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 -> Branch -> Tableau 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 :: Branch -> 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 -> Branch -> 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 -> Branch -> 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 :: Tableau -> Tableau 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 :: Branch -> Tableau reduce pl = split (reduceAll 1 pl) pl -- Remove contradictions -- Function to remove a list if it contains a contradiction. removeConts :: Tableau -> Tableau 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 :: Tableau -> Tableau 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 :: Branch -> Branch foo x | bar x = x | otherwise = [] -- 'bar' and comp recurse through the list comparing each prop -- with every other one using 'contra' bar :: Branch -> Bool bar [] = True bar (p:pl) = (comp p pl) && (bar pl) comp :: Prop -> Branch -> 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 :: Tableau -> Tableau looseEmptyLists [] = [] looseEmptyLists [[]] = [] looseEmptyLists ([]:xs) = looseEmptyLists xs looseEmptyLists (x:[]) = [x] looseEmptyLists (x:xs) = [x] ++ (looseEmptyLists xs) -- Some example Props plist1, plist2, plist3, plist4 :: Tableau 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 :: Tableau 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 :: Tableau 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))]] -- The box example as a test. test = tableauMain box