\documentclass[runningheads,envcountsame,envcountsect]{llncs}
\usepackage{amssymb,url,alltt,graphicx}
\raggedbottom

\begin{document}

\title{Practising logic through the web}
\author{Freek Wiedijk}
\institute{
Institute for Computing and Information Sciences \\
Radboud University Nijmegen \\
Toernooiveld 1, 6525 ED Nijmegen, The Netherlands}
\maketitle

\begin{abstract}
We present the ProofWeb system for practising
natural deduction in predicate logic and for remotely working with the
Coq proof assistant.
The ProofWeb system can be used for free, both for trying it out
as a guest
as well as for hosting computer labs for logic
and proof assistant courses, on the Nijmegen ProofWeb server
\url{http://proofweb.cs.ru.nl/}.
\end{abstract}

\subsection*{A computer lab for a logic course}

Suppose you are a lecturer at a computer science department
who has to teach the introductory logic course.
That course teaches natural deduction in three standard logics:
\begin{itemize}
\item
Propositional logic
\item
Predicate logic
\item
Predicate logic with equality
\end{itemize}
\noindent
You would like the computer to be used by your students
for their logic exercises.
What should you use?

In the Netherlands many of these courses currently use the Jape system
from the UK \cite{bor:suf:96}.
It allows students to check simple deductions with a computer program
that has a pleasant point-and-click interface.
However, the Jape system has restrictions.
It is not possible to save an unfinished deduction and later continue
working on it.
It is not possible to have types for variables.
It is not possible to reason about time in the deductions, or to reason arithmetically
in other contexts for that matter.
This all makes the use of Jape inconvenient for larger examples.
Also, with Jape there is no easy way to run a course in an centrally organized manner.
Each student has to install Jape on their own system, it is
hard to keep track of what the students are doing with it, and grading
students' work is labor intensive.

Here we present the ProofWeb system, as a better system to be used for computer labs for logic courses.
ProofWeb was developed as a joint effort between the Radboud University Nijmegen and the Free University
Amsterdam, in a small education innovation project funded by the Surf Foundation called \emph{Web-deductie voor het onderwijs in formeel denken}.
ProofWeb already has been, and still is, used in about a dozen logic courses in various
universities.

\subsection*{The Coq proof assistant as a web application}

Proof assistants are systems for developing and checking deductions
on the computer.
These systems are both used for verification of the correctness
of software and hardware, as well as for checking the correctness of mathematics.
There are several proof assistants to choose from
(important examples are PVS, HOL, Isabelle, ACL2, The B Method,
Twelf, and in some sense even Jape).
One of the best proof assistants currently
available is the Coq system developed at INRIA in France \cite{coq:08,ber:cas:04}.
Coq has been used for many impressive projects, like the validated
Compcert C compiler which compiles a large subset of C to assembly
for the PowerPC family of processors, getting a performance similar
to the gcc compiler with the first level of optimization turned on \cite{ler:06,bla:dar:ler:06},
and the formal proof of the Four Color Theorem by Georges Gonthier \cite{gon:06}.

Before the ProofWeb project, Henk Barendregt had for a long time already
been asking for a web interface
to the Coq system, to allow people to work with Coq
without first having to go through the trouble of installing it
on their computer.
There had been a project in which mathematicians from Russia were supposed
to contribute (they would be paid a fixed price for each lemma proved),
but before they had Coq running correctly on their systems the project already was
over.
If a Coq environment had been available on the web this might have
gone differently.
But Henk wanted a web interface to Coq for a more ambitious goal:
to have the whole world help with encoding all
of mathematics in Coq.
This would be an important step to make
that come about.

Cezary Kaliszyk, one of the PhD students in Henk's group in Nijmegen,
happened to be an expert on Web interfaces.
His PhD research was on making proof assistants more friendly,
but his master's thesis had been about Web interfaces.
When he heard about Henk's wish, in a Christmas holiday he whipped
together a simple but nice web interface to the Coq system.
This interface later was extended into the ProofWeb system.
Although various people were involved in that project,
Cezary remained the sole developer of the system.

\subsection*{The ProofWeb system}

The ProofWeb system has the following distinctive properties:
\begin{itemize}
\item
With ProofWeb the students work with the Coq proof assistant.
Their input is not being pre-processed by the ProofWeb interface;
i.e., the text that ProofWeb users are typing are actual Coq proof scripts.
With ProofWeb the students are working
with an industrial strength interactive theorem prover, with the
full power of that system available to them from the start.

\item
ProofWeb shows deductions in a style that matches as closely as
possible the deductions the way they are presented in elementary
logic courses.
Although ProofWeb shows the Coq presentation of the state
of the proof, there is also a display that really looks like the
diagrams from logic textbooks.
In fact, the ProofWeb system intentionally was made fully compatible
with a good logic textbook:
\emph{Logic in Computer Science: Modelling and Reasoning about Systems} by Michael Huth and Mark Ryan \cite{hut:rya:04}.
If a course uses this book then ProofWeb is a good choice for the lab work of that course.
And if a course wants to use ProofWeb for the lab work, then this book is a good
textbook to be used for the non-computer part of the course.

\item
ProofWeb comes with an extensive manual \cite{kal:raa:wie:wup:hen:vri:08} that both summarizes natural
deduction for predicate logic and presents all the details of
working with the ProofWeb system.
This manual can be downloaded as a PDF file from the ProofWeb web site.

\item
ProofWeb comes with a collection of more than a hundred
simple logic exercises
to be worked with the ProofWeb system.
Courses can have their own set of exercises, but
this set is a good default choice for an introductory logic course.

\item
To use ProofWeb there is no need to install special software.
In fact ProofWeb does not even use a plug-in.
All that one needs is a compatible web browser.
ProofWeb users can access ProofWeb from anywhere on the internet.
(For example, if necessary, students might go into an internet caf\'e to finish their
homework.)

\item
ProofWeb has good interfaces for both students and teachers to
manage their courses.
Students will see a list of exercises, and the status of these
exercises.
Teachers will see a list of students, and the status of those
students.

\end{itemize}

\subsection*{ProofWeb for teaching Coq}

ProofWeb can be used for teaching logic to undergraduate students,
but it also can be used for teaching proof assistants to graduate
students.
In fact, about half of the current ProofWeb courses are
type theory courses that teach the Coq system.

In such courses the exercises do not have the shape of having
to prove a single first order formula.
Instead they are long files with many lemmas, where
the students have to fill in the proofs of those lemmas.
Generally students then will have to complete one such an exercise per
week.

\subsection*{Fitch-style natural deduction}

There are two styles of presenting natural deduction proofs on paper.
The more commonly taught style was introduced by Frederic Fitch.
These proofs consists of lines that are grouped together either by
boxes around them or by having `flags' with assumptions in
the margin.
(Using flags is typical of the way this kind of proof is
taught at the Technical University of Eindhoven.
This style originated in the Automath project from the sixties and seventies.)

Fitch-style proofs are the style of natural deduction presented in
the book by Huth and Ryan that ProofWeb especially was designed to
match.
However, Fitch-style proofs do not exactly have the structure
of Coq proofs.
For this reason, in the ProofWeb project one of the major difficulties
was to get Fitch-style deduction to work well with the Coq system \cite{kal:wie:09}.

Here is a Fitch-style proof as shown in ProofWeb:
\def\mbar{\multicolumn{1}{|l}{}}
\let\green=\relax
\setlength\tabcolsep{.5em}
\begin{center}
\tt
\strut\hspace{-4em}%
\label{proof:fitch:proofweb}%
\begin{tabular}{rlllllll}
\cline{2-7}
1 & \mbar &&& \green{H1:} & $\exists$x, (P x $\lor$ $\neg$Q a) & assumption & \\\cline{3-7}
2 & \mbar & \mbar && \green{H2:} & Q a & assumption \\
\cline{4-7}
& \mbar & \mbar & \mbar & b \\
3 & \mbar & \mbar & \mbar & \green{H3:} & P b $\lor$ $\neg$Q a & assumption \\
\cline{5-7}
4 & \mbar & \mbar & \mbar & \multicolumn{1}{|l}{\green{H4:}} & P b & assumption
\\
5 & \mbar & \mbar & \mbar & \mbar & $\exists$x, P x & $\exists$i 4 \\
\cline{5-7}
6 & \mbar & \mbar & \mbar & \multicolumn{1}{|l}{\green{H5:}} & $\neg$Q a & assumption \\
7 & \mbar & \mbar & \mbar & \mbar & $\bot$ & $\neg$e 6,2 \\
8 & \mbar & \mbar & \mbar & \mbar & $\exists$x, P x & $\bot$e 7 \\
\cline{5-7}
9 & \mbar & \mbar & \mbar && $\exists$x, P x & $\lor$e 3,4-5,6-8 \\
\cline{4-7}
10 & \mbar & \mbar &&& $\exists$x, P x & $\exists$e 1,3-9 \\
\cline{3-7}
11 & \mbar &&&& Q a $\to$ $\exists$x, P x & $\to$i 2-10 \\
\cline{2-7}
12 &&&&& $\exists$x, (P x $\lor$ $\neg$Q a) $\to$ Q a $\to$ $\exists$x, P x & $\to$i 1-11
\end{tabular}%
\hspace{-4em}\strut
\end{center}
\medskip
\noindent
When doing the proof, this picture will be growing in the
lower-right pane of the ProofWeb window.
Here is what the ProofWeb interface looks like halfway down
a simpler example:
\begin{center}
\smallskip
\includegraphics[width=.8\textwidth]{shot_10.eps}
\smallskip
\end{center}
\noindent
Both the Coq view of the proof as well as the textbook
display of the proof are present simultaneously.
To our surprise when working on exercises like this,
students mostly completely
ignored the Coq proof state in the upper-right pane and just looked at the lower-right.

\subsection*{Gentzen-style natural deduction}

The other style of natural deduction that is
commonly used was introduced by Gerhard Gentzen.
This is the style that is used in the textbook
\emph{Logic and Structure} by Dirk van Dalen \cite{dal:04}.
(ProofWeb is not completely compatible with this book --
we decided that internal consistency was important, so
we had our Gentzen-style proof display be influenced by
the Huth and Ryan conventions -- but it comes very close.)

In the
case of Gentzen-style natural deduction the proofs look like trees, growing upward from the
statement that is proved.  When doing this kind of proof
on paper one generally gets space problems fast, but in
a computer one does not have this problem, as in that case one
has scroll bars.

Here is the same example proof, but this time presented in Gentzen
style:
\def\third#1{\hbox{\vbox to 0pt{\vspace{.15em}\hbox{#1}\vss}}}
\begin{center}\tt
\medskip
\strut\hspace{-4em}%
\begin{tabular}{ccclcl}
&&&& [$\neg$Q a]$^{\green{\tt H5}}\;$ [Q a]$^{\green{\tt H2}}$ & \third{$\neg$e} \\
\noalign{\vspace{.5\smallskipamount}}
\cline{5-5}
\noalign{\vspace{.5\smallskipamount}}
&& [P b]$^{\green{\tt H4}}$ & \third{$\exists$i} & $\bot$ & \third{$\bot$e} \\
\noalign{\vspace{.5\smallskipamount}}
\cline{3-3}\cline{5-5}
\noalign{\vspace{.5\smallskipamount}}
& [P b $\lor$ $\neg$Q a]$^{\green{\tt H3}}$ & $\exists$x, P x && $\exists$x, P x & \third{$\lor$e\green{[H4,H5]}} \\
\noalign{\vspace{.5\smallskipamount}}
\cline{2-5}
\noalign{\vspace{.5\smallskipamount}}
\strut[$\exists$x, (P x $\lor$ $\neg$Q a)]$^{\green{\tt H1}}$ && $\hspace{1.6em}${}$\exists$x, P x$\hspace{-1.6em}$ &&& \third{$\exists$e\green{[H3]}} \\
\noalign{\vspace{.5\smallskipamount}}
\cline{1-5}
\noalign{\vspace{.5\smallskipamount}}
& $\hspace{2.5em}${}$\exists$x, P x$\hspace{-2.5em}$ &&&& \third{$\to$i\green{[H2]}}\\
\noalign{\vspace{.5\smallskipamount}}
\cline{1-5}
\noalign{\vspace{.5\smallskipamount}}
& $\hspace{2.5em}$Q a $\to$ $\exists$x, P x$\hspace{-2.5em}$ &&&& \third{$\to$i\green{[H1]}} \\
\noalign{\vspace{.5\smallskipamount}}
\cline{1-5}
\noalign{\vspace{.5\smallskipamount}}
& $\hspace{-2.5em}${}$\exists$x, (P x $\lor$ $\neg$Q a) $\to$ Q a $\to$ $\exists$x, P x$\hspace{-8.5em}$ \\
\end{tabular}%
$\hspace{-8em}$
\end{center}
\medskip
\noindent
The ProofWeb code that generated both proofs (which just are different displays
of the same proof) was:
\let\red=\relax
\begin{quote}
\def\\{\char`\\}
\def\{{\char`\{}
\def\}{\char`\}}
\begin{alltt}
\red{Require Import ProofWeb.\medskip
Variable P Q : D -> Prop.
Variable a : D.\medskip
Theorem example :
  exi x, (P(x) \\/ ~Q(a)) -> Q(a) -> exi x, P(x).
Proof.
\green{imp_i H1.
imp_i H2.
exi_e (exi x, (P(x) \\/ ~Q(a))) b H3.
exact H1.
dis_e (P(b) \\/ ~Q(a)) H4 H5.
exact H3.
exi_i b.
exact H4.
fls_e.
neg_e (Q(a)).
exact H5.
exact H2.}
Qed.}
\end{alltt}
\end{quote}
\noindent
This is an actual Coq input script.
The commands occurring in this script can be selected from menu's in the ProofWeb
interface, so the students do not need to know these commands by heart.
Also, these commands are extensively explained in the ProofWeb manual.

