strategy for evaluating relevant sequents

[salmans]

The existing implementations of StrategyTrait do not take advantage of information about the previously evaluated sequents.

Definitions

Unbalanced Sequent: is a sequent whose body is true in the model evaluated by the chase step but its head is false in the model.

Consider the following example:

(1) P('a);
(2) Q(x) -> R(x);
(3) P(x) -> Q(x);

After evaluating (1), the only unbalanced sequent that should be processed by the consequent chase step is (3).
A more efficient instance of StrategyTrait should skip (2) since it can never be unbalanced after running a chase step on (1).

In general, the evaluation strategy should always schedule (syntactically) relevant sequents. Considering the expensive cost of evaluating sequents in models, this evaluation strategy is expected to dramatically improve performance.

Disadvantage

This approach is inherently in conflict with congruence closure for equality reasoning as unified elements might unbalance sequents that are not syntactically relevant:

(1) P(`a);
(2) Q(`b);
(3) `a = `b;
(4) Q(x) -> R(x);

After evaluating (1) and (2) followed by (3), sequent (4) should be processed, although it is not syntactically relevant to (3).

Due to complications arising from congruence closure for equality reasoning, equality must be evaluated as a unique first-order predicate (namely =) in presence of equality axioms, processed as sequents.

With this disadvantage, it's not clear under what conditions, the suggested solution improves the performance of the chase.