Inference Rules: Revision history

30 May 2013

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

28 May 2013

• curprev 11:0611:06, 28 May 2013‎ imported>Josselin‎ 32,597 bytes +2‎ Fix rule CNTR
• curprev 10:0510:05, 28 May 2013‎ imported>Josselin‎ 32,595 bytes +290‎ Fix GENMP rules
• curprev 08:3508:35, 28 May 2013‎ imported>Josselin‎ 32,305 bytes −119‎ Remove 2 rows from the new array
• curprev 08:3108:31, 28 May 2013‎ imported>Josselin‎ 32,424 bytes +172‎ Fix rules HYP_OR, GENMP_OR_GOAL_HYP, GENMP_OR_NOT_GOAL_HYP
• curprev 08:2208:22, 28 May 2013‎ imported>Josselin‎ 32,252 bytes +48‎ Add side condition (CNTR rule)

27 May 2013

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

10 September 2012

• 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.

29 September 2011

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

28 September 2011

• 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.

23 August 2011

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

23 May 2011

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

5 April 2011

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

4 April 2011

• 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

30 March 2011

• 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).

8 February 2011

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

7 February 2011

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

14 December 2010

• 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

13 December 2010

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

16 November 2010

• 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

15 October 2010

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

8 October 2010

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

17 September 2010

• 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.

9 September 2010

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

6 September 2010

• 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)

30 August 2010

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

27 August 2010

• 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

25 August 2010

• curprev 16:5616:56, 25 August 2010‎ imported>Laurent‎ 25,249 bytes −238‎ Changed REC_FUN_GOAL to FUN_GOAL_REC and fixed typing.

23 August 2010

• curprev 13:1413:14, 23 August 2010‎ imported>Desaperh‎ 25,487 bytes +760‎ Added rule REC_FUN_GOAL
• curprev 13:1213:12, 23 August 2010‎ imported>Desaperh‎ 24,727 bytes −760‎ Undo revision 6711 by Desaperh (Talk)
• curprev 13:0913:09, 23 August 2010‎ imported>Desaperh‎ 25,487 bytes +760‎ No edit summary

6 August 2010

• curprev 13:5513:55, 6 August 2010‎ imported>Nicolas‎ 24,727 bytes +584‎ added DATATYPE_INDUCTION; rewrote DATATYPE_DISTINCT_CASE
• curprev 12:3812:38, 6 August 2010‎ imported>Nicolas‎ 24,143 bytes +625‎ added DATATYPE_DISTINCT_CASE

4 August 2010

• curprev 16:3716:37, 4 August 2010‎ imported>Pascal‎ 23,518 bytes +129‎ No edit summary

28 April 2010

• curprev 13:4713:47, 28 April 2010‎ imported>Tommy‎ 23,389 bytes −884‎ Rules OV_SETENUM_L (resp. OV_SETENUM_R) and OV_L (resp. OV_R) have been implemented in r8699.

21 April 2010

• curprev 16:4616:46, 21 April 2010‎ imported>Tommy‎ 24,273 bytes +13‎ Added rules FUNIMG_SET_DOMSUB_L and FUNIMG_DOMSUB_L
• curprev 16:3216:32, 21 April 2010‎ imported>Tommy‎ m 24,260 bytes +871‎ No edit summary
• curprev 15:2715:27, 21 April 2010‎ imported>Laurent‎ 23,389 bytes +6‎ Fixed rules OV_L, OV_R, OV_SETENUM_L, and OV_SETENUM_R.
• curprev 15:2015:20, 21 April 2010‎ imported>Tommy‎ m 23,383 bytes +80‎ No edit summary
• curprev 13:0613:06, 21 April 2010‎ imported>Tommy‎ m 23,303 bytes 0‎ No edit summary

27 March 2010

• curprev 22:3022:30, 27 March 2010‎ imported>Laurent‎ m 23,303 bytes +8‎ No edit summary

1 February 2010

• curprev 11:5611:56, 1 February 2010‎ imported>Laurent‎ 23,295 bytes +1,470‎ Added rules SIMP_CARD_SETMINUS_L, SIMP_CARD_SETMINUS_R, SIMP_CARD_CPROD_L and SIMP_CARD_CPROD_R (were previously rewrite rules).

15 January 2010

• curprev 11:0711:07, 15 January 2010‎ imported>Laurent‎ 21,825 bytes 0‎ Marked CARD_EMPTY_INTERV as not implemented.