What is a proof?
In the DC Proof system, a proof is just a numbered sequence of statements, each of which may be either true or false. They are displayed on the DC Proof Main Screen ─ the screen you will see when you first startup DC Proof:
Fig. 1 Sample proof from Example 1 of tutorial
Here we have a simple 5-line proof. In the following tutorial, the meaning of each symbol here will be explained in detail. For now, simply notice the overall layout of a proof as displayed on the Main Screen shown above (Fig. 1).
Statements are shown here in a black font. To the left of each statement is a line number. Below each statement in a gray, slightly smaller font are the rule and line number references used to generate that statement. You may be able to guess their meaning. The first line of this proof, for example, was generated using the Premise Rule. The second and third lines were generated using the Split rule applied to line number 1.
Each proof begins with one or more initial assumptions (or premises) ─ statements that are assumed to be true. In the following tutorial, you will learn how to enter a premise using the Premise form:
Fig. 2 The Premise form from Example 1 of tutorial
The Premise form will verify the syntax of the statement you enter in the textbox and append it to the proof on the Main Screen.
From these initial premises, you will be able to generate (or infer) other statements using the rules and axioms that are built into the DC Proof program, e.g. the Split, Join and Conclusion rules as shown above (Fig. 1). In the following tutorial, you will learn how to use these and all other rules and axioms in DC Proof.
Tutorial Format
The following tutorial consists of ten examples of relatively simple proofs. At the top of each new page is a reminder of what we are trying to prove and the statements we have generated so far.
Fig. 3 Sample heading in tutorial from Example 1
At the end of each example are one or more exercises to test your understanding. Hints and full solutions are provided for each exercise (also found in the DC Proof / Samples directory).