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
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