Re: [isabelle] Where to learn about HOL vs FOL?



Yes, the question of whether or not to adopt an explicit logic of “definedness” continues to attract discussion. Most implemented formal systems have only total functions. Then there is PVS and the dependently-typed calculi, which allow partial functions but still don’t formalise the notion of “undefined”. I believe that Farmer advocates such formalisms. LCF and related systems formalise domain theory, in which the concept of definedness induces a partial ordering over all values. As always, increasing the expressiveness of the formalism also increases the difficulty of conducting proofs.

Larry Paulson


On 29 Dec 2013, at 21:55, Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr> wrote:

> From the same author (W. M. Farmer), an academic course (link below) I landed into. Its wordings in chapter 5, made me feel I've read something like this before… indeed, as I checked, this was in the Seven Virtues of STT.
> 
> http://imps.mcmaster.ca/courses/SE-2F03-05/slides/
> 
> Chapter 5 concisely explains (to me, even more concisely than in the Seven Virtues) many of the theoretical concepts found in Isar‑Ref and the Isabelle Tutorial (for people like me who are not from the academic world). He's a lot fan of the type theory.
> 
> Interestingly, at the end, he suggest an extension of STT, which would include indefinite expressions, which seems to be the same as what shown‑up during another topic with references to HOL+LCF as HOLCF (an Isabelle theory).





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