Bram-Hub/Willow

Support logical equivalence rules

Opened this issue · 0 comments

Is your feature request related to a problem? Please describe.
The logic engine currently has no way to re-express a statement in terms of equivalent statements; this can only be done through decomposition. While the truth tree method is complete, there is no way of directly applying traditional equivalence rules to statements.

Describe the solution you'd like
The user should be able to use equivalence rules as a step in a truth tree. The equivalence rule need not be performed in every child branch, and is not necessary for a statement to be considered fully decomposed.

Describe alternatives you've considered
The alternative requires that a user fully decompose the statement into atomic components, which can become tedious for large statements that can be quickly simplified using logical equivalences.

Additional context
There is no additional context.