Better ordering of available deductions: term-specific deductions before generic deductions

[Voileexperiments]

I can already see Existential Instantiation being put on the top of the deductions list when a THERE EXIST item in an environment is selected.

There are many other things that should go on top though. Lots of deductions, especially in the formula window, applies to all kinds of terms and they clutter the deductions list very quickly if the term is big enough. Meanwhile I'm already struggling to find which item TRUE/NOT FALSE is at every single time.

Suggestion:

• Acceptable: manually order term-specific deductions before generic deductions
• Better: automatically reorder them when presenting available deductions
• Best: put them into two different divs in the deduction window, separated vertically. Though then the hotkey assignation would have to be revised

[teorth]

I'm not sure what the distinction is here between "term-specific" deductions and "generic" deductions, could you clarify please?

[Voileexperiments]

When matching the rules against a specific term, the rules are matched in different kinds of strengths according to how specific they require the statements to be. e.g if (NOT B) AND (NOT (NOT B)) [assuming A] in the environment is selected:

• Reductio ad absurdum is the strongest (Given B AND (NOT B), assuming A)
• De Morgan's Law (Given (NOT A) AND (NOT B)) is the second strongest
• laws that involve Given A AND B (e.g Conjunction elimination) is the third strongest
• laws that involve Given A (e.g AND is idempotent) is the weakest

Similarly, Given NOT (NOT A) > Given NOT A > Given A, Given (NOT A) OR B > GIVEN A OR B; and TRUE/NOT FALSE is stronger than laws like Implication Introduction. Usually when we want to invoke a law we're using the more specific ones as they're stronger and more likely to appear in short proofs, and so they should come first in the list of deductions for easier access.

Maybe when the deduction list is displayed, it can be shorted first according to these criteria:

• Amount of necessary terms involved (not sufficient terms involved because some laws have default values, e.g the bound variable to be used in Existential Introduction)
• Complexity of the matched terms A, B, C... (probably by AST size?)
• Size of the AST of the law

Or, if it's too complex, can always just assign a "priority" property to each law for sorting.