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.
