It can be downloaded from here: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.27.6103
Larry Paulson > On 8 Aug 2016, at 12:13, Ken Kubota <m...@kenkubota.de> wrote: > > Dear Members of the Research Community, > > As part of my efforts to try to understand the type system of Isabelle/HOL, I > have gathered the references from the mails written by Corey Richardson and > Michael Norrish and from The Isabelle/Isar Reference Manual, especially from > a) Chapter 10: Higher-Order Logic (pp. 236 f.) > b) § 11.7 Semantic subtype definitions (pp. 260-263) > c) § 11.8 Functorial structure of types (pp. 263 f.). > > In all cases, with one exception, I was able to obtain either the link to the > online version or the ISBN number. > > > The exception is Mike Gordon's text "HOL: A machine oriented formulation of > higher order logic" (Technical Report 68, University of Cambridge Computer > Laboratory), registered at > http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-68.html > > As Isabelle is provided by the University of Cambridge Computer Laboratory, > among others, would it be possible for the Isabelle developers to make this > technical report available online as a PDF file? This was done for the first > five reports listed at > http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-table.html > > According to the references supplied with the traditional (Mike Gordon's) HOL > variant, a revised version exists: "Technical Report No.\ 68 (revised > version)", quoted from > > https://github.com/HOL-Theorem-Prover/HOL/blob/master/Manual/Description/references.tex > Either both versions or the revised version should be made available. > > > I would like to take this opportunity to thank Michael Norrish for his > advice. > The LOGIC part of HOL4 system's documentation at > > http://sourceforge.net/projects/hol/files/hol/kananaskis-10/kananaskis-10-logic.pdf > is the kind of short and precise formulation of the logical core I recently > proposed for Isabelle/HOL, too: > > https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-July/msg00105.html > > In this HOL4 document, it is stated: "From a logical point of view it would > be > better to have a simpler substitution primitive, such as 'Rule R' of Andrews' > logic Q0, and then to derive more complex rules from it." (p. 27) > This is exactly the same idea that I presented recently: "The main criterion > is > expressiveness [cf. Andrews, 2002, p. 205], or, vice versa, the reducibility > of > mathematics to a minimal set of primitive rules and symbols. [...] For the > philosopher it is not proof automation but expressiveness that is the main > criterion, such that the method with the least amount of rules of inferences, > i.e., a Hilbert-style system, is preferred, and all other rules become > derived > rules." > > https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-July/msg00028.html > > Similarly, the HOL4 document argues in favor of definitions instead of > introducing new axioms: "The advantages of postulation over definition have > been likened by Bertrand Russell to the advantages of theft over honest toil. > As it is all too easy to introduce inconsistent axiomatizations, users of the > HOL system are strongly advised to resist the temptation to add axioms, but > to > toil through definitional theories honestly." [p. 33] > In the same manner, I wrote: "One consequence [...] is to avoid the use of > non-logical axioms. [...] The appropriate way to deal with objects of certain > properties is to create a set of objects with these properties." [Kubota, > 2015, > p. 29] > For this reason, in the R0 implementation, the group axioms are expressed not > as axioms, but as properties in the definition of "Grp" (wff 266): > > http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf > (p. 359) > > > Kind regards, > > Ken Kubota > > > > Sources > > [S1] The Isabelle/Isar Reference Manual (February 17, 2016) > > http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2016/doc/isar-ref.pdf > > [S2] Reference in the e-mail written by Corey Richardson > > https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-July/msg00070.html > > Dmitry Traytel / Andrei Popescu / Jasmin C. Blanchette, Foundational, > Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied > to > Theorem Proving > http://dx.doi.org/10.1109/LICS.2012.75 > https://www21.in.tum.de/~traytel/papers/lics12-codatatypes/codat.pdf > > [S3] Reference in the e-mail written by Michael Norrish > "The chapters from the HOL book mentioned above are available as part of the > HOL4 system's documentation at: > > http://sourceforge.net/projects/hol/files/hol/kananaskis-10/kananaskis-10-logic.pdf/download > See §2.5.4 in particular for a discussion of how the system can be extended > with new types." > > The HOL System: LOGIC (November 6, 2014) > > http://sourceforge.net/projects/hol/files/hol/kananaskis-10/kananaskis-10-logic.pdf > > > Derived References (from [S1], pp. 260-263) > > [15] W. M. Farmer. The seven virtues of simple type theory. J. Applied Logic, > 6(3):267-286, 2008. > http://imps.mcmaster.ca/doc/seven-virtues.pdf > > [18] M. J. C. Gordon. HOL: A machine oriented formulation of higher order > logic. Technical Report 68, University of Cambridge Computer Laboratory, 1985. > > [50] A. Pitts. The HOL logic. In M. J. C. Gordon and T. F. Melham, editors, > Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, > pages 191-232. Cambridge University Press, 1993. > ISBN 0-521-44189-7 > > [57] M. Wenzel. Type classes and overloading in higher-order logic. In E. L. > Gunter and A. Felty, editors, Theorem Proving in Higher Order Logics: TPHOLs > '97, volume 1275 of Lecture Notes in Computer Science. Springer-Verlag, 1997. > http://www4.in.tum.de/~wenzelm/papers/axclass-TPHOLs97.pdf > > [22] F. Haftmann and M. Wenzel. Constructive type classes in Isabelle. In T. > Altenkirch and C. McBride, editors, Types for Proofs and Programs, TYPES > 2006, > volume 4502 of LNCS. Springer, 2007. > http://www4.in.tum.de/~wenzelm/papers/constructive_classes.pdf > > [27] O. Kuncar and A. Popescu. A consistent foundation for Isabelle/HOL. In > C. > Urban and X. Zhang, editors, Interactive Theorem Proving - 6th International > Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings, volume > 9236 of Lecture Notes in Computer Science. Springer, 2015. > http://www21.in.tum.de/~kuncar/kuncar-popescu-jar2016.pdf > http://andreipopescu.uk/pdf/ITP2015.pdf > > > Standard References > > Andrews, Peter B. (1986), An Introduction to Mathematical Logic and Type > Theory: To Truth Through Proof. Orlando: Academic Press. ISBN 0-12-058535-9 > (Hardcover). ISBN 0-12-058536-7 (Paperback). > > Andrews, Peter B. (2002), An Introduction to Mathematical Logic and Type > Theory: To Truth Through Proof. Second edition. Dordrecht / Boston / London: > Kluwer Academic Publishers. ISBN 1-4020-0763-9. DOI: > 10.1007/978-94-015-9934-4. > > Andrews, Peter B. (2014), "Church's Type Theory". In: Stanford Encyclopedia > of > Philosophy (Spring 2014 Edition). Ed. by Edward N. Zalta. Available online at > http://plato.stanford.edu/archives/spr2014/entries/type-theory-church/ (July > 2, > 2016). > > Church, Alonzo (1940), "A Formulation of the Simple Theory of Types". In: > Journal of Symbolic Logic 5, pp. 56-68. > > > Further References > > Kubota, Ken (2015), On the Theory of Mathematical Forms (draft from May 18, > 2015). Unpublished manuscript. SHA-512: a0dfe205eb1a2cb29efaa579d68fa2e5 > 45af74d8cd6c270cf4c95ed1ba6f7944 fdcffaef2e761c8215945a9dcd535a50 > 011d8303fd59f2c8a4e6f64125867dc4. DOI: 10.4444/100.10. See: > http://dx.doi.org/10.4444/100.10 > > Kubota, Ken (2015a), Excerpt from [Kubota, 2015] (pp. 356-364, pp. 411-420, > and > pp. 754-755). Available online at > http://www.kenkubota.de/files/R0_draft_excerpt_with_definitions_and_groups.pdf > > (January 24, 2016). SHA-512: 67a48ee12a61583bd82c286136459c0c > 9fd77f5fd7bd820e8b6fe6384d977eda 4d92705dac5b3f97e7981d7b709fc783 > 3d1047d1831bc357eb57b263b44c885b. > > ____________________ > > Ken Kubota > doi: 10.4444/100 > http://dx.doi.org/10.4444/100 > > ------------------------------------------------------------------------------ What NetFlow Analyzer can do for you? Monitors network bandwidth and traffic patterns at an interface-level. Reveals which users, apps, and protocols are consuming the most bandwidth. Provides multi-vendor support for NetFlow, J-Flow, sFlow and other flows. Make informed decisions using capacity planning reports. http://sdm.link/zohodev2dev _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
