*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] Experimental tweaks to make HOL intuitionistic-by-default*From*: Josh Tilles <merelyapseudonym at gmail.com>*Date*: Sun, 21 Dec 2014 18:03:07 -0500*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <alpine.LNX.2.00.1412211403240.33155@lxbroy10.informatik.tu-muenchen.de>*References*: <CAGTcTFw5QbLPQ_YaSzmT5uXLgVjuyo6vnKNrmEJcGrzfEYCh=A@mail.gmail.com> <425E3845-D343-40DD-ADCA-81E49E4C6375@cam.ac.uk> <CAGTcTFzPk4XsjKFcQenDqPR5xE84VO9ihb8uEEQSKSzU1vkT=A@mail.gmail.com> <alpine.LNX.2.00.1412152100540.30515@lxbroy10.informatik.tu-muenchen.de> <CAGTcTFygtwufnmF7_0dD3hbViLXubfh5Tp0twYkHQPcJOdADSA@mail.gmail.com> <alpine.LNX.2.00.1412211403240.33155@lxbroy10.informatik.tu-muenchen.de>

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

**References**:

- Previous by Date: Re: [isabelle] Experimental tweaks to make HOL intuitionistic-by-default
- Next by Date: [isabelle] Now out in print: "Concrete Semantics with Isabele/HOL"
- Previous by Thread: Re: [isabelle] Experimental tweaks to make HOL intuitionistic-by-default
- Next by Thread: [isabelle] Deadline Extension: FESCA@ETAPS 2015
- Cl-isabelle-users December 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list