### PCP: Point and Click Proofs

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