Idea: Bottom-up prover statement selection: forbidden, allowed, required (low priority)

[david-a-wheeler]

I'm not sure I understand what selecting statements in the bottom-up prover does.

That said, I have a thought. Perhaps this should be a 3-way option: Forbidden, Allowed, Required.

In particular, mmj2 allows specification of required statements at the first level, and this is often useful to force the use of specific statements - making searching much faster and making it more likely you'll find the proof you wanted. You might also add a button like "require use of previous statement" since in many cases you're adding a statement to extend on a previous one.

I haven't thought through all the ramifications, and there may be another/better way. But I thought it'd be better to record the thought before it disappeared from my head, and perhaps this idea will point the way to a good/better idea.

[david-a-wheeler]

This may not be all that critical since you can specify other things, but it makes sense to put this in the "hopper of ideas" to see if anyone thinks it's important.