-- Theorem prover (section 2.6) - incorrect version module TheoremProver1 where import QuickCheck import List import Monad newtype Name = Name String deriving (Eq, Show) data Form = Var Name | Form :& Form | Not Form deriving (Eq, Show) names :: Form -> [Name] names (Var v) = [v] names (p :& q) = names p `union` names q names (Not p) = names p data Valuation = Val { falses :: [Name], trues :: [Name] } deriving (Eq, Show) nothing :: Valuation nothing = Val { falses = [], trues = [] } tableau :: Form -> Valuation -> [Valuation] tableau (Var v) val | v `elem` trues val = [val] | v `elem` falses val = [] | otherwise = [val {trues = v:trues val}] tableau (Not (Var v)) val | v `elem` trues val = [] | v `elem` falses val = [val] | otherwise = [val {falses = v:falses val}] tableau (p :& q) val = [valpq | valp <- tableau p val, valpq <- tableau q valp] tableau (Not (p :& q)) val = tableau (Not p) val ++ tableau (Not q) val models :: Form -> [Valuation] models p = tableau p nothing instance Arbitrary Name where arbitrary = sized \$ \n -> do c <- elements (take (n+1) ['a'..'z']) return (Name [c]) valuationOver :: [Name] -> Gen Valuation valuationOver ns = do bs <- vector (length ns) return (Val { falses = [ n | (n,False) <- ns `zip` bs ], trues = [ n | (n,True ) <- ns `zip` bs ] }) -- A not-very-intelligent answer to Exercise 2.6 - try to improve it instance Arbitrary Form where arbitrary = sized arbForm arbForm 0 = liftM Var arbitrary arbForm n | n > 0 = frequency [(1,liftM Var arbitrary), (2,liftM2 (:&) subForm subForm), (2,liftM Not subForm)] where subForm = arbForm (n `div` 2) -- Note that there's an error in the definition on page 35 - it talks about -- "trues v" and "falses v". (|=) :: Valuation -> Form -> Bool val |= Var v | v `elem` trues val = True | v `elem` falses val = False | otherwise = error "undefined variable" val |= (p :& q) = (val |= p) && (val |= q) val |= Not p = not (val |= p) prop_Sound :: Form -> Bool prop_Sound p = all (\val -> val |= p) (models p)