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

*To*: QED-like <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*: A question (sorry if repeated)*From*: Piotr Rudnicki <piotr@cs.ualberta.ca>*Date*: Wed, 17 Jul 2002 16:41:51 -0600*Sender*: pvs-owner@csl.sri.com*User-Agent*: Mutt/1.2.5.1i

Hi: On April 25 I posted the following question to qed@mcs.anl.gov: Grzegorz Bancerek and I are writing a sort of half-way report on the formalization of "A Compendium of Continuous Lattices" in Mizar. Another effort that (I am aware of) of formalizing an entire book is Jutting's formalization of Landau's "Grundlagen der Analysis" in AUTOMATH in the 70's. Does anybody know about other efforts on formalizing an entire book? To my surprise - the answer was that essentially "no". The responses that I got are summerised in the paragraph attached below. I would like to repeat my question not asking necessarily for a complete book anymore but any SUBSTANTIAL chunk of mathematics formally checked. Now, what is such a chunk? Hard to say but it should be foundational work, without assuming convenient facts when needed. Books or parts of books would be best. Thanks in advance, -- Piotr Rudnicki CompSci, University of Alberta, Edmonton, Canada email: piotr@cs.ualberta.ca http://web.cs.ualberta.ca/~piotr ------------------------- In the past, there were some attempts to formalize entire mathematical books in computerized proof-checking systems. The best known example was done in the 1970's when L.~S.~Jutting formalized Landau's {\em Grundlagen der Analysis} in de Bruijn's AUTOMATH system (see ~\cite{JUTTING,LANDAU,AUTOMATH}). We are sure that in other proof assistants, people have been undertaking similar efforts of formalizing mathematical books, but we are aware of only two partially completed attempts: 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, and in the 1980's, J.~Siekmann's group from Saarbr\"{u}cken started checking D\"{u}ssen's {\em Halbgruppen und Automaten} with the help of the MKRP prover.

- Prev by Date:
**Call for Participation: ISSRE 2002 Student Program** - Next by Date:
**PVS 3.0 Beta** - Prev by thread:
**Call for Participation: ISSRE 2002 Student Program** - Next by thread:
**PVS 3.0 Beta** - Index(es):