The PCP system splits the browser window vertically into two frames. The left frame contains the (partial) proof, and the narrower right frame contains the possible choices available for the next step.
Initially the proof frame contains a list of axioms and formulas to be proved, with the latter preceded by a line of the form ...^...v...
This line indicates a gap in a proof and the two arrow symbols point at the line above and below the gap respectively. Each symbol is a button that can be clicked to direct the focus of subsequent actions to that line of the proof. The line with the current focus has an undo button instead of one of the arrow symbols, and also a hide/show button.
The undo button deletes the focus step of the proof (although main level proof steps cannot be undone presently).
The hide/show button allows subproofs and other gaps to be hidden so that the user can focus on the part of the proof that is currently of interest.
Each proof step is numbered, and subproofs are numbered like subsections in a book. Proof steps with a numbered button correspond to a rule which can be applied at the current focus step.
Clicking a numbered button (which does not correspond to a gap) applies the rule and produces in the choose frame a list of possible expressions (perhaps none) to be inserted at the focus. In some case one may need to apply a substitution to the possible expressions. Variables are substituted by terms that have to be typed in a fairly natural ascii syntax (e.g. x ^^ (y vv x), spaces are optional; ^^ is the meet symbol, ^ is for superscripts, vv is the join symbol, v is a variable). A more complete description of the syntax for formulas is in preparation. A look at the HTML source of the main frame of a PCP proof page may be helpful.
Selecting one of these expressions modifies the proof at the focus. If the focus was above the gap, the rule is applied in a forward reasoning fashion. If the focus is below the gap, each conjunct of the selected expression that still needs to be proved is inserted with a new gap above it.
Clicking a numbered button of a gap inserts a new subproof. The type of the subproof depends on what expression is below the gap:
proofHeader="\ <b>Proposition:</b> Every semilattice is a meet-semilattice.<br>\ <b>Proof:</b><br>"; currentProof=[ {expr:"x*y*z=x*(y*z)", axiom:true, name:"associativity"}, {expr:"x*y=y*x", axiom:true, name:"commutativity"}, {expr:"x*x=x", axiom:true, name:"idempotence"}, {expr:"x<=y iff x*y=x", axiom:true, name:"leq definition"}, {expr:"...", gap:true}, {expr:"x<=x", name:"reflexivity"}, {expr:"...", gap:true}, {expr:"x<=y and y<=x implies x=y", name:"antisymmetry"}, {expr:"...", gap:true}, {expr:"x<=y and y<=z implies x<=z", name:"transitivity"}, {expr:"...", gap:true}, {expr:"x*y<=x", name:"lower bound"}, {expr:"...", gap:true}, {expr:"x*y<=y", name:"lower bound"}, {expr:"...", gap:true}, {expr:"z<=x and z<=y implies z<=x*y", name:"infimum"} ]; parseProof(currentProof);
A functioning PCP webpage (like PCPsemilattices.html) contains the initial partial proof, and also requires the two frame pages PCPproof.html and PCPchoose.html (which remain the same for all PCP webpages).