| 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 a1ii 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).
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 milpgame1.1a.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.
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 ...".
(The following 3 paragraphs were added on 5-Feb-2020.)
If you want to find a rule that fits with the ENTERED statement and existing statements, you should follow these steps: Between the border of "Find the rules that fits", in the text pane you can enter the desired statement (you can check the correctness by clicking the "Syntax check" button), marked target must be null, enter the number of hypotheses that rule should have, select the first existing statements by clicking on it (label "Start with:" will show you the first selected statement from a list of ordered statements), then you can click on "Search and apply the rule". (If the number of hypotheses is 0 it is not necessary to have selected a first existing statement.)
If you just want to insert into the proof a new unproved statement, you should do the following: in the border of "Find the rules that fits", in the text pane you can enter the desired statement (you can check the correctness by clicking the "Syntax check" button); the marked target must be null then click on "Insert the above statement". (An unproved statement must be not be identical with a theorem hypothesis because it cannot be proved further, you just simply insert the theorem hypothesis.)
If you want to find a rule that fits with the MARKED target statement and existing statements you should do the following: click on desired target statement, click on "Mark the target" (the label "Marked that is:" will show the target statement), enter the number of hypotheses that rule should have, select the first existing statements by clicking (label "Start with:" will show you the first selected statement from a list of ordered statements), then you can click on "Search and apply the rule". (If the number of hypotheses is 0 it is not necessary to have selected a first existing statement.) After you enter a proof in forward strategy you can get the text version (similar to mmj2) of the proof by clicking on "Text version of the proof".
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 22-Mar-2021.
Copyright terms (for the text on this web page): Public domain |
W3C HTML validation [external] |