Inference Rules
From Event-B
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 |
see below for | A
| |
* | HYP_OR |
see below for | A
| |
* | CNTR |
see below for | 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_LR |
M
| ||
* | EQV_RL |
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_BUNION_R |
M
| ||
* | FIN_KUNION_R |
where is fresh | M
| |
* | FIN_QUNION_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
| |
INDUC_NAT |
of type appears free in ; is introduced as a fresh identifier | M
| ||
INDUC_NAT_COMPL |
of type appears free in ; is introduced as a fresh identifier | M
|
Those following rules have been implemented in the reasoner GeneralizedModusPonens.
Name | Rule | Side Condition | A/M | |
---|---|---|---|---|
* | GENMP_HYP_HYP |
see below for | A | |
* | GENMP_NOT_HYP_HYP |
see below for | A | |
* | GENMP_HYP_GOAL |
see below for | A | |
* | GENMP_NOT_HYP_GOAL |
see below for | A | |
* | GENMP_GOAL_HYP |
see below for | A | |
* | GENMP_NOT_GOAL_HYP |
see below for | A | |
* | GENMP_OR_GOAL_HYP |
see below for | A | |
* | GENMP_OR_NOT_GOAL_HYP |
see below for | 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_SUBSETEQ_LR |
A | ||
* | EQUAL_SUBSETEQ_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 | |
* | DERIV_IN_SUBSET |
A |
The conventions used in this table are described in Variations in HYP, CNTR and GenMP.
Side Condition | |||
---|---|---|---|
|
|
where a and b are integers | |
|
|
||
|
|
||
|
|
where A and B are sets | |
|
|
||
|
|
||
where e and f are scalars | |||
See also Extension Proof Rules#Inference Rules.