###
**PCP:
**
**P**oint and
**C**lick **P**roofs

Peter
Jipsen, 2001-2003
This is the home page for the interactive "Point and Click Proof"
(PCP) environment that allows the investigation of
algebraic theories, such as groups, rings, lattices
and others. Here are some brief instructions on how to use the system, as
well as some description of the details.

Implementing quasi-equational logic on the web
Talk given at the AMS Sectional Meeting, University of South Carolina,
March 16-18, 2001.

The PCP system has a number of
features that make it suitable for use in undergraduate algebra courses,
and for general presentation of formal proofs on the web: specifically PCP

- has a proof structure that is similar to informal proofs
- produces proofs that are annotated by the names of the axioms
- uses fairly standard mathematical notation for output
- has an interface that is simple and allows only the application of valid
rules
- requires only occasional keyboard input in a simple ascii notation
- is implemented entirely in JavaScript and works with Netscape 4.5 or
Internet Explorer 5 (or later versions)
- integrates easily with webpages about the theories under investigation
- is very compact (~1000 lines of code)
- has a simple model to represent proofs and partial proofs
- is extendible to interact with automated theorem provers

In particular, PCP does not find proofs automatically. The user has
to choose which rule/axiom to apply at each point, so
finding a proof requires strategy and insight. PCP assists by
recording proof steps and avoiding mistakes.
Although the parser can read and write a wide range of mathematical
expressions (in a simplified TeX notation) which includes first
order logic and set theory,
PCP is currently restricted to a fragment of first order logic to
allow a simple interface and get some experience with this approach
of representing formal proofs. Specifically it can handle proofs
in quasi-equational theories, i.e. collections of universally
quantified implications between conjunctions of atomic formulas.

PCP is currently still under development, but already quite useful.
Of course there are several known problems (e.g. on Unix systems the
symbols are shown in their ascii form) and probably many
undiscovered bugs. No claims about soundness or completeness are made
for the current version. Please let me know if
you notice any problems or have suggestions for improvements.

Future extensions may include

- viewing proofs at several levels of detail
- replaying proofs to show the dynamic structure
- producing output in the linear proof style popular in CS
- extending to first order and higher order logics