[TYPES/announce] System Announcement: ProofWeb

[Freek Wiedijk]

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 proofweb at cs.ru.nl.  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.