Variations in HYP, CNTR and GenMP

From Event-B
Revision as of 10:13, 29 August 2013 by imported>Laurent (Laurent moved page Variants in HYP, CNTR and GenMP to Variations in HYP, CNTR and GenMP without leaving a redirect: Variant is misleading in an Event-B context)
Jump to navigationJump to search

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.