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

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:

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":

The newer "Handbook of Practical Logic and Automated Reasoning" by John Harrison also has a chapter on "Interactive theorem proving", see also --- 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.


        1,152,367 people so far

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