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.
On 7 August 2010 18:14, dan portin
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.
Hi Dan One would need a detailed knowledge of tableau-style theorem provers to answer that... In the code above Tableau is the same type after rewriting. If that's the case, maybe you don't need a state monad solution. However, if you are labelling something with /w/ which looks like an integer from your explanation, then first you want to make a variation of the Tableau datatype that holds the label, thus rewrite would be a type changing function: rewrite :: Tableau -> Tableau' Where Tableau' is an alternative definition of Tableau that includes a field for /w/ (possibly in the auxiliary types Status or Expr, which would likewise need an alternative definition). If this is what you want to do, you should be able to thread "number supply" through the rewrite and rule functions fairly simply with a state monad. rewrite :: Tableau -> State Int Tableau' Best wishes Stephen
Hi Stephen, thanks for your reply: In the code above Tableau is the same type after rewriting. If that's
the case, maybe you don't need a state monad solution. However, if you are labelling something with /w/ which looks like an integer from your explanation, then first you want to make a variation of the Tableau datatype that holds the label, thus rewrite would be a type changing function:
rewrite :: Tableau -> Tableau'
I think the basic tableau data type would look like: data Tableau = Node (World, Expr) [Tableau] type World = Int and the rewrite function would need to track the current position of rewrite in the tableau and store a complete tableau (or some kind of record, possibly in a zipper) in order to move around, depending on the instruction it's given. So I would need something like: rewrite :: Tableau -> State (Record, Tableau) So that it could be passed an instruction such as: (Poss, [ex]) -> (a) inject ex into Tableau; (b) Store Tableau in Record; (c) move to correct spot in Record; (d) restart rewriting from position in Record. Even though Haskell's my first language, I still want a function that says: store current Tableau in *r, then get r* and restart.
If this is what you want to do, you should be able to thread "number supply" through the rewrite and rule functions fairly simply with a state monad.
rewrite :: Tableau -> State Int Tableau'
I think this means that when implementing the monad, I should define (>>=) as a general rule similar to the set of instructions above, e.g,. if f is a function that injects the list ex into a tree structure, and g is a rewrite function, then
= should have a structure abstracted from the following:
f >>= g = do f ~> State Record Tableau store Tableau in Record do g at Record make Record into current Tableau This seems similar to the "threading" method that, for instance, Wadler uses in the first sections of his paper on functional programming and monads, when building an evaluator that keeps track of division operations. Thanks or the response. If you see any glaring 'monadic errors,' I'd be happy to hear about them, but your advice was helpful :)
participants (2)
-
dan portin -
Stephen Tetley