# ANN: theoremquest-0.0.0

14 messages
Open this post in threaded view
|
Report Content as Inappropriate

## ANN: theoremquest-0.0.0

 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 [hidden email] 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_______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|
Report Content as Inappropriate

## Re: ANN: theoremquest-0.0.0

 On 28 February 2011 14:59, Tom Hawkins 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?No.I'd wage money on it.-- Colin AdamsPreston, Lancashire, ENGLAND()  ascii ribbon campaign - against html e-mail /\  www.asciiribbon.org   - against proprietary attachments _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|
Report Content as Inappropriate

## Re: ANN: theoremquest-0.0.0

 Have you tried it? It's completely addictive (and takes up a big chunk of my free time). I'm not sure it'll appeal to everyone, but I wouldn't dismiss it off-hand like that. On Mon, Feb 28, 2011 at 10:16 AM, Colin Adams wrote: On 28 February 2011 14:59, Tom Hawkins 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?No.I'd wage money on it.-- Colin AdamsPreston, Lancashire, ENGLAND()  ascii ribbon campaign - against html e-mail /\  www.asciiribbon.org   - against proprietary attachments _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|
Report Content as Inappropriate

## Re: ANN: theoremquest-0.0.0

Open this post in threaded view
|
Report Content as Inappropriate

## Re: ANN: theoremquest-0.0.0

 In reply to this post by Tom Hawkins-2 > I find this fairly interesting. Once you're finished grappling with the > logical core, I wouldn't mind helping out with a web interface, time > permitting. I suspect attracting mass appeal, or getting users at all, is > helped massively by having a web interface. Thanks for your interest.  Yes, a web interface would be ideal. Currently the library has hooks to translate the transactions to JSON to ease construction of any Javascript client -- thought these translations still need to be implemented.  Note the 'RspInJSON' request: http://hackage.haskell.org/packages/archive/theoremquest/0.0.0/doc/html/TheoremQuest-Transactions.html#t:Req_______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|
Report Content as Inappropriate

## Re: ANN: theoremquest-0.0.0

 In reply to this post by Colin Adams-3 On Mon, Feb 28, 2011 at 17:02, Colin Adams <[hidden email]> wrote: > > No I haven't. I'm not a mass-market gamer. I'm an ex-hard-core gamer. > I think that basically, it is the same psychological stuff that is going on in the brains of (puzzle) gamers and people who interactively proves theorems. It is like solving an intricate puzzle, the pieces fitting just being lemmas, axioms, definitions, corollaries and what not. It gives me the very same kick as fragging 8 players with a quad in Quake Live does. That said, it is probably not for everybody. What is true of both is that they are quite addictive. Learning to do a technically hard jump in QL is the very same as learning a new proof technique: when you have it under your wings, you can go to places impossible before. Many "normal" puzzle games fit into the NP-complete class as well, so it would look as if human beings like the challenge of trying to solve hard problems. Theorem proving is simply yet another beast in the zoo, underpinning the other games. -- J. _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|
Report Content as Inappropriate

## Re: ANN: theoremquest-0.0.0

 On 28 February 2011 17:59, Jesper Louis Andersen wrote: Many "normal" puzzle games fit into the NP-complete class as well, so it would look as if human beings like the challenge of trying to solve hard problems. Theorem proving is simply yet another beast in the zoo, underpinning the other games.Cale Gibbard once argued that programming is essentially a form of theorem proving. And people love programming as a hobby, so I can see that taken to its "logical conclusion" (groan) of actually solving proofs. Could there be a ProofOverflow? Tee, just joking. I think. _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|
Report Content as Inappropriate

## Re: ANN: theoremquest-0.0.0

Open this post in threaded view
|
Report Content as Inappropriate

## Re: ANN: theoremquest-0.0.0

 > But what I miss when using these proof assistants, and what I have my > eyes on, is a way to Search ALL The Theorems.  In current proof > assistants, developments are still distributed in "packages" -- and a > particular development might have already proved a very useful lemma > that wasn't the main result, and if I'm doing something only barely > related I will probably not find that package and have to prove that > lemma again.  I hope that a *good* theorem search engine would bump > the level at which I do computer-assisted mathematics to nearly the > level I do math in my head (conceptual, not technical). Theorem search is one of my main motivations for a multi-player, centralized database architecture.  With two people plugging away at different problems, I have to imagine occasionally they develop lemmas that could benefit each other.  Of course the search could be googlish, where one would enter a desired proposition and it would return a handful of matching candidates.  It could also be automated. For example, each theorem submitted to the database could be checked if, a) any assumptions of the theorem are already proven, and b) any other theorem call it out as an assumption.  Then these reductions would be perform automatically.  The greater the ability of the search to bridge the gap between dissimilar conclusions and assumptions, the greater the automation. Thanks for your interest.  Let me know if you have any suggestions or guidance. -Tom _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|
Report Content as Inappropriate

## Re: ANN: theoremquest-0.0.0

 In reply to this post by Luke Palmer-2 On Mon, 2011-02-28 at 19:37 -0700, Luke Palmer wrote: > But what I miss when using these proof assistants, and what I have my > eyes on, is a way to Search ALL The Theorems.  In current proof > assistants, developments are still distributed in "packages" -- and a > particular development might have already proved a very useful lemma > that wasn't the main result, and if I'm doing something only barely > related I will probably not find that package and have to prove that > lemma again.  I hope that a *good* theorem search engine would bump > the level at which I do computer-assisted mathematics to nearly the > level I do math in my head (conceptual, not technical).  That may be a > pipe dream. This was attempted to some extent in the Mowgli and HELM projects: http://mowgli.cs.unibo.it/http://helm.cs.unibo.it/The HELM project in particular is relevant.  To whit: > First of all, having a common, application independent, meta-language > for mathematical proofs, similar software tools could be applied to > different logical dialects, regardless of their concrete nature. This > would be especially relevant for all those operations like searching, > retrieving, displaying or authoring (just to mention a few of them) > that are largely independent from the specific logical system. > Unfortunately the related Coq and NuPRL searchable libraries seems to be down at the moment, as all implementation effort has been switched to Matita, which uses some of the Mowgli and HELM components. Thanks, Dominic _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|
Report Content as Inappropriate

## Re: ANN: theoremquest-0.0.0

 In reply to this post by Daniel Peebles Daniel Peebles schrieb: > Have you tried it? It's completely addictive (and takes up a big chunk > of my free time). +1  after completing some missions in PVS. :-) _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|
Report Content as Inappropriate

## Re: ANN: theoremquest-0.0.0

 In reply to this post by Tom Hawkins-2 On Feb 28, 7:59 pm, Tom Hawkins <[hidden email]> 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 [hidden email] > 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|
Report Content as Inappropriate

## Re: ANN: theoremquest-0.0.0

 > I am curious -- how easy is it to use theoremquest for playing with > equational theories? Let me turn the question around:  How easy is it to play with equational theories in HOL Light?  Because this is the planed basis for TheoremQuest. -Tom _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe