Inference Rules: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Josselin Fix rules HYP_OR, GENMP_OR_GOAL_HYP, GENMP_OR_NOT_GOAL_HYP |
imported>Josselin Remove 2 rows from the new array |
||
Line 263: | Line 263: | ||
{|class="RRHeader" text-align="left" border="1" cellspacing="4" cellpadding="8" rules="all" frame="box" style="margin:1em 1em 1em 0; border-style:solid; border-color:#AAAAAA; display:table; {{{style|}}}" | {|class="RRHeader" text-align="left" border="1" cellspacing="4" cellpadding="8" rules="all" frame="box" style="margin:1em 1em 1em 0; border-style:solid; border-color:#AAAAAA; display:table; {{{style|}}}" | ||
! <math>\textbf{P}</math> !! <math>\textbf{P}^{\dagger}</math> !! <math>\textbf{nP}^{\dagger}</math> | ! <math>\textbf{P}</math> !! <math>\textbf{P}^{\dagger}</math> !! <math>\textbf{nP}^{\dagger}</math> | ||
{{RRRow}}| <math> a = b </math> || <math> b = a </math> || <math> \lnot b = a </math> | {{RRRow}}| <math> a = b </math> || <math> b = a </math> || <math> \lnot b = a </math> | ||
{{RRRow}}| <math> a < b </math> || <math> \lnot a \ge b, \lnot b \le a, b > a </math> || <math> a \ge b, b \le a, \lnot b > a </math> | {{RRRow}}| <math> a < b </math> || <math> \lnot a \ge b, \lnot b \le a, b > a </math> || <math> a \ge b, b \le a, \lnot b > a </math> | ||
{{RRRow}}| <math> a > b </math> || <math> \lnot a \le b, \lnot b \ge a, b < a </math> || <math> a \le b, b \ge a, \lnot b < a </math> | {{RRRow}}| <math> a > b </math> || <math> \lnot a \le b, \lnot b \ge a, b < a </math> || <math> a \le b, b \ge a, \lnot b < a </math> | ||
{{RRRow}}| <math> a \le b </math> || <math> \lnot a > b, \lnot b < a, b \ge a </math> || <math> a > b, b < a, \lnot b \ge a </math> | {{RRRow}}| <math> a \le b </math> || <math> \lnot a > b, \lnot b < a, b \ge a </math> || <math> a > b, b < a, \lnot b \ge a </math> | ||
{{RRRow}}| <math> a \ge b </math> || <math> \lnot a < b, \lnot b > a, b \le a </math> || <math> a < b, b > a, \lnot b \le a </math> | {{RRRow}}| <math> a \ge b </math> || <math> \lnot a < b, \lnot b > a, b \le a </math> || <math> a < b, b > a, \lnot b \le a </math> | ||
{{RRRow}}| <math> a \subseteq b </math> | {{RRRow}}| <math> a \subseteq b </math> || || | ||
{{RRRow}}| <math> a \subset b </math> | {{RRRow}}| <math> a \subset b </math> || || | ||
{{RRRow}}| <math> \lnot a = b </math> || || <math> b = a </math> | {{RRRow}}| <math> \lnot a = b </math> || || <math> b = a </math> | ||
{{RRRow}}| <math> \lnot a < b </math> || || <math> \lnot a > b, \lnot b < a, b \ge a </math> | {{RRRow}}| <math> \lnot a < b </math> || || <math> \lnot a > b, \lnot b < a, b \ge a </math> | ||
{{RRRow}}| <math> \lnot a > b </math> || || <math> \lnot a \le b, \lnot b \ge a, b < a </math> | {{RRRow}}| <math> \lnot a > b </math> || || <math> \lnot a \le b, \lnot b \ge a, b < a </math> | ||
{{RRRow}}| <math> \lnot a \le b </math> || || <math> \lnot a > b, \lnot b < a, b \ge a </math> | {{RRRow}}| <math> \lnot a \le b </math> || || <math> \lnot a > b, \lnot b < a, b \ge a </math> | ||
{{RRRow}}| <math> \lnot a \ge b </math> || || <math> \lnot a < b, \lnot b > a, b \le a </math> | {{RRRow}}| <math> \lnot a \ge b </math> || || <math> \lnot a < b, \lnot b > a, b \le a </math> | ||
{{RRRow}}| <math> \lnot a \subseteq b </math> | {{RRRow}}| <math> \lnot a \subseteq b </math> || || | ||
{{RRRow}}| <math> \lnot a \subset b </math> | {{RRRow}}| <math> \lnot a \subset b </math> || || | ||
{{RRRow}}| <math> \textbf{P} </math> || <math> \textbf{P} </math> ||<math> \neg\, \textbf{P} </math> | {{RRRow}}| <math> \textbf{P} </math> || <math> \textbf{P} </math> ||<math> \neg\, \textbf{P} </math> | ||
|} | |} | ||
Revision as of 08:35, 28 May 2013
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 ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
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 |
![]() |
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 ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
A |
* | DERIV_IN_SUBSET |
![]() |
A |
![]() |
![]() |
![]() |
---|---|---|
![]() |
![]() |
![]() |
![]() |
![]() |
![]() |
![]() |
![]() |
![]() |
![]() |
![]() |
![]() |
![]() |
![]() |
![]() |
![]() |
||
![]() |
||
![]() |
![]() | |
![]() |
![]() | |
![]() |
![]() | |
![]() |
![]() | |
![]() |
![]() | |
![]() |
||
![]() |
||
![]() |
![]() |
![]() |
See also Extension Proof Rules#Inference Rules.