\subsection*{The student's view of ProofWeb}

When a student follows a course that uses the ProofWeb system,
he or she will go to the ProofWeb server that hosts the course.
The student will then select the course from a menu,
login in to the system by entering username and password,
and then will be presented with the list of exercises:
\begin{center}
\smallskip
\includegraphics[width=.8\textwidth]{shot_17.eps}
\smallskip
\end{center}
Each exercise will have four possible statuses, which are color
coded:
\begin{center}
\begin{tabular}{ll}
Gray & Not touched \\
Red & Incomplete \\
Orange & Correct \\
Green & Solved
\end{tabular}
\end{center}
\noindent
The goal for the student will be to work the exercises until the traffic lights in his list are all green.
(The orange status means that the proof is correct,
but that the student used proof steps that are not allowed for the course.
For example Coq's powerful automation will not be allowed when doing exercises in
elementary logic.)

\subsection*{The teacher's view of ProofWeb}

The teacher can login for the course too, but with the teacher's
interface.
He or she then will be presented with a table that lists all the students,
with for each student a count of how many of that student's
exercises there are of each of the four different colors.
The teacher also can login as if he were a specific student, to
grade exercises or maybe help the student with finding a solution.

Apart from this, the teacher interface also allows the teacher to
add student logins or change passwords.
Finally there is a button for downloading all files for the course
as a big tar file, for archival purposes at the end of a course.

\subsection*{The MathWiki project}

ProofWeb was primarily developed for logic education,
but in Nijmegen we have more ambitious goals for it.

Recently, the project \emph{MathWiki: a Web-based Collaborative Authoring
Environment for Formal Proofs} was funded in NWO's {vrije competitie},
to develop a system to be called MathWiki.
This system will be a cross between a Wikipedia for mathematics,
and the system that Henk was dreaming of where all the world would
help build a Coq version of all of mathematics.
An aspect of the MathWiki project is that it is not supposed to be just
about the Coq proof assistant.
Eventually many proof assistants will be available through our interface.

A prototype of MathWiki already was developed and a web page about this
work can be found on the ProofWeb server.

\subsection*{Trying it?}

If you want to try ProofWeb: it is completely free.
Currently there are three way of using the system:
\begin{itemize}
\item
First you can access it as a guest user.
For this you do not even need to register.
Just click the Guest login button.
It is probably useful to first look through the ProofWeb manual
to know what to do next.

\item
Second you can host courses on the Nijmegen ProofWeb server.
For this, just send an email message to \url{proofweb@cs.ru.nl}.

\item
Third, you might not trust someone else with your students' data.
In that case you might download the ProofWeb server and install
it on a machine of your own.
At the moment this has not been done much,
and you will probably need some help from Nijmegen with
that,
which of course we will be happy to provide.

\end{itemize}
\noindent
We hope ProofWeb will be useful both for logic teaching, as well as
for exposing more students to proof assistants.
If you have any questions about ProofWeb, just send mail to
\begin{center}
\url{proofweb@cs.ru.nl}
\end{center}
Or you should surf to
\begin{center}
\url{http://proofweb.cs.ru.nl/}
\end{center}
and take a look for yourself at the system that we developed.

\bibliographystyle{plain}
\bibliography{frk}

\end{document}