Variations in HYP, CNTR and GenMP

This page explains how the variants array in Inference Rules have been generated.

The reasoners implementing the inference rules HYP, HYP_OR, CNTR and GENMP take into account such variants of $\textbf{P}$ and $\lnot \textbf{P}$. These variants correspond to a predicate equivalent or a sufficient conditon for apply the rule. The variants are only relational predicates. We consider $\textbf{P} \limp \textbf{P}^{\dagger}$ and $\textbf{P} \limp \lnot \textbf{nP}^{\dagger}$. Moreover, the default value of $\textbf{P}^{\dagger}$ is $\textbf{P}$ and this of $\textbf{nP}^{\dagger}$ is $\lnot \textbf{P}$ .

Only the negative predicate "¬ a = b" is allowed, the others are rewritten because the reasoners implementing those inference rules are applied after such normalization of relational predicates.