See also:

Proof Assistant User Guide

ProofAssistantGUIQuickHOWTO.html

ProofAssistantGUIDetailedInfo.html

ProofAssistantGUIDeriveFeature.html

StepUnifier.html

PageLocalRef.mmp

WorkVariables.html

StepSelectorSearch.html

BottomUpProving-ByNormMegill.html

To properly explain why someone would wish to perform this function, the best source is the inventor, Norm Megill. What follows is stolen from the Asteroid Meta wiki

`mmj2ProofAssistantFeedback.html`

webpage.Feedback: unification lockups

(This is a general mmj2 issue, not related specifically to the beta.)

Suppose we are developing a proof and have gotten to this point:

` $( <MM> <PROOF_ASST> THEOREM=xxx LOC_AFTER=?`

1::ax-1 |- ( &W1 -> ( &W2 -> &W1 ) )

2::ax-2 |- ( ( &W7 -> ( &W4 -> &W7 ) )

-> ( ( &W7 -> &W4 ) -> ( &W7 -> &W7 ) ) )

3::ax-1 |- ( &W7 -> ( &W4 -> &W7 ) )

4:3,2:ax-mp |- ( ( &W7 -> &W4 ) -> ( &W7 -> &W7 ) )

5::ax-2 |- ( ( ( &W7 -> &W4 ) -> ( &W7 -> &W7 ) )

-> ( ( ( &W7 -> &W4 ) -> &W7 )

-> ( ( &W7 -> &W4 ) -> &W7 ) ) )

6:4,5:ax-mp |- ( ( ( &W7 -> &W4 ) -> &W7 )

-> ( ( &W7 -> &W4 ) -> &W7 ) )

qed:?: |- ( ( ph -> ps ) -> ( ( ch -> ph ) -> ( ch -> ps ) ) )

$)

Then we realize, oops, step 4 should be "4:2,3:ax-mp" and not "4:3,2:ax-mp". But after we make this correction, the proof is "stuck" because the work variables now have the wrong patterns.

If we ctrl-z all the way back, which could have been a long time ago, we will lose all the work we did in the meantime.

On the other hand, if we completely erase the proof's formulas by hand:

$( <MM> <PROOF_ASST> THEOREM=xxx LOC_AFTER=?

1::ax-1

2::ax-2

3::ax-1

4:2,3:ax-mp

5::ax-2

6:4,5:ax-mp

qed:?: |- ( ( ph -> ps ) -> ( ( ch -> ph ) -> ( ch -> ps ) ) )

$)

then press ctrl-u, everything is magically corrected to exactly what I want to see:

$( <MM> <PROOF_ASST> THEOREM=xxx LOC_AFTER=?

1::ax-1 |- ( &W1 -> ( &W2 -> &W1 ) )

2::ax-2 |- ( ( &W3 -> ( &W4 -> &W5 ) )

-> ( ( &W3 -> &W4 ) -> ( &W3 -> &W5 ) ) )

3::ax-1 |- ( ( ( &W3 -> ( &W4 -> &W5 ) )

-> ( ( &W3 -> &W4 ) -> ( &W3 -> &W5 ) ) )

-> ( &W6

-> ( ( &W3 -> ( &W4 -> &W5 ) )

-> ( ( &W3 -> &W4 ) -> ( &W3 -> &W5 ) ) ) ) )

4:2,3:ax-mp |- ( &W6

-> ( ( &W3 -> ( &W4 -> &W5 ) )

-> ( ( &W3 -> &W4 ) -> ( &W3 -> &W5 ) ) ) )

5::ax-2 |- ( ( &W6

-> ( ( &W3 -> ( &W4 -> &W5 ) )

-> ( ( &W3 -> &W4 ) -> ( &W3 -> &W5 ) ) ) )

-> ( ( &W6 -> ( &W3 -> ( &W4 -> &W5 ) ) )

-> ( &W6 -> ( ( &W3 -> &W4 ) -> ( &W3 -> &W5 ) ) ) ) )

6:4,5:ax-mp |- ( ( &W6 -> ( &W3 -> ( &W4 -> &W5 ) ) )

-> ( &W6 -> ( ( &W3 -> &W4 ) -> ( &W3 -> &W5 ) ) ) )

qed:?: |- ( ( ph -> ps ) -> ( ( ch -> ph ) -> ( ch -> ps ) ) )

$)

This shows that mmj2 inherently has the ability to recover from such mistakes. However, erasing all the proof's formulas to recover from such mistakes is tedious to do by hand. Annoying even. :)

I would
be happier if there were an option that simply erases the entire wff
content. Or at least resets work variables back to their "most general"
state. This will give me the freedom to experiment without fear that an
accidental bad unification will lock up the proof.