The EPGY Theorem Proving Environment

Program Demonstrations

One way we help students learn to use our software is by providing them with AVI movies depicting useful tools. The following movies were designed to illustrate various tools available in the program. They may also serve, however, to give some impression of how the system looks and feels.

• Expand by Definition (646kB)
• Derivation System Introduction (1,977kB)
• The conditional proof strategy (1,499kB)
• The biconditional proof strategy (1,557kB)
• The "proof by contradiction" strategy (1,1413kB)
• The "proof by cases" strategy (1,656kB)
• Universal generalization in the backwards direction (1,1025kB)
• Existential generalization in the backwards direction (878kB)
• Universal generalization in the forwards direction (892kB)
• Existential generalization in the forwards direction (550kB)
• Universal instantiation (822kB)
• Existential instantiation (541kB)
• Renaming a bound variable (748kB)

The above movies are all in the AVI format. We recommend that you download them and play them with your favorite movie viewer. All these movies require the Techsmith Screen Capture Codec in order to play properly. We recommend the Camtasia Player (also from Techsmith) as a viewer for our movies.