Inference Rules: Revision history

From Event-B

View logs for this page

Jump to navigation Jump to search

Diff selection: Mark the radio buttons of the revisions to compare and hit enter or the button at the bottom.
Legend: (cur) = difference with latest revision, (prev) = difference with preceding revision, m = minor edit.

curprev 15:1015:10, 3 June 2024‎ Guillaume talk contribs‎ 36,436 bytes +1‎ Rule FIN_COMPSET_R has been implemented in Rodin 3.9

curprev 10:2210:22, 1 February 2024‎ Guillaume talk contribs‎ 36,435 bytes +203‎ Add rule for finiteness of explicit set comprehension

curprev 14:3214:32, 13 April 2023‎ Guillaume talk contribs‎ 36,232 bytes +2‎ Rules EQV_LR and EQV_RL were implemented

curprev 09:3009:30, 6 April 2023‎ Guillaume talk contribs‎ 36,230 bytes 0‎ Add star to proof rules implemented in Rodin 3.8

curprev 15:2615:26, 21 October 2022‎ Guillaume talk contribs‎ 36,230 bytes +26‎ Fix inference rule FIN_KUNION_R

curprev 09:2009:20, 17 October 2022‎ Guillaume talk contribs‎ 36,204 bytes +694‎ Add rules for finiteness of union

curprev 16:0016:00, 23 June 2014‎ imported>Nicolas‎ m 35,510 bytes −595‎ Removed induction on integers (was wrong), reviewed induciton on naturals
curprev 13:4713:47, 23 June 2014‎ imported>Nicolas‎ m 36,105 bytes +1,449‎ Added INDUC_* inference rules

curprev 14:2414:24, 13 June 2014‎ imported>Laurent‎ 34,656 bytes +218‎ Split EQV into EQV_LR and EQV_RL

curprev 10:1410:14, 29 August 2013‎ imported>Laurent‎ m 34,438 bytes +2‎ No edit summary

curprev 12:1412:14, 20 August 2013‎ imported>Josselin‎ 34,436 bytes +266‎ Add scalar case in Variants array.

curprev 15:4215:42, 1 August 2013‎ imported>Josselin‎ 34,170 bytes +679‎ added space in array for improved readability
curprev 13:4113:41, 1 August 2013‎ imported>Josselin‎ 33,491 bytes +1,252‎ Fix HYP, HYPOR, GenMP rules + added inclusion cases

curprev 09:3909:39, 31 July 2013‎ imported>Josselin‎ 32,239 bytes −301‎ moved explanation in Variants_in_HYP,_CNTR_and_GenMP page

curprev 16:0116:01, 30 July 2013‎ imported>Josselin‎ 32,540 bytes 0‎ Fix explanation about variants of P and not P
curprev 14:3314:33, 30 July 2013‎ imported>Josselin‎ 32,540 bytes +55‎ Added new variants of P and not P

curprev 08:4908:49, 30 May 2013‎ imported>Josselin‎ 32,485 bytes −112‎ Fix HYP rule (Removed predicate with a not symbol)

curprev 15:4615:46, 27 May 2013‎ imported>Josselin‎ 32,204 bytes +1,857‎ Fix rules HYP and CNTR (case distinction on relational predicate)

curprev 09:5809:58, 10 September 2012‎ imported>Billaude‎ m 30,347 bytes +8‎ SIM_OV_REL, SIM_OV_TREL, SIM_OV_PFUN and SIM_OV_TFUN were miswritten.

curprev 14:5414:54, 29 September 2011‎ imported>Billaude‎ 30,339 bytes +110‎ Add a missing rule. Correct two rule's names.

curprev 16:3416:34, 28 September 2011‎ imported>Billaude‎ 30,229 bytes +4,431‎ Add inference rules used in MapOvrGoal, MembershipGoal (so far), GeneralizedModusPonens and the AutoRewriterL3.

