An Example Naproche Session

The following example session with screenshots was carried out with an early NAPROCHE version programmed in SWI-Prolog, running under Suse-Linux and TeXmacs.

Start up the TeXmacs editor with the NAPROCHE plugin. The header line of TeXmacs will contain a "Proof-Checker" button. When pressed, it initiates proof checking of the current buffer.

Plain text editing with TeXmacs proceeds in the usual way. The mathematical mode is obtained by typing a $-sign. Mathematical symbols like α can be entered by using the standard LaTeX commands and pressing <enter>. So ∖a l p h a and <enter> produces an α.

 

A logical "and" (∧) can typed as ∖w e d g e or obtained with one mouse-click from the symbol menues provided in the mathematical mode, in this case from the menue denoted by ℘ .

One can leave the mathematical mode by leaving the blue box around the mathematical text using the right-arrow keys (→) or by typing another $-sign.

The text typed so far is treated as a comment by the proof-checker. Only text in the quotation environment is proof-checked. The quotation environment is available by typing <\quotation> (i.e., ∖q u o t a t i o n <enter>), or by using the menues Text > Environment > Quotation. Writing inside the quotation environment is possible just like outside.

There are various editing tools like copying text by marking it with the mouse and pasting it by ctrl-y or by klicking the middle mouse button.

The proof of the De Morgan equivalence proceeds in the standard way. Assume the left-hand side of the equivalence in order to obtain the right-hand side. A proof by contradiction may be initiated by "Assume for a contradiction that". Assumptions can be freely introduced in a proof. Note that the status line usually shows the internal state of the editor.

The status line is also used by the NAPROCHE system for the two possible messages of the checker: "The proof is accepted" and "The proof is NOT accepted". So if one presses the Proof-Checker button now, the proof will be accepted, since the proof so far only consisted of the introduction of assumptions.

If we introduce an (orthographical) mistake into the proof like starting a sentence with a small letter, the proof checker rejects the proof.

So we correct the spelling mistake and continue the proof by assuming ¬α. Then α can be deduced from the assumption α∧β, and a contradiction can be deduced from the ¬α and α.

This is vindicated by the proof-checker:

This means that the last assumption implies a contradiction. This conclusion is expressed by the keyword "Thus":

We proceed similarly for β:

So each case of the disjunction ¬α∨¬β leads to a contradiction. So the converse ¬(¬α∨¬β) of the last open assumption holds. This consequence is also indicated by a "Thus".

Another application of "Thus" shows the left-to-right direction of the equivalence.

A "Qed." requires checking the last open theorem against the statements established so far. Since the left-to-right implication does not imply the equivalence, the proof ended by "Qed." at this point is rejected.

  Thus we remove the "Qed." and start the converse direction:

To prove α∧β from this assumption, one assumes ¬α and uses rules of ∨-introduction and contradiction. Similarly one obtains β.

α and β may be conjoined by ∧-introduction, and one gets the right-to-left implication.

Now we can close the proof by "Qed." since → and ← imply ↔︎.