Labelled Tableaux

Moving

2007-02-03T01:46:00.000+11:00

This blog is defunct. It's content, along with that of my other blogs, is now hosted at thomas-sutton.id.au.

Writing and Ownership

2005-11-04T09:35:00.000+11:00

My thesis was due last Friday (delayed to last Monady) and I have an extension (or, rather, an I-don't-have-it-done) until today. Unfortunately, it doesn't look like I'll have it done by my deadline today either. For some reason, I just haven't wanted, or been able to, write.

I think that this is due, in part, to the fact that this is my own project (rather than the one I originally started on) which I'd been thinking about for a while before I started my Honours year. As such, I don't feel any sort of obligation to work on it for any purposes other than my own gratification. While this is a good thing by some measures (it's a project that I am interested in, etc., etc.) it is very, very, bad by others (like that fact that I don't feel any particular drive to write about it).

All I know is that I'm well and truly sick of University and computer science. If Honours is a taste of research and a hint of what a Ph.D. is like, then I want nothing to do with either. This used to be fun...

Relational Algebra in Haskell

2005-08-31T14:03:00.000+10:00

I've just spoken to Jon about the problems and ideas I have posted about previously. One of the things I came away with is the suggestion that I might be thinking about relational algebras (perhaps an algebra over a set) rather than hypergraphs. I'm not entirely sure that this is the case (the "hypergraph" Wikipedia article above seems to describe what I'm thinking of), but the "algebra over a set" article is certainly applicable as well).

As a result, I've been able to dig up a couple of things that look like they might help me implement support for generic frames (i.e. those with an arbitrary number of n-relations for arbitrary values of n greater than 0).

While I've seen A Relational Algebra Simulator in Haskell before, it didn't occur to me that it might be applicable to my problem. RATH - Relation Algebra Tools in Haskell, however is new to me and looks like it provides a complete library (rather than the example program of the first link).

Whether I have enough time to catch up on my course-work, finish my system (as it stands), write a thesis and learn enough about this topic to extend the system using such a generalisation remains to be seen.

Another possibly useful generalisation might be to extend the concept of "relation" from sets of tuples to mutisets (or bags) of tuples, thereby allowing relations in a frame to be mutigraphs (i.e. graphs allowing multiple edges between a given pair of vertices). The Data.Graph.Inductive library supports labelled edges which suggests that it might also support multigraphs to some degree (if edges with non-identical labels are non-identical, then you can simulate an unlabelled multigraph by labelled each edge with an index).

I'd like to write a generic graph library with support for multigraphs and [uniform] hypergraphs, possibly by extending Data.Graph.Inductive, but this will probably wind up being pushed back until the Christmas break.

Modal Logic Wikipedia Articles

2005-08-31T13:14:00.000+10:00

I've been poking at Wikipedia again (I dislike free time) and decided that a list of articles relevant to modal logic might be useful. To that end, I present a partial list of Wikipedia articles:

In addition to the articles above (which aren't really directly relevent to my work), there are a number of articles that I've found useful in trying to puzzle my way through things. A partial list of these useful articles is:

More articles will be added to this list as they are uncovered.

Annoyances of the Feature Kind

2005-08-25T18:22:00.000+10:00

Yesterday, I finally sat down and wrote a priority queue (a heap to those in the know) to store the formulae on a branch that still need to be processed. Chris Okasaki (in his book Purely Functional Data Structures) defines the interface of a heap as follows:

class Heap h where    empty     :: (Ord a) => h a
  isEmpty   :: (Ord a) => h a -> Bool

  insert    :: (Ord a) => a -> h a -> h a
  merge     :: (Ord a) => h a -> h a -> h a

  findMin   :: (Ord a) => h a -> a
  deleteMin :: (Ord a) => h a -> h a

This is a problem (in my opinion) in that it requires that heaps (all heaps) be over ordered data-types. The entire reason that I am attempting to extend the heap is to remove the ordering from the contained type, and use a priority type instead. Thus we are no longer saying that, for example, α < β but that (priority α) < (priority β)

I'll be the first to admit that this isn't much of a distinction to make (especially from a pragmatic "programmer" point of view), but it is a nicer approach.

I got around this problem, such as it is, by modifying my Prioritised class to have a function to inject values into my Priority type and one to extract them. The heap then is a type synonym:type PriorityHeap t = LeftistHeap (Priority t) with the restriction that you need to explicitly wrap values you insert into a heap:let h' = insert (priority v) h in ... and unwrap those you get out: let v = value $ findMin h' in ...

Not terribly inconvenient, but not ideal. I'm fairly sure that this could be solved with some functional dependancies magic, but the current state of affairs is good enough to be getting on with.

Purely Functional Data Structures

2005-08-12T15:30:00.000+10:00

The Haskell code from Purely Functional Data Structures by Chris Okasaki can be found as his web-site at the United States Military Academy.

RSChem is Burning Down, Burning Down, Burning Down...

2005-08-05T14:52:00.000+10:00

RSChem is currently on fire. There haven't been any reported injuries, but they have evacuated that precinct of the campus.

Hmmm.

2005-07-29T22:34:00.000+10:00

The presentation is over and done with. It didn't go too badly, though I did run under-time: I finished my presentation and asked (begged) for questions half way through my time slot. I'm not sure how much of it the audience caught, or what sort of comments the assessing academics will give me, but I'm reasonable happy with my performance.

Having seen all of the presentations, I find myself wondering at how many of the projects involve writing compilers and optimisers. One is attempting to learn tests to avoid computing expensive functions unless they're required (with collision detection as the experimental framework). Another is doing something with symbolic optimisation of robot dynamics (which looks a lot like single static assignment). I'm compiling a DSL to Haskell. Someone else is experimenting with interval arithmetic (which I want to implement in Haskell) for scientific computations.

Presentations...

2005-07-28T19:20:00.000+10:00

I have to give my mid-term seminar tomorrow afternoon and I'm getting rather nervous about it.

My supervisor has told me that my slides aren't accessible enough (i.e. I require too much prior knowledge), but I can't see any way to simplify things or remove content without missing important things. I'm not happy, but I don't the time fine-tune it any more.

If you're at the ANU (I'm not sure if the public is allowed) and free tomorrow at 1:00 (my presentation is at 1:26), come along to the Department of Computer Science seminar room (N101) and watch me embarrass myself.

Stupidity or How Dumb Can I Get

2005-07-25T19:21:00.000+10:00

I've just been trying to install hs-plugins on my iBook with GHC 6.4. Sorting out the dependancies, getting stuff to build and getting the libraries installed has been ridiculously complex.

Now that I've got it built and installed (part of which required using hugs because runghc refused to run the setup programme), it doesn't appear to have registered the package, which means I need to manually provide the details to GHC every time I compile some code using System.Plugins (rather than just tell the compiler to use the package: -package plugins).

I need to figure out what it going wrong with my environment and fix it. Perhaps by tearing some capabilities out...

Update: I've got that problem fixed (make install doesn't appear to update the package database). Now all I need to do is work out a way to be able to specify the data-types in the plug-ins.

Dependancies...

2005-07-25T17:26:00.000+10:00

I'm currently experimenting with hs-plugins, a library which supports dynamically loading plugins in Haskell. Or, rather, I would be if I could manage to sort out the various hassles I'm encountering in installing it.

The only problem is that hs-plugins depends on Language.Haskell.Hsx. This would be fine, if it came in the GHC distribution. Alas it doesn't, so I've had to find and install it myself. This isn't too much trouble - I have, after all, been using UNIX-like systems for at least 7 years now. The only bump in this stretch of the road is that Language.Haskell.Hsx depends on Happy.

Haskell is getting to the point where it could really do with a CPAN-style package archive, if only because introducing it now will be so much easier than later when it is actually necessary. Cabal already provides these sorts of features (dependancy chasing, etc).

Generality for its own sake

2005-07-25T14:44:00.000+10:00

System.Console.GetOpt is a Haskell port of the GNU getopt library (which is almost impossible to find, unless they mean getopt(3) in glibc). In spite of being written in Haskell, the awfulness of getopt shines through.

More on Literate Haskell

2005-07-21T22:50:00.000+10:00

I've been having fun extending my environment for literate Haskell programming in LaTeX. While I still haven't looked at the suggestion my previous post provoked (though I'll get round to it eventually), I have been taking the opportunity to learn some of the more programme-y things one can do in LaTeX.

The macro I use for the title of each module (called \module funnily enough) now checks to see if it is a sub-module (i.e. contains a '.' in its name) and makes it a \subsection if it does. For now, this will be enough, but later on there will be some configurability to this to make sure that we don't typeset modules as sub-sections of random other modules.

I'm also planning on making the pretty-printing code build a list of imported modules as it typesets the Haskell and then include the appropriate files (I've got an \import macro all ready and waiting) afterward.

I like playing with LaTeX.

Licencing

2005-07-19T13:28:00.000+10:00

A fourth post for today, also on a non-logic related topic. I'll be releasing an initial, non-modal, version of my code soon (in the next couple of weeks) and need to think about a licence for it. I've narrowed it down to four alternatives:

the Creative Commons attribution share alike licence;
the Creative Commons attribution non-commercial share alike licence;
the Australian Public Licence B; or
a BSD-like licence.

I'm leaning toward the Creative Commons licences at this point, but the Australian Public License could be good as well.

If anyone has suggestions or arguments for or against any licence (please don't bother suggesting the GPL and friends), please leave a comment.

Thoughts on Hypergraphs

2005-07-19T10:12:00.000+10:00

I'll start this post with a disclaimer that I am a mathematically naive person and don't really know what I'm talking about.

After my post last night (or this morning), I though a bit more about hypergraphs and started playing with a few ideas for a data structure based on incidence lists (lists of every edge incident on a particular vertex). While I've got something that works (after a fashion and in a naive and trivial sort of way), I've come to a realisation that I don't really know what a lot of the things I might want to do to such graphs actually mean.

What,if anything, do reflexivity, transitivity and symmetry mean in the context of a hypergraph? I've been trying to figure this out using the composition relation from arrow logic as an example but I'm still not sure I'm getting anywhere.

Be that as it may, I've started working on a prototype of a hypergraph package for Haskell and if I can figure out how various things ought to work and how to generalise it to relations of arbitrary arity, I'll release it separately.

Literate Haskell

2005-07-19T09:27:00.000+10:00

Last night I spent a while wrestling with latex, vim, make and ghc as part of my source-code reorganisation. One of the things I've been wanting for quite a while, is a vim syntax highlighting mode that understands the LaTeX literate Haskell syntax and displays both the Haskell code and the LaTeX code properly. Last night, I finally got it to work, though it has taken a bit of hackery in my Haskell files: I need to have a comment in every file so that the highlighter can detect the LaTeX.

This is a problem as the LaTeX detection heuristic appears to be:

Look for a \documentclass macro (the begining of a LaTeX document); or
Look for a LaTeX command; or
Assume that the "literate" part is not LaTeX

Needless to say, this is rather annoying as I'm writing a program with a number of modules (and thus a number of files) and want to produce a single document from them. To ameliorate this problem, I just make sure to include a LaTeX-style comment on the first line of every literate Haskell file and use a few macros to do include imported modules into the LaTeX document.

I'm also using the listings package to pretty-print the Haskell code and my next goal is to use its custom keyword handling capabilities to automatically include the modules that we import (if they exist in our source tree and are LaTeX-style literate code).

Renovation in Progress

2005-07-19T00:57:00.000+10:00

I'm about one third of the way through the rewrite of the system so far, this time using doing the job properly (checking that there aren't too many or too few of anything in particular, that the numbers all agree, etc). Even if they had no other worth, the clarity that the monadic approach lends to code (parsing and error handling at the moment) more than justifies the presence of monads in Haskell.

I expect to have the system into a fairly robust state in the next day or two after which I'll knock together a small test suite (De Morgan's Laws, a bunch of tautologies and the like) and then move on. I hope to have the features required to implement K finished well within two weeks.

