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.<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 -> (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;">-- 'rewrite' 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. 'rewrite' recurses over</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;">-- the tableau until all nodes are complete. 'consTableau' 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 -> 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 -> 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 -> moveAnd rewrite t</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;"> False -> case (rule $ getExpr t) of</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;"> (None, _) -> check $ moveAnd rewrite t</span><br style="font-family: courier new,monospace;"><span style="font-family: courier new,monospace;"> (Extend, ex) -> rewrite (check $ inject Extend ex t)</span><br style="font-family: courier new,monospace;">
<span style="font-family: courier new,monospace;"> (Branch, ex) -> 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 -> [Expr] -> Tableau -> 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 -> Node s expr [foldr (\e y -> 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 -> Node s expr $ map (\e -> 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 -> 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'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 <b>general structure</b> of what I'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'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>