Re: [isabelle] Some corrections and amendments
On 12.07.2016 02:19, Gottfried Barrow wrote:
On 7/11/2016 2:57 AM, Andreas RÃhler wrote:
On 09.07.2016 05:05, Gottfried Barrow wrote:
On 7/7/2016 11:26 AM, Ken Kubota wrote:
Paulson argued that natural deduction is far superior to
for automated proof. This is, of course, correct, since Hilbert-style
metatheorems become symbolically representable in natural deduction
theorems (and not just metatheorems), but this only reflects the
perspective with the pragmatic aim of quickly obtaining proofs. For
philosopher it is not proof automation but expressiveness that is
criterion, such that the method with the least amount of rules of
i.e., a Hilbert-style system, is preferred, and all other rules
In particular, there is this sentence of yours: "...this only
reflects the engineer's perspective with the pragmatic aim of
quickly obtaining proofs. For the philosopher it is not proof
automation but expressiveness that is the main criterion..."
I completely understand the issue of low status vs. high status [ ... ]
The difference seems that between "What" and "How" rather.
No serious discussion what supposed to ensue, and it's not supposed to
start with my reply here. Your short sentence tells me that maybe you
didn't focus on my jokes.
Any seriousness was supposed to get swamped by my attempt at creative
writing. The attempt at creativity was for the purposes of ridiculing
an idea. There was actually no need for a defense to be made. Writing
nothing would have been better, maybe.
Ken wants to compare his raw ideas, valid or not (I wouldn't know),
with Larry Paulson's work, which is the foundation for what has ended
up being more than 30 years work, founded on Robin Milner's ML,
drawing from Mike Gordon's work, propelled further by Tobias Nipkow et
Well, "valid or not" is indeed the question, nothing else.
This archive was generated by a fusion of
Pipermail (Mailman edition) and