On Feb 28, 7:59 pm, Tom Hawkins <tomahawk...@gmail.com> wrote: > 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%20Decision%20Procedure%20for%20Dijkstra-Scholten%27s%20Syllogistic%20Logic%20with%20Complements.pdf?sequence=2 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
