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



I'll follow up with more details/questions later, but I want to express my
gratitude immediately: thank you *very* much.

On Monday, December 15, 2014, Makarius <makarius at sketis.net> wrote:

> On Fri, 21 Nov 2014, Josh Tilles wrote:
>
>  I've come across a few errors that are blocking my progress. I'm not sure
>> what to do besides trying to become familiar with *all* of Isabelle's
>> internals
>>
>
> As far as I can tell, there is nobody on this planet who is familiar with
> all of Isabelle's internals. In fact the situation is better imagined like
> this: http://toplowridersites.com/you-are-here-milky-way-galaxy/
>
>
> 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
>
> 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.
>
>
> That won't help in the project to remove the classical principle from
> Isabelle/HOL, which I would consider futile.  Why change the logic anyway?
> Better use it (and its many ad-on tools) to model your own language and
> logic inside it.
>
>
>         Makarius
>
> ------------------------------------------------------------
> ----------------
>                 http://stop-ttip.org  1,152,367 people so far
> ------------------------------------------------------------
> ----------------
>



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