Inference Rules
From Event-B
Revision as of 16:34, 28 September 2011 by imported>Billaude (Add inference rules used in MapOvrGoal, MembershipGoal (so far), GeneralizedModusPonens and the AutoRewriterL3.)
CAUTION! Any modification to this page shall be announced on the User mailing list!
Rules that are marked with a * in the first column are implemented in the latest version of Rodin. Rules without a * are planned to be implemented in future versions. Other conventions used in these tables are described in The_Proving_Perspective_(Rodin_User_Manual)#Inference_Rules.
Name | Rule | Side Condition | A/M
| |
---|---|---|---|---|
* | HYP |
A
| ||
* | HYP_OR |
A
| ||
* | CNTR |
A
| ||
* | FALSE_HYP |
A
| ||
* | TRUE_GOAL |
A
| ||
* | FUN_GOAL |
where and denote types and is one of , , , , , , . | A
| |
* | FUN_IMAGE_GOAL |
where denotes a set of relations (any arrow) and is WD strict | M
| |
FUN_GOAL_REC |
where and denote types, denotes a set of relations (any arrow) and is one of , , , , , , . | A
| ||
* | DBL_HYP |
A
| ||
* | AND_L |
A
| ||
* | AND_R |
A
| ||
IMP_L1 |
A
| |||
* | IMP_R |
A
| ||
* | IMP_AND_L |
A
| ||
* | IMP_OR_L |
A
| ||
* | AUTO_MH |
A
| ||
* | NEG_IN_L |
A
| ||
* | NEG_IN_R |
A
| ||
* | XST_L |
A
| ||
* | ALL_R |
A
| ||
* | EQL_LR |
is a variable which is not free in | A
| |
* | EQL_RL |
is a variable which is not free in | A
| |
SUBSET_INTER |
where and are not bound by | A
| ||
IN_INTER |
where and are not bound by | A
| ||
NOTIN_INTER |
where and are not bound by | A
| ||
* | FIN_L_LOWER_BOUND_L |
The goal is discharged | A
| |
* | FIN_L_LOWER_BOUND_R |
The goal is discharged | A
| |
* | FIN_L_UPPER_BOUND_L |
The goal is discharged | A
| |
* | FIN_L_UPPER_BOUND_R |
The goal is discharged | A
| |
* | CONTRADICT_L |
M
| ||
* | CONTRADICT_R |
M
| ||
* | CASE |
M
| ||
* | IMP_CASE |
M
| ||
* | MH |
M
| ||
* | HM |
M
| ||
EQV |
M
| |||
* | OV_SETENUM_L |
where is WD strict | A
| |
* | OV_SETENUM_R |
where is WD strict | A
| |
* | OV_L |
where is WD strict | A
| |
* | OV_R |
where is WD strict | A
| |
* | DIS_BINTER_R |
where and denote types. | M
| |
* | DIS_BINTER_L |
where and denote types. | M
| |
* | DIS_SETMINUS_R |
where and denote types. | M
| |
* | DIS_SETMINUS_L |
where and denote types. | M
| |
* | SIM_REL_IMAGE_R |
M
| ||
* | SIM_REL_IMAGE_L |
M
| ||
* | SIM_FCOMP_R |
M
| ||
* | SIM_FCOMP_L |
M
| ||
* | FIN_SUBSETEQ_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |
* | FIN_BINTER_R |
M
| ||
FIN_KINTER_R |
where is fresh | M
| ||
FIN_QINTER_R |
M
| |||
* | FIN_SETMINUS_R |
M
| ||
FIN_REL |
where denotes a set of relations (any arrow) | A
| ||
* | FIN_REL_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |
* | FIN_REL_IMG_R |
M
| ||
* | FIN_REL_RAN_R |
M
| ||
* | FIN_REL_DOM_R |
M
| ||
FIN_FUN_DOM |
where is one of , , , , , , | A
| ||
FIN_FUN_RAN |
where is one of , , | A
| ||
* | FIN_FUN1_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |
* | FIN_FUN2_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |
* | FIN_FUN_IMG_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |
* | FIN_FUN_RAN_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |
* | FIN_FUN_DOM_R |
the user has to write the set corresponding to in the editing area of the Proof Control Window | M
| |
* | LOWER_BOUND_L |
must not contain any bound variable | M
| |
* | LOWER_BOUND_R |
must not contain any bound variable | M
| |
* | UPPER_BOUND_L |
must not contain any bound variable | M
| |
* | UPPER_BOUND_R |
must not contain any bound variable | M
| |
* | FIN_LT_0 |
M
| ||
* | FIN_GE_0 |
M
| ||
CARD_INTERV |
where is WD strict | M
| ||
CARD_EMPTY_INTERV |
where is WD strict | M
| ||
* | DERIV_LE_CARD |
and bear the same type | M
| |
* | DERIV_GE_CARD |
and bear the same type | M
| |
* | DERIV_LT_CARD |
and bear the same type | M
| |
* | DERIV_GT_CARD |
and bear the same type | M
| |
* | DERIV_EQUAL_CARD |
and bear the same type | M
| |
SIMP_CARD_SETMINUS_L |
M | |||
SIMP_CARD_SETMINUS_R |
M
| |||
SIMP_CARD_CPROD_L |
M | |||
SIMP_CARD_CPROD_R |
M
| |||
* | FORALL_INST |
is instantiated with | M
| |
* | FORALL_INST_MP |
is instantiated with and a Modus Ponens is applied | M
| |
* | FORALL_INST_MT |
is instantiated with and a Modus Tollens is applied | M
| |
* | CUT |
hypothesis is added | M
| |
* | EXISTS_INST |
is instantiated with | M
| |
* | DISTINCT_CASE |
case distinction on predicate | M
| |
* | ONE_POINT_L |
The rule can be applied with as well as with | A
| |
* | ONE_POINT_R |
The rule can be applied with as well as with | A
| |
* | SIM_OV_REL |
where is one of , , , , , , , , , , | A
| |
* | SIM_OV_TREL |
where is one of , , ,, , | A
| |
* | SIM_OV_PFUN |
where is one of , , , , , , | A
| |
* | SIM_OV_TFUN |
where is one of , , , | A |
Those following rules have been implemented in the reasoner GeneralizedModusPonens.
Name | Rule | Side Condition | A/M | |
---|---|---|---|---|
* | GENMP_HYP_HYP |
A | ||
* | GENMP_NOT_HYP_HYP |
A | ||
* | GENMP_HYP_GOAL |
A | ||
* | GENMP_NOT_HYP_GOAL |
A | ||
* | GENMP_GOAL_HYP |
A | ||
* | GENMP_NOT_GOAL_HYP |
A | ||
* | GENMP_OR_GOAL_HYP |
A | ||
* | GENMP_OR_NOT_GOAL_HYP |
A |
Thos following rules have been implemented in the MembershipGoal reasoner.
Name | Rule | Side Condition | A/M
| |
---|---|---|---|---|
* | SUBSET_SUBSETEQ |
A | ||
* | DOM_SUBSET |
A | ||
* | RAN_SUBSET |
A | ||
* | EQUAL_SUBSET_LR |
A | ||
* | EQUAL_SUBSET_RL |
A | ||
* | IN_DOM_CPROD |
A | ||
* | IN_RAN_CPROD |
A | ||
* | IN_DOM_REL |
A | ||
* | IN_RAN_REL |
A | ||
* | SETENUM_SUBSET |
A | ||
* | OVR_RIGHT_SUBSET |
A | ||
* | RELSET_SUBSET_CPROD |
where is one of , , , , , , , , , , | A |
See also Extension Proof Rules#Inference Rules.