If anyone knows of a way to define a hypergraph inductively, please drop a note in the comments. If I can't find such a representation then I'm going to have a hard time supporting ternary and higher relations.

The Natural Numbers

2005-07-18T19:49:00.000+10:00

One of the statements in my calculus language is the operator declaration:

Neg operator "~" has arity 1, fixity 0, priority 1.

As negative numbers don't really make much sense as the arity and fixity of an operator, I've just spent a while knocking up a Haskell implementation of the natural numbers.

While I dislike programming in Java and other "OO" languages, they do make it a lot easier to extend types than is the case in Haskell. It would be much easier to do this sort of thing if Haskell supported instance declarations (the things that make most polymorphic functionality work in Haskell) on type synonyms. If it did, Natural.hs would be about 6 lines of code (plus a few lines of boiler plate) rather than nearly 60 lines.

My new type Natural (just a wrapper around Integer) is an instance of eight separate type classes:

Eq (they can be compared for equality)
Ord (values can be ordered with respect to each other)
Show (values can be converted to strings)
Read (values can be parsed out of strings)
Bounded (the range of values is bounded), though Natural shouldn't have an upper bound
Enum (values can be enumerated)
Num (values are numbers)
Real (values are real numbers)
Integral (values are integral numbers)

It probably ought to have a few more like:

