On 13/06/2005, at 8:29 PM, Henning Thielemann wrote:
On Sat, 11 Jun 2005, Thomas Sutton wrote:
The end goal in all of this is that the user (perhaps a logician
rather than a computer scientist) will describe the calculus they
wish to use in a simple DSL. This DSL will then be translated into
Haskell and linked against some infrastructure implementing general
tableaux bits and pieces. These logic implementations ought to be
composable such that we can define modal logic to be propositional
calculus with the addition of [] and <>.
Is there a need for a custom DSL or will it be possible to express
theorems in Haskell?
Having used HOL a bit, I'm not sure that using a general PL as the
user interface to a theorem prover is such a great idea. The goal of
the project (an honours project) is to be able to construct
[counter-] models using as wide a range of /labelled tableaux
calculi/ as possible, thus the need for a DSL of some description (to
specify each calculus).
The theorems themselves will be expressed using the operators
described for each calculus (using the DSL). It will be, in essence,
a meta theorem prover.
QuickCheck can test properties which are just Haskell
functions with random input, so it would be comfortable to use these
properties for proving, too. There is also the proof editor Alfa.
As far
as know it is written in Haskell but the theorems are not expressed in
Haskell.
I've not looked at QuickCheck yet, though I've been meaning to get to
it for quite a while; I'll have to bump it up the queue.
Cheers,
Thomas Sutton
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
