On Feb 28, 7:59 pm, 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 tomahawk...@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 am curious -- how easy is it to use theoremquest for playing with equational theories? In particular equational logic -- see https://www.ideals.illinois.edu/bitstream/handle/2142/11411/A%20Rewriting%20...