Re: [Haskell-cafe] ANN: theoremquest-0.0.0
On Mar 8, 8:20 pm, Tom Hawkins wrote: > > 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. Dunno... I am far from being a theorem-prover buff/expert :-) I know of Dijkstra-Scholten logic -- not as a formal logician but as a math teacher. But anyhow that (HOL) gives me some context and sense of direction -- Thanks. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANN: theoremquest-0.0.0
On Feb 28, 7:59 pm, 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? 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
Re: [Haskell-cafe] ANN: theoremquest-0.0.0
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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANN: theoremquest-0.0.0
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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANN: theoremquest-0.0.0
On Mon, Feb 28, 2011 at 7:59 AM, 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? And if so, could a population of gamers collectively solve > interesting and relevant mathematical problems? I think this is an interesting project. This kind of thing has been on my mind recently. I haven't necessarily been thinking about how to "publicize" theorem proving, but I have been thinking about how to use computers to coordinate the efforts of mathematicians (including mere hobbyists like me). While our goals are not identical, they are certainly related. I was set on creating my own language for a while that would facilitate this, because I'm that kind of hubristic fellow. But I realized that it would probably be a better tactic to use an existing, more popular system, since I can leverage the existing work of others for a basis, and others already know their way around this system. It's easier to get critical mass starting from a few hundred than from one. 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. A theorem search engine I would consider "good" would have to solve a few technical problems: a big one is recognizing isomorphisms -- two people declared isomorphic structures and then proved some different results about them. We would like to be able to search for results about one and find results about the other. This is probably assisted by a user who proves the isomorphism between the two structures -- inferring isomorphisms automatically is probably too much to hope for. And then there's the issue of the highly overloaded word "isomorphism" -- there is no single definition, and results can be interchangeable in different ways appropriate in different contexts with different subtleties. Suffice to say I think your project is cool and I have my eye on it. Have you thought about searching? Luke > 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'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 > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org
Re: [Haskell-cafe] ANN: theoremquest-0.0.0
On 28 February 2011 17:59, Jesper Louis Andersen < jesper.louis.ander...@gmail.com> 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANN: theoremquest-0.0.0
On Mon, Feb 28, 2011 at 17:02, Colin Adams 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANN: theoremquest-0.0.0
> 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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] ANN: theoremquest-0.0.0
No I haven't. I'm not a mass-market gamer. I'm an ex-hard-core gamer. On 28 February 2011 15:53, Daniel Peebles wrote: > 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 < > colinpaulad...@googlemail.com> 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 Adams >> Preston, Lancashire, ENGLAND >> () ascii ribbon campaign - against html e-mail >> /\ www.asciiribbon.org - against proprietary attachments >> >> ___ >> Haskell-Cafe mailing list >> Haskell-Cafe@haskell.org >> http://www.haskell.org/mailman/listinfo/haskell-cafe >> >> > -- Colin Adams Preston, Lancashire, ENGLAND () ascii ribbon campaign - against html e-mail /\ www.asciiribbon.org - against proprietary attachments ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] 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 Adams > Preston, Lancashire, ENGLAND > () ascii ribbon campaign - against html e-mail > /\ www.asciiribbon.org - against proprietary attachments > > ___ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > > ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] 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 Adams Preston, Lancashire, ENGLAND () ascii ribbon campaign - against html e-mail /\ www.asciiribbon.org - against proprietary attachments ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] 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 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'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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
