Milpgame |

Milpgame is a proof assistant and a checker (showing an error message if something goes wrong) for the Metamath language. You can enter the demonstration (proof) either forward and backward relative to the statement to prove. Milpgame checks if a statement is well formed (the program has a syntactic verifier). You can save unfinished proofs without the use of the dummylink theorem. The demonstration is shown as a tree, and statements are shown using HTML definitions (defined in the $t typesetting comment of the database). Milpgame is distributed as a Java .jar (JRE version 6 update 24 written in NetBeans IDE).

Video tutorial no. 2 [retrieved 28-Feb-2018]

You can save unfinished proofs in *.mlp format, which
you can open later to complete the proof of the theorem or problem.

If you
enter on "Edit -> Search" and search for a theorem name, you can go to the
source of the theorem, and from there you can enter new proof.

Download milpgame0.6.zip, unzip it, and follow the instructions in readme.txt. For proving theorems using the current set.mm, download set.mm from Github/set.mm and open the file with Milpgame. System requirements: 2 GB of RAM and 1366x768 screen resolution.

- milpgame0.6.zip - Milpgame 0.6 Cross-platform (Windows, Linux, Mac OS)
- tests.zip - Optional test files (see below)
- instructions.txt - Text version of instructions

For help
and feedback send Filip an email at
milpgame@yahoo.com

Milpgame cannot modify set.mm. After you prove a theorem, you must paste the proof into set.mm manually using a text editor. Prior to the proving, you must add to set.mm the theorem to be proved, accompanied by an empty proof (that is, whose proof consists of the single character "?"), using a text editor.

After you start Milpgame, go to "File -> Open" and choose the set.mm file. (To play with test1 through test6, you must download one of the test.mm files and set04.06.2013.mm in the same folder and then Open the test.mm in Milpgame.)

When working with set.mm, Milpgame takes about 40 seconds to load, depending on your CPU.

Move the cursor to "Edit -> Search", check "Search by name", and enter the name of the theorem that you want to prove. From the list that appears, click on the desired theorem name and "Go" to the source. Then click on the theorem and click on "Edit this proof" (a new tab will appear).

There are two strategies for proving theorems, called Forward Chaining and Backward Chaining.

In the tab with theorem name on it, click "Change strategy" to change it to "Forward Chaining". This strategy allows you to enter the proof starting with the hypotheses and ending with the theorem statement.

In order to prove the theorem, you must fill the "List of Rules" with axioms, theorems and hypotheses. The "List of Rules" can be filled with axioms and theorems using "Edit -> Search". (You enter the name of axiom or theorem in the place holder, check "Search by name", and click on "Search". A list of results will appear. Choose the axiom or theorem, then click on "Add" to add it to the "List of Rules".)

Any hypotheses of the theorem to be proved are listed after the "Edit this proof" button. To add a hypothesis to the "List of Rules", click on the hypothesis then click on the "Add" button to add it to the "List of Rules" as "Hypothesis...".

In the following instructions, an axiom or theorem with no hypotheses is called "simple", and one that has hypotheses is called "complex".

To assign a hypothesis to the proof, you must in enter it into the "List of Rules" as described, click on the hypothesis, click "Select", then click on "Apply Rule: Hypothesis of ..."

To assign a simple axiom or simple theorem to the proof, you must enter it in the "List of Rules", click on the axiom [theorem], click "Select", then click "Apply Rule: Axiom [Theorem] of ...".

To move up or down through the hypotheses and statements, click on "Move Up" or "Move Down".

Undetermined variables are called "$v0", "$v1", etc. In order to fill in a variable (i.e. assign it to an expression), you must click on the statement with the variable, then click on "Edit proof variables". Fill in the variable with a desired expression that qualifies for the variable type (such as wff or class).

To add a simple or complex theorem or axiom to the proof, you must click on the statement, enter the "List of Rules", choose a theorem or axiom, then click on "Apply Rule: Theorem [or Axiom] of ...".

In the tab with theorem name on it, click "Change strategy" to change it to "Backward Chaining". This will allow you to enter the proof starting with the theorem statement and ending with the hypotheses.

To add a simple or complex theorem or axiom to the proof, you must click on the statement, enter the "List of Rules", choose a theorem or axiom, then click on "Apply Rule: Theorem [or Axiom] of ...".

The instructions are similar for the case of a hypothesis.

Undetermined variables are called "$v0", "$v1", etc. In order to fill in a variable (i.e. assign it to an expression), you must click on the statement with the variable, then click on "Edit proof variables". Fill in the variable with a desired expression that qualifies for the variable type (such as wff or class).

If you want to add an existing statement to the proof, click on "Add an existing statement". If you want to delete a branch, click on the statement that you want to delete and then click "Delete branch". The "Syntax" button is used to show the syntactic definitions for wff, class, and set variables. In the "Edit -> Formula" editor, you can create a statement using symbols (HTML definitions) and then obtain the corresponding ASCII result that can be used to edit set.mm (with a text editor).

This page was last updated on 30-Mar-2018.
Copyright terms (for the text on this web page): Public domain |
W3C HTML validation [external] |