0

I've been trying to write a program to check whether a propositional logic formula is valid or not by representing it as a tree and then recursively negating the root node and all subtrees appropriately to look for contradictions, and I reached a point where I don't know how to proceed or if I should just rewrite everything.

This is how I'm representing the tree, SBranch is only used for the NOT operator.

data Tree = Leaf {op :: String, eval :: Bool} | DBranch {op :: String, eval :: Bool, left :: Tree, right :: Tree} | SBranch {op :: String, eval :: Bool, left :: Tree} deriving Show

I have a function that takes a String in prefix notation and turns it into a tree using the above data type. Then, I have two functions, one that negates a subtreee and another that validates it (not sure if these are the appropriate words, english is not my first language).

vTree :: Tree -> Tree
vTree tree
    | opr == "^" = tree{eval = True, left = vTree $ left tree, right = vTree $ right tree} -- RULE 3
    | opr == "v" = tree{eval = True} -- TODO -- RULE 5
    | opr == "->" = tree{eval = True} -- TODO -- RULE 1
    | opr == "~" = tree{eval = True, left = fTree $ left tree} -- RULE 7
    | otherwise = tree{eval = True}
    where opr = op(tree)

fTree :: Tree -> Tree
fTree tree
    | opr == "^" = tree{eval = False } -- TODO -- RULE 4
    | opr == "v" = tree{eval = False, left = fTree $ left tree, right = fTree $ right tree} -- RULE 6
    | opr == "->" = tree{eval = False, left = vTree $ left tree , right = fTree $ right tree } -- RULE 2
    | opr == "~" = tree{eval = False, left = vTree $ left tree} -- RULE 8
    | otherwise = tree{eval = False}
    where opr = op(tree)

The guards marked with TODO are the ones where I don't know what to write, for example, for an AND to be false, either the left side can be false or the right side can be false, so if I only make a recursive call to build a tree based on only one of these alternatives, my proof is not going to be correct. This is the idea I had in mind that I don't know how to and I'm not sure whether I can even use this in Haskell (I'm still trying to learn it). How I imagined I could solve this problem So, does anyone know how I could write this or an alternative way if this is not possible or unecessarily difficult?

Matheus
  • 1
  • 1
  • You might consider writing a function like `negateTree :: Tree -> Tree` that negates ever `eval` in the tree (much like you describe what you want to do in your opening sentence), and then see if you can use that to merge `vTree` and `fTree` into a single function. With that done, consider that your `^` case for `vTree` already doesn't make sense: what if one of the child trees is False? You'll need to actually check the truth values of the recursive calls to determine the truth value of the parent. – DDub Nov 20 '22 at 16:38

0 Answers0