I wrote a simple tableau theorem prover for propositional logic as my first Haskell program. My next goal is to write a theorem prover for modal logic. Fortunately, this is more complicated. In essence, I have a tableau data type, a rules function, and a rewrite function, which generate a tableau, surrounded by auxiliary functions to collapse the tableau into paths and extract interpretations. The tableau rewrite function is below. The "Status" and "check" functions are unnecessary, but I added them anyways, because some (other) tableau proof systems will require them. data Tableau = Node Status Expr [Tableau] deriving Eq data Status = C | I deriving (Show, Eq) -- Rules for propositional tableau. Rules are of the form (s, ex), where -- the value of s (Action) indicates the appropriate action (extend or branch) -- for the tableau rewritign function to take when injecting the formulas in -- the list ex. rule :: Expr -> (Action, [Expr]) rule (Var x) = (None, [Var x]) rule (Not (Var x)) = (None, [Not (Var x)]) rule (Not (Not e)) = (Extend, [e]) rule (Impl e1 e2) = (Branch, [Not e1, e2]) rule (Not (Impl e1 e2)) = (Extend, [e1, Not e2]) rule (Conj e1 e2) = (Extend, [e1, e2]) rule (Not (Conj e1 e2)) = (Branch, [Not e1, Not e2]) rule (Disj e1 e2) = (Branch, [e1, e2]) rule (Not (Disj e1 e2)) = (Extend, [Not e1, Not e2]) -- 'rewrite' constructs a complete tableau from a given tableau by applying the -- appropriate tableau rule at each incomplete node, then appropriately -- injecting the resultant expressions into the tableau. 'rewrite' recurses over -- the tableau until all nodes are complete. 'consTableau' constructs a -- complete tableau from an expression. consTableau :: Expr -> Tableau consTableau e = rewrite $ Node I e [] rewrite :: Tableau -> Tableau rewrite t = case (isComplete t) of True -> moveAnd rewrite t False -> case (rule $ getExpr t) of (None, _) -> check $ moveAnd rewrite t (Extend, ex) -> rewrite (check $ inject Extend ex t) (Branch, ex) -> rewrite (check $ inject Branch ex t) inject :: Action -> [Expr] -> Tableau -> Tableau inject a ex (Node s expr []) = case a of Extend -> Node s expr [foldr (\e y -> Node I e [y]) (Node I (last ex) []) (init ex)] Branch -> Node s expr $ map (\e -> Node I e []) ex inject a ex (Node s expr es) = Node s expr $ map (\b -> inject a ex b) es The most common rule for modal tableaux is: For a formula (◊P, *w*), increment *w* by some number *n *to yield the relation (*w*, *w* + *n*), then extending the tableau with a formula (P, *w + n*) for each formula (◻P, *w*) on the current path. In order to implement the rule, I would need to: (a) save the state of the tableau after each rewrite rule is applied; (b) if a rewrite rule for ◊ is applied, index the resultant relation and rewrite every formula ◻P on the current path; (3) check for infinite loops using a fairly simple algorithm. I see two ways this could be accomplished: (1) Implement the tableau rewriting using the state monad; (2) use a function like *rewrite* which saves the state of the tableau in an argument (so that after each rewrite, the state of the tableau is stored, and I can restart the recursion at that point). I'm trying to learn Haskell, however, so I'd like to learn more about monads. I understand the simple examples of monads generally given in tutorials (like Wadler's paper, which I'm working through), but I'm not sure what the *general structure* of what I'm looking for would look like (that is a problem). So my question, finally, is: *what would be the general structure of the implementation of the state monad for a tableau-style theorem prover* *look like, schematically*. I can't really square my goal with example implementations of the state monad, where the state is threaded through in a series of let expressions. Thanks, and sorry for the long post.