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



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.


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, but contrast also helps to learn something.


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


	Makarius

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




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