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 &quot;Status&quot; and &quot;check&quot; functions are unnecessary, but I added them anyways, because some (other) tableau proof systems will require them.<br>
<br><span style="font-family: courier new,monospace;">data Tableau = Node Status Expr [Tableau]</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;"> deriving Eq</span><br style="font-family: courier new,monospace;">
<br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">data Status = C | I</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;"> deriving (Show, Eq)</span><br style="font-family: courier new,monospace;">
<br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">-- Rules for propositional tableau. Rules are of the form (s, ex), where</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;">-- the value of s (Action) indicates the appropriate action (extend or branch)</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">-- for the tableau rewritign function to take when injecting the formulas in</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;">-- the list ex.</span><br style="font-family: courier new,monospace;"><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">rule :: Expr -&gt; (Action, [Expr])</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;">rule (Var x)            = (None, [Var x])</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">rule (Not (Var x))      = (None, [Not (Var x)])</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;">rule (Not (Not e))      = (Extend, [e])</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">rule (Impl e1 e2)       = (Branch, [Not e1, e2])</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;">rule (Not (Impl e1 e2)) = (Extend, [e1, Not e2])</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">rule (Conj e1 e2)       = (Extend, [e1, e2])</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;">rule (Not (Conj e1 e2)) = (Branch, [Not e1, Not e2])</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">rule (Disj e1 e2)       = (Branch, [e1, e2])</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;">rule (Not (Disj e1 e2)) = (Extend, [Not e1, Not e2])</span><br style="font-family: courier new,monospace;"><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">-- &#39;rewrite&#39; constructs a complete tableau from a given tableau by applying the</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;">-- appropriate tableau rule at each incomplete node, then appropriately</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">-- injecting the resultant expressions into the tableau. &#39;rewrite&#39; recurses over</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;">-- the tableau until all nodes are complete. &#39;consTableau&#39; constructs a </span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">-- complete tableau from an expression.</span><br style="font-family: courier new,monospace;">
<br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">consTableau :: Expr -&gt; Tableau</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">consTableau e = rewrite $ Node I e []</span><br style="font-family: courier new,monospace;">
<br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">rewrite :: Tableau -&gt; Tableau</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">rewrite t = case (isComplete t) of</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;">            True  -&gt; moveAnd rewrite t</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">            False -&gt; case (rule $ getExpr t) of</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;">                     (None, _)    -&gt; check $ moveAnd rewrite t</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">                     (Extend, ex) -&gt; rewrite (check $ inject Extend ex t)</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;">                     (Branch, ex) -&gt; rewrite (check $ inject Branch ex t)</span><br style="font-family: courier new,monospace;"><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;">inject :: Action -&gt; [Expr] -&gt; Tableau -&gt; Tableau</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">inject a ex (Node s expr []) = case a of</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;">   Extend -&gt; Node s expr [foldr (\e y -&gt; Node I e [y]) (Node I (last ex) []) (init ex)]</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;">   Branch -&gt; Node s expr $ map (\e -&gt; Node I e []) ex          </span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;">inject a ex (Node s expr es) = Node s expr $ map (\b -&gt; inject a ex b) es</span><br><br><font face="arial,helvetica,sans-serif">The most common rule for modal tableaux is:<br>
<br></font><div style="margin-left: 40px;"><font face="arial,helvetica,sans-serif">For a formula (</font>◊P, <i>w</i>), increment <i>w</i> by some number <i>n </i>to yield the relation (<i>w</i>, <i>w</i> + <i>n</i>), then extending the tableau with a formula (P, <i>w + n</i>) for each formula (◻P, <i>w</i>) on the current path. <br>
</div><br>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 <i>rewrite</i> 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).<br>
<br>I&#39;m trying to learn Haskell, however, so I&#39;d like to learn more about monads. I understand the simple examples of monads generally given in tutorials (like Wadler&#39;s paper, which I&#39;m working through), but I&#39;m not sure what the <b>general structure</b> of what I&#39;m looking for would look like (that is a problem). So my question, finally, is: <i>what would be the general structure of the implementation of the state monad for a tableau-style theorem prover</i> <i>look like, schematically</i>. I can&#39;t really square my goal with example implementations of the state monad, where the state is threaded through in a series of let expressions.<br>
<br>Thanks, and sorry for the long post.<br><br>