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 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.


Indeed.

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.

Well, "valid or not" is indeed the question, nothing else.




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