[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: QED-like <qed@mcs.anl.gov>, coq-club@pauillac.inria.fr, info-hol@jaguar.cs.byu.edu, isabelle-users@cl.cam.ac.uk, imps@hygelac.cas.mcmaster.ca, nuprllist@cs.cornell.edu, pvs@csl.sri.com, nqthm-users@cs.utexas.edu, nuprl@cs.cornell.edu*Subject*: Re: A question*From*: Piotr Rudnicki <piotr@cs.ualberta.ca>*Date*: Wed, 24 Jul 2002 00:01:00 -0600*Sender*: pvs-owner@csl.sri.com*User-Agent*: Mutt/1.2.5.1i

Hi: In my question posted a few days ago I was asking for information about formalization of any substantial chunk of mathematics formally checked but I never defined what such a chunk is. I indicated that I was most interested in books or parts of books that were originally meant for human consumption. I got quite a number of answers for which I would like to thank. Most of the answers concerned relatively isolated developments even if they covered advanced material. Of the books or part of books having the nature of mathematical monographs that were formalized I have only the following: - In the 1970's L. S. Jutting formalized Landau's {\em Grundlagen der Analysis} in de Bruijn's AUTOMATH system. The same material was then covered by Udding in a way directly written for Automath. - D. L. Simon in his 1990 PhD thesis at University of Texas at Austin checked {\em The elementary theory of numbers} by Leveque using the Boyer-Moore prover. - J. Siekmann's group from Saarbr\"{u}cken started checking D\"{u}ssen's {\em Halbgruppen und Automaten} in the MKRP prover in the 1980's. - Shang-Ching Chou: Mechanical Geometry Theorem Proving, D. Reidel Publishing Company, 1987 supposedly tries to formalise Euklid's Elements but I could not lay my hands on the book yet. - L.~C.~Paulson and K.~Gr\c{a}bczewski reported on the Isabelle formalization of most of Chapter I of Kunen's {\em Set Theory} and two first chapters of Rubin and Rubin, {\em Equivalents of the Axiom of Choice}. - T. Nipkow formalized in Isabelle/HOL the first 100 pages of Winskel's {\em The Formal Semantics of Programming Languages}. - Compendium of continuous lattices in Mizar. I am also aware of some formalizations under way in Nijmegen. I am sure that there are more efforts of the kind I am looking for, so should you know another one, please let me know. Thanks, -- Piotr Rudnicki CompSci, University of Alberta, Edmonton, Canada email: piotr@cs.ualberta.ca http://web.cs.ualberta.ca/~piotr

- Prev by Date:
**PVS 3.0 Beta** - Next by Date:
**Executing PVS** - Prev by thread:
**PVS 3.0 Beta** - Next by thread:
**Executing PVS** - Index(es):