curprev 11:1611:16, 23 August 2011‎ imported>Billaude‎ 25,798 bytes −320‎ No edit summary

curprev 07:2507:25, 23 May 2011‎ imported>Billaude‎ m 26,118 bytes 0‎ IMP_CASE is now marked as implemented.

curprev 09:2009:20, 5 April 2011‎ imported>Laurent‎ m 26,118 bytes 0‎ No edit summary

curprev 16:4416:44, 4 April 2011‎ imported>Laurent‎ 26,118 bytes +821‎ Added rules FIN_REL, FIN_FUN_DOM and FIN_FUN_RAN
curprev 15:0315:03, 4 April 2011‎ imported>Laurent‎ 25,297 bytes +268‎ Added rule IMP_CASE

curprev 14:5214:52, 30 March 2011‎ imported>Nicolas‎ m 25,029 bytes 0‎ NEG_IN_L and NEG_IN_R back to implemented status, after checking implementation
curprev 14:3114:31, 30 March 2011‎ imported>Laurent‎ 25,029 bytes +32‎ FIxed rules NEG_IN_L and NEG_IN_R (see bug #3244113).

curprev 14:4114:41, 8 February 2011‎ imported>Tommy‎ m 24,997 bytes +1‎ Implemented FORALL_INST_MT in r10767.

curprev 13:4513:45, 7 February 2011‎ imported>Tommy‎ m 24,996 bytes +427‎ Added FORALL_INST_MT rule

curprev 12:5612:56, 14 December 2010‎ imported>Laurent‎ m 24,569 bytes −1‎ No edit summary
curprev 12:5512:55, 14 December 2010‎ imported>Laurent‎ 24,570 bytes +237‎ Fixed FIN_QINTER_R and added FIN_KINTER_R

curprev 17:0417:04, 13 December 2010‎ imported>Nicolas‎ 24,333 bytes +195‎ added rule FIN_QINTER_R

curprev 13:4713:47, 16 November 2010‎ imported>Laurent‎ m 24,138 bytes 0‎ Marked rules ONE_POINT_L and ONE_POINT_R as implemented
curprev 13:3413:34, 16 November 2010‎ imported>Laurent‎ m 24,138 bytes 0‎ Marked rule FUN_IMAGE_GOAL as implemented

curprev 08:2608:26, 15 October 2010‎ imported>Desaperh‎ 24,138 bytes 0‎ No edit summary

curprev 14:5614:56, 8 October 2010‎ imported>Desaperh‎ 24,138 bytes 0‎ Rule FUN_IMAGE_GOAL has been implemented

curprev 16:4716:47, 17 September 2010‎ imported>Laurent‎ 24,138 bytes −172‎ Removed WD-strictness condition where it was unnecessary and unimplemented.
curprev 14:3214:32, 17 September 2010‎ imported>Laurent‎ 24,310 bytes −321‎ Replaced "top-level" with WD strictness or freeness condition.

curprev 12:2712:27, 9 September 2010‎ imported>Nicolas‎ m 24,631 bytes −1,120‎ moved datatype rules to extension proof rules page

curprev 08:5408:54, 6 September 2010‎ imported>Nicolas‎ m 25,751 bytes +34‎ added a link to datatype rule examples
curprev 08:2508:25, 6 September 2010‎ imported>Nicolas‎ m 25,717 bytes −71‎ simplified representation of rule DATATYPE_INDUCTION (the meaning remains the same)

curprev 12:1412:14, 30 August 2010‎ imported>Wohuai‎ m 25,788 bytes +191‎ No edit summary

curprev 14:0814:08, 27 August 2010‎ imported>Laurent‎ 25,597 bytes 0‎ Rule FUN_IMAGE_GOAL is manual
curprev 13:1313:13, 27 August 2010‎ imported>Laurent‎ 25,597 bytes +348‎ Added rule FUN_IMAGE_GOAL

Retrieved from ‘https://wiki.event-b.org/index.php/Inference_Rules’

Navigation menu