Variations in HYP, CNTR and GenMP

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

Context

The reasoners implementing the inference rules HYP, HYP_OR, CNTR and GENMP_* look for exact matches of a predicate. But, quite often a relational predicate no exact matches (for instance, because it has been normalized). Moreover, there is sometimes a variant which is equivalent to the predicate which is checked. For instance, "¬ a = b" is equivalent to "¬ b = a". Finally, the reasoners shall also consider variants which are a sufficient condition for the rule. For instance, if the goal is "a ≤ b", then a hypothesis "a < b" is a sufficient condition to discharge the goal with HYP.

Objective

The reasoners implementing these inference rules should take into account such variants of $\textbf{P}$ and $\lnot \textbf{P}$ when looking for occurrences.

Conventions

These variants have been generated based on the following rules:

• $\textbf{P} \limp \textbf{P}^{\dagger}$
• $\textbf{P} \limp \lnot \textbf{nP}^{\dagger}$

In the case of the predicate which is checked is positive the default value of $\textbf{P}^{\dagger}$ is $\textbf{P}$ and this of $\textbf{nP}^{\dagger}$ is $\lnot \textbf{P}$. If the predicate is negative, the default value of $\textbf{nP}^{\dagger}$ is $\textbf{P}$. However, the negative arithmetic predicates are not taken into account by the reasoners implementing those inference rules because these reasonner are applied after such normalization of relational predicates. For instance, "¬ a < b" is normalized to "b ≤ a". There is an exception in the case "¬ a = b", this predicate is allowed by the normalization.