[Haskell-cafe] Using type classes for polymorphism of data
thsutton at gmail.com
Tue Jun 14 21:45:47 EDT 2005
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
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.
More information about the Haskell-Cafe