[Haskell-cafe] ANN: theoremquest-0.0.0

[Tom Hawkins]

I have been wanting to gain a better understanding of interactive
theorem proving for some time.  And I've often wondered: Can theorem
proving be made into a user-friendly game that could attract mass
appeal?  And if so, could a population of gamers collectively solve
interesting and relevant mathematical problems?

To try to answer these questions -- and to gain some experience myself
with theorem proving -- I started a project called TheoremQuest [1].
TheoremQuest intends to be a multi-player game system, where the game
server receives requests by clients, such as theorem queries and
inference rule applications.  The TheoremQuest server validates
deductions, compares them with existing theorems in the database, then
returns results.  TheoremQuest's deductive system borrows that of John
Harrison's HOL Light [2].

There are 2 Hackage packages:  theoremquest [3] is a library that
declares types for terms, inference rules, and client-server
transactions, used by both server and clients; and theoremquest-client
[4] is an example client (tq).  All the code, including the
server-side, is hosted at github [5].

Currently the client-server interface is working, but little else.
The library has defined most of the core inference rules, but has none
of the basic types or axioms.  And the "tq" client is nothing at all
like a game; at this point it is just a command line tool to test the
server.  Currently "tq" can ping the server, create a new user, apply
inference rules, and print out theorems.  Here's how "tq" can prove "x
|- x":

$ tq newuser tomahawkins tomahawkins at gmail.com
Ack
$ export THEOREMQUEST_USER=tomahawkins
$ tq infer 'ASSUME (Var (Variable "x" Bool))'
Id 1
$ tq theorem 1
assumptions:
Var (Variable "x" Bool)
conclusion:
Var (Variable "x" Bool)

I'd love to have help with this project, if anyone's interested.  I'm
still grappling with the logical core, but I think the real challenge
will be creating game clients that are both capable and yet intuitive
enough to appeal to the general population.  If the masses can play
Sudoku, shouldn't they be capable of interactive theorem proving?

-Tom

[1] http://theoremquest.org
[2] http://www.cl.cam.ac.uk/~jrh13/hol-light/
[3] http://hackage.haskell.org/package/theoremquest
[4] http://hackage.haskell.org/package/theoremquest-client
[5] http://github.com/tomahawkins/theoremquest