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 Hilbert-style systems
for automated proof. This is, of course, correct, since Hilbert-style
metatheorems become symbolically representable in natural deduction as regular theorems (and not just metatheorems), but 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, such that the method with the least amount of rules of inferences, i.e., a Hilbert-style system, is preferred, and all other rules become derived
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.

GZ








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.