HomePage RecentChanges

mmj2StepProver

Next mmj2 Release: Step Prover

ETA? 1-Apr-2009?

User-Design Doc

StepProverDoc.zip – documentation and untested source code for Step Prover (README.txt inside explains).

User-Design Doc Comments

1. The specification of the "givens" for the designated proof step is wrong. It says that an empty, ("" – null string), value in the step's Hyp field means "use the theorem's logical hypotheses as the Givens". Doing this would mean that there would be no way to specify zero Givens for the subproof. So, there are, again, just two options, a) specify a "?" designating all prior steps in the Proof Worksheet as Givens; and b) explicitly list the Givens, chosen from among the previous steps (e.g. "1,4,5").

2. It may not be clear, but the SearchWith? parameter is redundant unless a MaxSearchStmt? is specified and the assertion labels in the SearchWith? parameter are beyond the MaxSearchStmt? label. If the SearchWith? assertions are inside the MaxSearchStmt? range then there is no need to list them – they will be searched in the normal course of events. The purpose of SearchWith? is to list assertions to be used while also restricting the normal search for justifying assertions. Examples are, say lemmas, or new and improved theorems. It would be possible to specify a SearchMaxStmt? of "ax-1" – the first assertion, and to specify a "?" (all) in the Hyp field, designating all prior proof steps as Givens. Then the Step Prover would be forced to use just the SearchWith? theorem to reprove the designated step using the Givens and the SearchWith? assertion(s).

3. A strategy for using the Step Prover would be to prove a theorem bottom-up, which is the way Step Prover goes about the job, but to input a proof step above the step in progress and to specify it as a Given. This would mean that you know you can prove your formula if you can prove the previous step. The previous step can be input with a "?" in the Hyp field meaning "Incomplete Hypotheses", and need not itself be proven yet.

4. I reworked the order of the proof search for hypotheses of a given subproof step.

The original version (source uploaded with the user specs) created the children in the proof subtree in Reverse Polish order according to the order of the hypotheses in Assrt.logHypArray.

To speed up proof search the order used is now given by Assrt.sortedLogHypArray, (which is already loaded by mmj2 when the Assrt is loaded into LogicalSystem?,) and the steps are derived in Polish Prefix order (to simplify the code).

The sort sequence is descending order by formula length (number of Metamath math symbols), and in the case of a tie, the LogHyp? formula which has at least one variable in common with the Assrt.formula is first.

The only drawback to this approach is that when the CandidateProof? is output, the children of each subproof step must be "desorted" and output in RPN order. That adds a tricky bit of code :-)

The advantage is a very significant pruning of the search tree in the average case and a major disaster avoided (we hope) in the worst case scenario. Previous, mmj2 has used the sortedLogHypArray throughout the Proof Assistant unification search and StepUnifier? search. I didn't seriously consider using the sortedLogHypArray until I started thinking… Performance is expected to be dramatically not as bad as it would have been using unsorted hypotheses :-)