New subject: Data structure for Propositional Logic formulas

12 Oct 2011

      Hi,

I wrote this program to work with formulas in propositional logic:

data Formula =
               | Variable Char
               | Not Formula | And Formula Formula | Or Formula Formula
               | Imply Formula Formula | Equivalent Formula Formula
               deriving (Eq)

instance Show Formula where
    show (Variable v) = [v]
    show (Not f)      = "~" ++ show f
    show (And f g)    = "(" ++ show f ++ " & " ++ show g ++ ")"
    show (Or f g)     = "(" ++ show f ++ " v " ++ show g ++ ")"
    show (Imply f g ) = "(" ++ show f ++ " -> " ++ show g ++ ")"
    show (Equivalent f g ) = "(" ++ show f ++ " <-> " ++ show g ++ ")"

To make a formula you can do something like:

ghci> let f = Or (Variable 'C') (And (Variable 'A') (Not (Variable 'C')))
ghci> f
(C v (A & ~C))

So, my questions are:

1. Do you think this is an elegant solution or would you define custom 
operators (or, and, ->, <->) instead? Or something completely different?
2. If I pack this code into a module how would add a new logic 
connective like xor or nand to Formula? Meaning, can I add another type 
constructor to it?
3. Is there a way to "nest" data definitions, e.g. I would like to 
replace the 'Variable Char' type constructor by 'Literal Char', whereas 
a Literal is either a Variable or a negated Variable. Literals can be 
negated, too.

Thanks a lot.
Alex

Data structure for Propositional Logic formulas

Alexander Raasch

Daniel Schoepe

Daniel Schoepe

Benedict Eastaugh

Christian Maeder

Benedict Eastaugh

Christian Maeder

Rustom Mody

tags

participants (5)