[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
SYSTEM ANNOUNCEMENT: PROOFWEB We are pleased to announce the availability of our ProofWeb system for teaching logic and using proof assistants through the web. For details go to the ProofWeb home page at: http://proofweb.cs.ru.nl/ Attached to this mail is the text on the ProofWeb home page. Cezary Kaliszyk Dan Synek Femke van Raamsdonk Freek Wiedijk Herman Geuvers James McKinna WHAT IS PROOFWEB? ProofWeb is both a system for teaching logic and for using proof assistants through the web. ProofWeb can be used in three ways. First, one can use the guest login, for which one does not even need to register. Secondly, a user can be a student in a logic or proof assistants course. We are hosting courses free of charge. If you are a teacher and would like to host your course on this server, send email to [EMAIL PROTECTED] Thirdly, if teachers do not want to trust us with their students' files, they can freely download the ProofWeb system and run it on a server of their own. LOGIC ON THE WEB ProofWeb is a system for practising natural deduction on the computer. It is almost, but not quite, entirely unlike the Jape system. ProofWeb is based on the Coq proof assistant and runs inside any modern web browser. To use ProofWeb one does not need to install software locally, not even a plugin: a web browser is all one needs. With ProofWeb one runs logic exercises on a web server, just like gmail keeps all mail messages on its server. This means that students will be able to access their exercises wherever they have a web browser, and that teachers at any time can see the status of their students' work. ProofWeb comes with a database of basic logic exercises that are graded according to difficulty. The ProofWeb system automatically grades the exercises of the students. To the students this is presented as a traffic light: their goal is to get a green light for all their exercises. A ProofWeb user talks to the Coq system on the server without any translation. There just are a few additional tactics to make Coq's behavior follow the logic textbooks. This means that in ProofWeb the full power of Coq is available, even to beginner students. On the other hand ProofWeb tries hard to present deductions exactly the way they look in the textbooks. In particular ProofWeb exactly follows the conventions of a well-known logic textbook, "Logic in Computer Science: Modelling and Reasoning about Systems" by Michael Huth and Mark Ryan, published by Cambridge University Press. For this reason ProofWeb is especially attractive for courses that use this textbook. ProofWeb both supports Gentzen-style natural deduction in which proofs look likes trees with the conclusion at the root, and Fitch-style natural deduction in which proofs consist of lines grouped together with boxes or "flags". PROOF ASSISTANTS ON THE WEB ProofWeb is a system that allows anyone to try out proof assistants without installing anything. It is almost, but not quite, entirely unlike the Proof General interface for proof assistants. ProofWeb was designed to be used with Coq, but the interface has been successfully extended to other proof assistants, and in particular it supports the Isabelle system. Although ProofWeb was designed for teaching logic to undergraduate computer science students, it also has been successfully used to teach proof assistant courses to graduate students. RELATED PROJECTS The ProofWeb interface has been used and extended in various projects. The main ones are a prototype by Cezary Kaliszyk and Pierre Corbineau of a system that combines ProofWeb with a mathematical encyclopedia in the style of Wikipedia, and PC-Extra, an arbitrary precision calculator by Cezary Kaliszyk, based on the PhD work of Russell O'Connor. ABOUT PROOFWEB ProofWeb was developed in 2006 and 2007 in the education innovation project "Web deduction for education in formal thinking" which was financed by Surf Foundation, the Radboud University Nijmegen and the Free University Amsterdam. The main developer of the system was Cezary Kaliszyk, after ideas by Freek Wiedijk. The ProofWeb exercise database and a first version of the natural deduction tactics were developed by Maxim Hendriks. ProofWeb was refined based on experiences with the system in courses given by Femke van Raamsdonk, Hanno Wupper and Roel de Vrijer.