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 ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
A
|
* | FUN_IMAGE_GOAL |
![]() |
where ![]() ![]() |
M
|
FUN_GOAL_REC |
![]() |
where ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
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 |
![]() |
![]() ![]() |
A
|
* | EQL_RL |
![]() |
![]() ![]() |
A
|
SUBSET_INTER |
![]() |
where ![]() ![]() ![]() |
A
| |
IN_INTER |
![]() |
where ![]() ![]() ![]() |
A
| |
NOTIN_INTER |
![]() |
where ![]() ![]() ![]() |
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 ![]() |
A
|
* | OV_SETENUM_R |
![]() |
where ![]() |
A
|
* | OV_L |
![]() |
where ![]() |
A
|
* | OV_R |
![]() |
where ![]() |
A
|
* | DIS_BINTER_R |
![]() |
where ![]() ![]() |
M
|
* | DIS_BINTER_L |
![]() |
where ![]() ![]() |
M
|
* | DIS_SETMINUS_R |
![]() |
where ![]() ![]() |
M
|
* | DIS_SETMINUS_L |
![]() |
where ![]() ![]() |
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 ![]() |
M
|
* | FIN_BINTER_R |
![]() |
M
| |
FIN_KINTER_R |
![]() |
where ![]() |
M
| |
FIN_QINTER_R |
![]() |
M
| ||
* | FIN_SETMINUS_R |
![]() |
M
| |
FIN_REL |
![]() |
where ![]() |
A
| |
* | FIN_REL_R |
![]() |
the user has to write the set corresponding to ![]() |
M
|
* | FIN_REL_IMG_R |
![]() |
M
| |
* | FIN_REL_RAN_R |
![]() |
M
| |
* | FIN_REL_DOM_R |
![]() |
M
| |
FIN_FUN_DOM |
![]() |
where ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
A
| |
FIN_FUN_RAN |
![]() |
where ![]() ![]() ![]() ![]() |
A
| |
* | FIN_FUN1_R |
![]() |
the user has to write the set corresponding to ![]() |
M
|
* | FIN_FUN2_R |
![]() |
the user has to write the set corresponding to ![]() |
M
|
* | FIN_FUN_IMG_R |
![]() |
the user has to write the set corresponding to ![]() |
M
|
* | FIN_FUN_RAN_R |
![]() |
the user has to write the set corresponding to ![]() |
M
|
* | FIN_FUN_DOM_R |
![]() |
the user has to write the set corresponding to ![]() |
M
|
* | LOWER_BOUND_L |
![]() |
![]() |
M
|
* | LOWER_BOUND_R |
![]() |
![]() |
M
|
* | UPPER_BOUND_L |
![]() |
![]() |
M
|
* | UPPER_BOUND_R |
![]() |
![]() |
M
|
* | FIN_LT_0 |
![]() |
M
| |
* | FIN_GE_0 |
![]() |
M
| |
CARD_INTERV |
![]() |
where ![]() |
M
| |
CARD_EMPTY_INTERV |
![]() |
where ![]() |
M
| |
* | DERIV_LE_CARD |
![]() |
![]() ![]() |
M
|
* | DERIV_GE_CARD |
![]() |
![]() ![]() |
M
|
* | DERIV_LT_CARD |
![]() |
![]() ![]() |
M
|
* | DERIV_GT_CARD |
![]() |
![]() ![]() |
M
|
* | DERIV_EQUAL_CARD |
![]() |
![]() ![]() |
M
|
SIMP_CARD_SETMINUS_L |
![]() |
M | ||
SIMP_CARD_SETMINUS_R |
![]() |
M
| ||
SIMP_CARD_CPROD_L |
![]() |
M | ||
SIMP_CARD_CPROD_R |
![]() |
M
| ||
* | FORALL_INST |
![]() |
![]() ![]() |
M
|
* | FORALL_INST_MP |
![]() |
![]() ![]() |
M
|
* | FORALL_INST_MT |
![]() |
![]() ![]() |
M
|
* | CUT |
![]() |
hypothesis ![]() |
M
|
* | EXISTS_INST |
![]() |
![]() ![]() |
M
|
* | DISTINCT_CASE |
![]() |
case distinction on predicate ![]() |
M
|
* | ONE_POINT_L |
![]() |
The rule can be applied with ![]() ![]() |
A
|
* | ONE_POINT_R |
![]() |
The rule can be applied with ![]() ![]() |
A
|
* | SIM_OV_REL |
![]() |
where ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
A
|
* | SIM_OV_TREL |
![]() |
where ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
A
|
* | SIM_OV_PFUN |
![]() |
where ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
A
|
* | SIM_OV_TFUN |
![]() |
where ![]() ![]() ![]() ![]() ![]() |
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 ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
A |
See also Extension Proof Rules#Inference Rules.