Variations in HYP, CNTR and GenMP: Difference between revisions

From Event-B
Jump to navigationJump to search
← Older editNewer edit →
imported>Laurent
m 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
imported>Laurent
No edit summary
Line 1: Line 1:
This page explains how the variants array in [[Inference Rules]] have been generated.
This page describes the introduction of variations in the HYP, HYP_OR, CNTR and GENMP reasoners.


= Context =
= 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.
The reasoners implementing the inference rules {{Rulename|HYP}}, {{Rulename|HYP_OR}}, {{Rulename|CNTR}} and {{Rulename|GENMP_*}} look for exact matches of a predicate. But, quite often, similar predicates that do not match exactly (e.g., because it has been normalized) would suffice. There is also the possibility that a variation which is equivalent to the predicate would be present. For instance, "¬ a = b" is equivalent to "¬ b = a". Finally, the reasoners shall also consider variations 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 {{Rulename|HYP}}.


= Objective =
= Objective =


The reasoners implementing these inference rules should take into account such variants of <math>\textbf{P} </math> and <math> \lnot \textbf{P} </math> when looking for occurrences.
The point of this enhancement is therefore to increase the proof power of the considered reasoners by having them consider variations of the sought predicate.


= Conventions =
= Conventions =


These variants have been generated based on the following
The variations in the [[Inference Rules]] page have been generated such that the following facts hold:
rules:
* <math> \textbf{P} \limp \textbf{P}^{\dagger} </math>
* <math> \textbf{P} \limp \textbf{P}^{\dagger} </math>
* <math> \textbf{P} \limp \lnot \textbf{nP}^{\dagger} </math>
* <math> \textbf{P} \limp \lnot \textbf{nP}^{\dagger} </math>


 
Moreover, we consider only variations that are in normal form (that is invariant under rewriting by the auto-rewriter of the sequent prover). This is why the table does not contain predicates such as <math>\lnot a < b</math>, but contain <math>b\le a</math> instead.
In the case of the predicate which is checked is positive the default value of <math> \textbf{P}^{\dagger} </math> is <math> \textbf{P} </math> and this of <math> \textbf{nP}^{\dagger} </math> is <math> \lnot \textbf{P} </math>. If the predicate is negative, the default value of <math> \textbf{nP}^{\dagger} </math> is <math> \textbf{P} </math>. 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.

Revision as of 10:28, 29 August 2013

This page describes the introduction of variations in the HYP, HYP_OR, CNTR and GENMP reasoners.

Context

The reasoners implementing the inference rules

HYP

,

HYP_OR

,

CNTR

and

GENMP_*

look for exact matches of a predicate. But, quite often, similar predicates that do not match exactly (e.g., because it has been normalized) would suffice. There is also the possibility that a variation which is equivalent to the predicate would be present. For instance, "¬ a = b" is equivalent to "¬ b = a". Finally, the reasoners shall also consider variations 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 point of this enhancement is therefore to increase the proof power of the considered reasoners by having them consider variations of the sought predicate.

Conventions

The variations in the Inference Rules page have been generated such that the following facts hold:

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

Moreover, we consider only variations that are in normal form (that is invariant under rewriting by the auto-rewriter of the sequent prover). This is why the table does not contain predicates such as \lnot a < b, but contain b\le a instead.

Retrieved from ‘https://wiki.event-b.org/index.php?title=Variations_in_HYP,_CNTR_and_GenMP&oldid=10619’