Hi Bill,
Why are miz3 and Mizar the only proof assistants where
one can easily write up human readable proofs?
I'm surprised you're not including Isar in this list!
And do you know about ForTheL (see
http://nevidal.org/download/forthel.pdf)? Now _there's_
a readable formal language! :-)
Also,
Hi Rob,
(exists f. forall x. P(x, f(x))) = (forall x. exists y. P(x, y))
So _this_ is the kind of choice that I have no problems with,
as it doesn't threaten my Platonism. (It is even provable
in type theory! (But only if you use the right flavor of
existential quantifier of course :-)))
I
Hi Cris,
At a philosophical level I'm surprised that Freek's
intervals of Platonism are during the week, with formalism
on weekends.
It was a reference to a book related to the philosophy
of mathematics that I liked a lot when I was much younger.
See the quote on
On Tue, Aug 7, 2012 at 1:19 PM, Freek Wiedijk fr...@cs.ru.nl wrote:
Also, does anyone know what is the status of Mohan
Ganesalingam's work in this direction (see for example
http://people.pwf.cam.ac.uk/mg262/CSLI%20talk.pdf)?
No, but we can ask him :) (CC'ed)
Context:
The tutorial for the HOL-Omega system is still in process, but there is now
available a teaser for the tutorial. This is essentially one chapter of the
tutorial, giving a series of examples that in a light way briefly
demonstrate the essential new features of the logic.
You check that your definition is correct by proving appropriate
theorems about it. For example, HOL4 provides an EVAL function so
that you can do things like
EVAL ``FACT 20``;
val it = |- FACT 20 = 243290200817664: thm
and this is the sort of thing you'd like to
On 08/08/12 11:21, Bill Richter wrote:
Thanks, Michael! HOL Light does not have your EVAL, but maybe it has
something similar. EVAL is indeed the sort of thing that Colin Rowat and I
were looking for. I did read a bit about rewriting, and I see that it's in
the EVAL ballpark, but it
