A binary feature that returns zero iff the constraint of the given taclet app
is stronger than the original constraint of the formula to which the rule is
applied (i.e.
This feature is similar to ConstraintStrengthenFeature, but
instead of just comparing the constraint resulting from a rule application
with the original constraint of the find-formula of the application, the new
constraint is compared with the joint of the original constraint and the user
constraint.
This feature returns zero if and only if the focus of the given rule
application exists, is not top-level and the symbol immediately above the
focus is badSymbol.
This feature returns zero if and only if the focus of the given rule
application exists, is not top-level and the symbol immediately above the
focus is badSymbol.
Walking from the root of a formula down to the focus of a rule application,
count how often we choose the left branch (subterm) and how the right
branches.
Feature that returns zero if there is no atom with negative polarity on a
common d-path and on the left of the find-position within the find-formula as
a formula of the antecedent.
Binary feature that returns zero iff the find-formula of a rule contains a
d-path consisting only of positive literals (as a formula of the antecedent).
Used terminology is defined in Diss.
Binary feature that returns zero iff the hyper-tableaux simplification method
approves the given application (which is supposed to be the application of a
beta rule).
Binary feature that returns true iff the hyper-tableaux simplification method
approves the given application (which is supposed to be the application of a
replace-known rule).