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 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
___
Ha
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
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/li
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 hav
> 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
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
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
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 solvi
> 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,
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 tha
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 wan
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.
--
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 mathe
14 matches
Mail list logo
