Re: [isabelle] Some corrections and amendments
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 the
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 al.
I'm nobody's friend here, but I gotta figure that Isabelle, its logic
included, simply represents what Larry Paulson decided to commit to as a
public work, that its not the totality of his mind.
As to "what", "how", and "why", it's not like he hasn't been exposed to
a full gamut of ideas, including that which is pure and impractical.
People want to attack the purity of Isabelle/Pure, but without providing
a serious alternative. Maybe it's the "30 years work thing", that a
serious work takes.
This archive was generated by a fusion of
Pipermail (Mailman edition) and