Random (values can be randomly generated); and
Ix (values can used as array indices)

but it'll get the job done -- all I need from it is Eq and Ord.

A Delay or Murphy Strikes

2005-07-12T11:48:00.000+10:00

I've just had to take my iBook in to The Mac Shop to get its charger (or perhaps the power regulation circuitry) fixed as it no longer wants to charge.

Unfortunately, this means that I'm unable to do any work for the next few days and may not get as much as I'd like done before my return to Canberra.

Cool Things That'll Help

2005-07-10T11:49:00.000+10:00

In the cool things that will help implement this project, the Haskell Hierarchical Libraries contain a Graph library which supports querying the existence a path between specified nodes, just what I'll need to implement box rules.

Another cool thing I need to look at more is the definition of "a monad for stateful non-deterministic computations" in the All About Monads tutorial.

I need to learn more about monad transformers.

Parsing and Patterns

2005-07-10T11:16:00.000+10:00

The logic compiler generates Haskell code to implement a calculus. This includes a data-type to represent formulae, a function to resolve those formulae into sub-formulae, functions to format them for output, miscellaneous utility functions and a parser to parse formulae in the language the calculus operates with. As the code stands currently, the logic language allows the user to define operators with arbitrary arity and fixity. One might, if one were of a mind, define a 4-fix # operator with an arity of 3. A formula with such an operator might look like: α₁ α₂ α₃ # α₄
As the code stands, the generated parser is built using the buildExpressionParser facility of the Parsec parser library. Unfortunately, buildExpressionParser is only capable of handling expression languages with unary prefix, binary infix and unary postfix operators, meaning that we can't generate parsers for all calculi that can be defined with our language.

To fix this, I'm going to have to write a more general expression parser generator (hopefully using buildExpressionParser as a base) that can handle operators of arbitrary arity and fixity. Either that, restrict the system to only unary and binary operators which would make implementing some [conceivable] logics very difficult, if not impossible.

On the other hand, buildExpressionParser has greatly simplified the pattern handling code in the compiler. In our language (which is so simple as to not need a name), we define rules such as: Resolve "a->b" to "~a" or "b". The patterns (the bits in quote marks) are formulae using the operators of the calculus, with arbitrary alphabetic names for variables (which can stand for any sub-formula - we can make no distinction at this point between sub-formulae and propositions as I haven't got round to implementing that yet). Our compiler generates at run time a parser for the formulae of the calculus and uses it to parse the rule patterns and generate appropriate snippets of code which we use for pattern-matching in the Haskell code implementing the calculus. For example, the rule above would be translated to the Haskell code resolve (Impl a b) = Or [(Neg a), b]

Once we've parsed the pattern and generated a function, we get the pattern matching at run-time for free from Haskell.

Done! or It's A Start!

2005-07-09T16:54:00.000+10:00

Last night (or, more correctly, this morning) I constructed a model: ~a, b for the formulæ: ~a, a∨b using only the tableau framework and an automatically generated implementation of the propositional calculus:

Tableau> prove [Neg (Prop "a"), Disj (Prop "a") (Prop "b")]
Model [b,~a]

Now all I have to do is fix the bugs, extend what's there to labelled tableau and test it all. :-)

I can do it, I can do it...

2005-07-03T21:57:00.000+10:00

The system is nearly to the stage where I can write the propositional logic in it. I've been held up by a bit of trouble writing the code to generate a formula parser from the definitions of the logical operators. Once that is written, I need to modify it slightly (to generate a parser, rather than generate code to generate a parser) to parse the rule patterns, and logic compiler will be finished.

Then it'll need a Makefile (or something similar) to link a logic with the tableau engine (the simple, unlabelled version of it is finished), and we'll be finished with this initial stage of development.

Incremental Development

2005-06-27T10:11:00.000+10:00

Incremental development is fun. I've just added support for branching as required to implement the disjunction and implication rules of my propositional calculus and it's been quite interesting to see just how easy a functional programming language makes with sort of exploratory approach to design and development.

Once I've got this up and running (all I need to do is add a check for contradiction), I'll refactor it to be a little neater, write a parser and generator that supports all of the features and get an initial, pre-alpha, demonstration version posted.

Hopefully that'll be in the next two or three days.

Another Night's Worth of Code

2005-06-24T09:52:00.000+10:00

I've just finished the first major part of my first step along the road to [real] implementation: I now have a working type for propositional calculus, a simple representation of a tableau branch, can saturate said branch (modulo the rules which branch) and generate a model (which is simply a list of literals at this point).

Next, I need to extend this tableau implementation to support branching and then complete the logic with correct rules for branching connectives (disjunction and implication). Once that is done, I'll rewrite my language parser and code generator so that I can actually generate this implementation of the propositional calculus from the definition.

Once that is done, I'll move on to the basic propositional modal logic: K. Getting K to work will require that I implement labels, relations and extend my language so that it can import and extend existing logics. Once that is done, I'll move onto a more complex modal logic (perhaps S4) before tackling intuitionistic logic (which uses two-part labels).

Reusing Throwaway Code

2005-06-24T07:08:00.000+10:00

I've just had my first go at writing a monad, and it's harder than it would seem. As a result of my moderately dismal failure, I've decided to go back and actually read the monads sections of the various Haskell tutorials (the Gentle Introduction, Yet Another Haskell Tutorial, and anything else I find laying around on my hard disc). I've just been looking at Yet Another Haskell Tutorial and the section on computations (Section 8.4.2 in the PDF) defines a small graph library which might be a useful starting point when I need to start dealing with transitive, Euclidean and even more bizarre frames and rules with conditions on them.

In one section, I get some [hopefully] usable code, and a better understanding of monads.

[Haskell-cafe] Re: Using type classes for polymorphism of data constructors

2005-06-23T23:36:00.000+10:00

[Haskell-cafe] Re: Using type classes for polymorphism of data constructors

A message on the Haskell-cafe mailing list gives an alternative (better, even) approach to the polymorphism of formulæ using differential types. It works just as well as my solution, and results in much more complex (and therefore complete) types:

Main> :t (Impl (Prop "p") (Poss (Prop "p")))
Impl (Prop "p") (Poss (Prop "p")) :: PC2 PC0 (Modal1 PC0)

I'm not yet sure which route I'll take. My approach results in a single data type (PC, Modal, etc) for each language, which is good, but the types don't mean much and it isn't Haskell-98 (or, at least, Hugs won't load it as such). Ralf's approach also works, the types is assigns formulæ contain more information and it is Haskell-98.

I'll probably wind up using a version based on Ralf's example, unless I run into problems.

Goals: the Motivation of Procrastination

2005-06-23T04:42:00.000+10:00

So far, I have:

written a parser for my logic definition language;
solved the problem I was having with polymorphism;
designed, in the large, my data structures; and
thought about name for the project.

We've now entered the mid-year holiday between the two semesters and I am hoping to get a large amount of my implementation done during the break. On my list of things to do are:

define a state monad (to model the saturation of a branch);
define a backtracking monad (to model the branching of non-deterministic choices);
find a way to compose them (perhaps by deriving a monad transformer);
finalise the structure of the logic modules;
write a realistic (perhaps even production) parser and code generator for the logics;
learn to use hs-plugins to write dynamically loadable modules (and find a way to make logic modules dynamically loadable); and
implement some representative test logics (propositional calculus, K, intuitionistic logic, something with transitive frames, etc).

I've got a lot of work ahead of me, but the next few weeks are going to be fun. At the end of it, I will (I hope) have a running system to extend and improve and a much greater knowledge of Haskell.

Polymorphism and Generality Redux; or The Beneficial Side Effects of Reading

2005-06-22T23:32:00.000+10:00

I've started looking at how to code my backtracking monad (the framework that will provide the branching, failure, etc within which the tableau method for each logic will be implemented). To try to get a handle on the subject, I've started looking at Deriving Backtracking Monad Transformers by Ralf Hinze.

Section 3 of the paper defines an abnormal termination (i.e. exceptions) monad and 3.1 begins to define a transformer to extend an arbitrary monad with exceptions. As part of this, it uses an existentially quantified type variable in the definition of a type constructor (for :>>=). Needless to say, the similarity to my previous attempts to make polymorphic formulae was obvious.

Although I'm still, by any meaningful standard, a Haskell novice and haven't looked at this extension before, I've managed to extend that example (by restricting the type variable to members of my Formula type class) and Hey, Presto! I can now create polymorphic types representing my inter-mixable logical languages.

As an example, I've got a type PC for the propositional calculus, and a type < span style="font-family: monospace;" >Modal for alethic modal logic. The connectives of each language can take formulae of either type (or both) as parameters, and everything Just Works^TM.

Polymorphism, they way it was intended.

Meta-post: Inward Links.

2005-06-16T05:58:00.000+10:00

Wow, this blog has been mentioned in both Consequently (Greg Restall's blog) and That Logic Blog (Jon Cohen's blog).

Now I'll just have to get some meaningful posts up.

Hello, I'll be your host tonight as we play...

2005-06-11T23:25:00.000+10:00

Name that Project...

My project is in need of a name. Rather than give it an acronym, I've been trying to think of a name at least somewhat relevant to the topic at hand and my approach. I'm currently thinking about "Vindaloo" with the rather tenuous link being Haskell Curry and that the project will, I hope, be pretty hot (for some definition). "Vindaloo," though, doesn't have all that much to do with modal logic.

Names have never been a strong point of mine (I still don't know the names of many of the people I've seen and talked to every day this year), so I'll take this opportunity to solicit suggestions: If you can think of a name for a labelled tableaux theorem prover written in the Haskell programming language please leave your suggestions in a comment, or email them to me at: thsutton at gmail dot com.

Polymorphism and Generality

2005-06-11T23:06:00.000+10:00

One of the main goals of this project, to my mind at least, is generality. The prover must be easily extendable with support for a wide range (ideally, the entire range) of labelled tableaux calculi. Furthermore, it ought to be possible to define new logics as extensions to existing logics: propositional modal logic, for example, is an extension of the propositional calculus to support two new operators: ◇ and □.

Unfortunately, I've not been able to get determine just how to get this level of flexibility to work under Haskell's type system. I've asked the Haskell-cafe mailing list for pointers and, in the mean time, have moved on to doing this composition in the compiler for my mini-language rather than in the generated Haskell code.

Hopefully, I'll get this to work as it will be quite useful and, unless I'm mistaken, interesting.

Data Structures

2005-06-10T18:22:00.000+10:00

I'm getting to the point where I'll have to start thinking about the data structures used to implement my tableaux. They need to be as small as possible and allow fast membership testing and updating. As my current goal is to accept a formula to prove and produce either a counter-model or a "yes" as output. As such, I will only ever need access to those parts of the tree on the path from the current node, to the root. The tree is, essentially, the progress of the computation backtracking over time.

As such, I'm looking forward to trying to write the run-time (once I've finished figuring out how the logic-specific code the DSL will be transformed into will work). It will require a bit of input handling (in the IO monad), parsing (in the Parser monad) and backtracking (in some backtracking monad) along with some state (perhaps a State monad, perhaps built into the backtracking monad) and a whole bunch of lazy computation (the actual tableau rules).

Unless I am overlooking something (I'm sure I am and I imagine that Raj and Pietro agree), my main data structure will be...
a list. The main rationale behind this decision (rather than trying to build some sort of tree structure, or some bizarre nested set-like structure) is that, as I'm merely trying to build a model, the tree itself is expressed in the computation (or, rather, its backtracking). Furthermore, as I'm working with labelled tableaux (with an explicit modal relation), all I need to construct a model once I've found an open branch is the list of formulæ (and relations) from the end of that branch, to the root of the tree.

In Haskell, lists act like (and probably are) singly linked lists of cons cells with a pointer to the item, and one to the rest of the list. This means that you can add stuff to the front of a list without modifying the original list. This is rather helpful as it means that we can add junk onto one end of a list, which is what we'll be doing with tableaux (adding things to the end of the branch), and you can have multiple lists sharing the same tail (to give an right-way-up tree structure, like an upside-down tableau or a sequent proof). As we're going to be doing backtracking (because we can through away everything we don't need to write a model), and we've got a ready-made tree structure that can be extended at the leaves, there is a very simple way to code it all up: as a monad (for the backtracking) over the list pointers.

Using a monad (probably a MonadPlus) to implement backtracking will allow us to express branching naturally (using mzero "fail" on branch closure and mplus to do the "branching" evaluation) and if we add in a little state to each branch (a pointer to the current head of the list, for instance) we have a backtracking model search procedure. All that remains is to implement it (no doubt discovering that my understanding of monads is completely wrong) and find out which mountains I need to move to get this approach to work for the non-simple case...

Advice, Suggestions and Supervision

2005-06-10T15:47:00.000+10:00

I've just had a talk with Pietro about my project and directions in which I might move it. Pietro's PhD project (the Tableaux Work Bench) is written in OCaml (an eager functional programming language) and works with implicit tableaux. My Honours project (which needs a name, suggestions are welcome) is written in Haskell (a lazy, pure functional language) and works with labelled tableaux.

In spite of these differences, the projects are quite similar and Pietro's advice and suggestions are going to be invaluable. In our meeting, we discussed the data structures I am planning on using which has helped solidify my thoughts, which I shall write up and post this evening.

Parsing stuff in Haskell

2005-06-10T04:45:00.000+10:00

I've just started looking parsing in Haskell with Parsec. After a few hours of reading the documentation (PDF, 424K)and poking at the examples, I've managed to hack together a parser for my little language.

Only a few hours after I started looking at Parsec, I've got a prototype which generates code in an abstract syntax suitable for passing to a semantics checker and code generator (the system will generate Haskell from specs written in my DSL, which is then linked against some infrastructure). Very cool. Haskell is great for my productivity.

About Labelled Tableaux

2005-06-06T01:00:00.000+10:00

On this blog I will chronicle the work on my Honours project in computer science: developing a system to construct counter-models for non-theorems of modal logics. This system will be a small theorem prover based on tableaux, written in Haskell.

I will link to relevant papers and technical reports, technical details which I encounter whilst coding, material that I make available to download, and anything else in the slightest bit relevant to the topic at hand.