Re: [isabelle] Experimental tweaks to make HOL intuitionistic-by-default



On Sun, Dec 21, 2014 at 8:10 AM, Makarius <makarius at sketis.net> wrote:

> On Sat, 20 Dec 2014, Josh Tilles wrote:
>
>  On Fri, 21 Nov 2014, Josh Tilles wrote:
>>>
>>>  P.S. I'm about a hundred pages into *ML for the Working Programmer*, so
>>> I
>>>
>>>> apologize if all of my questions are just a result of my not yet having
>>>> read the chapter about constructing a tactical theorem prover [?]
>>>>
>>>>
>>> There is certainly something to learn from it: how proof assistants were
>>> implemented in the early 1990-ies. See also the famous Handbook article
>>> by
>>> Larry Paulson "Designing a theorem prover": http://www.cl.cam.ac.uk/
>>> techreports/UCAM-CL-TR-192.html
>>>
>>
>> Are you being tongue-in-cheek? I can't tell. Like, I wouldn't have
>> guessed that implementation techniques from twenty years ago are relevant
>> now...
>>
>
> I did not intend to make jokes about old, but important articles.  There
> is definitely something to learn from ancient times, where the concepts are
> easier to see without all the rest around it that emerged over the
> decades.  Of course, you need to put things into the historical
> perspective, and see the key points of newer prover architecture --
> Isabelle is very rich in that respect.

Ahh, I understand now. That's a very good point! Thank you for clarifying.

>
>
>
>  The newer "Handbook of Practical Logic and Automated Reasoning" by John
>>> Harrison also has a chapter on "Interactive theorem proving", see also
>>> http://www.cl.cam.ac.uk/~jrh13/atp --- it describes HOL-Light, so the
>>> prover architecture is very minimalistic.
>>>
>>
> Note that HOL-Light is interesting in being a minimalistic model of an
> LCF-style prover that is in actual use.  That is part of its culture, and
> in contrast to Isabelle,

noted. thanks

> but contrast also helps to learn something.

agreed.

>  Better use it (and its many ad-on tools) to model your own language and
>>> logic inside it.
>>>
>>>  I'm not sure what you mean. Could you elaborate? Or perhaps point me
>> toward some examples or explanations by other people?
>>
>
> See what Larry said about non-standard analysis.

Will do.

>   When you want to do realistic applications, it is better to keep the
> existing logical foundations, and build within that huge building what you
> need in addition.
>
For realistic applications, I wholeheartedly agree. But I don't believe I'm
working on "realistic" applications (at the very least, not yet);
basically, I'm just using Isabelle to do math while learning math.

>
>
>         Makarius
>
> ------------------------------------------------------------
> ----------------
>                 http://stop-ttip.org  1,218,911 people so far
> ------------------------------------------------------------
> ----------------
>



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