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.