You can subscribe to this list here.
2009 
_{Jan}
(2) 
_{Feb}
(5) 
_{Mar}

_{Apr}

_{May}
(2) 
_{Jun}
(8) 
_{Jul}
(4) 
_{Aug}

_{Sep}

_{Oct}
(2) 
_{Nov}
(6) 
_{Dec}


2010 
_{Jan}
(1) 
_{Feb}
(1) 
_{Mar}
(3) 
_{Apr}
(2) 
_{May}
(2) 
_{Jun}
(2) 
_{Jul}
(18) 
_{Aug}
(13) 
_{Sep}
(7) 
_{Oct}

_{Nov}

_{Dec}
(2) 
2011 
_{Jan}

_{Feb}
(11) 
_{Mar}

_{Apr}
(4) 
_{May}

_{Jun}
(1) 
_{Jul}
(18) 
_{Aug}
(16) 
_{Sep}
(12) 
_{Oct}
(12) 
_{Nov}
(19) 
_{Dec}
(42) 
2012 
_{Jan}
(16) 
_{Feb}
(3) 
_{Mar}
(8) 
_{Apr}
(14) 
_{May}
(30) 
_{Jun}
(5) 
_{Jul}
(7) 
_{Aug}
(3) 
_{Sep}
(10) 
_{Oct}
(4) 
_{Nov}
(10) 
_{Dec}
(1) 
2013 
_{Jan}
(14) 
_{Feb}
(8) 
_{Mar}
(5) 
_{Apr}
(3) 
_{May}
(9) 
_{Jun}
(19) 
_{Jul}

_{Aug}
(27) 
_{Sep}
(5) 
_{Oct}
(18) 
_{Nov}
(12) 
_{Dec}
(8) 
2014 
_{Jan}
(5) 
_{Feb}
(8) 
_{Mar}
(20) 
_{Apr}
(22) 
_{May}
(28) 
_{Jun}
(9) 
_{Jul}
(6) 
_{Aug}
(46) 
_{Sep}
(40) 
_{Oct}
(15) 
_{Nov}
(8) 
_{Dec}
(34) 
2015 
_{Jan}
(20) 
_{Feb}
(15) 
_{Mar}
(18) 
_{Apr}
(20) 
_{May}
(3) 
_{Jun}
(13) 
_{Jul}
(10) 
_{Aug}
(19) 
_{Sep}
(8) 
_{Oct}
(15) 
_{Nov}

_{Dec}

S  M  T  W  T  F  S 






1

2

3

4

5

6

7

8

9

10

11
(1) 
12

13

14

15

16

17

18

19

20

21

22

23
(1) 
24

25

26
(1) 
27

28

29
(1) 
30
(1) 
31







From: Duy Khanh Le <le.cs@gm...>  20130323 11:07:27

Hi, I am a newbie using Redlog to solve floating point constraints. I recently reinstalled my machine and hence I also reinstalled redcsl from SVN by following the instruction at http://sourceforge.net/apps/mediawiki/reducealgebra/index.php?title=Installation However, after I was able to get redcsl installed, redcsl seems to work in an unexpected way. This is the command that I typed in redcsl IDE: 1: load redlog; 2: rlabout(); Redlog Development Version, Sat Mar 23 15:07:38 2013 (C) A. Dolzmann and T. Sturm http://www.redlog.eu/ 5: rlset R; 7: phi1:=rlall((((((x <> 1.)) or ((y <> 1.))) or ((x > 1.))) or ((x = y)))); \phi\mathrm{:=}\forall x\forall y\left(\left(\left(x1\,\neq\, 0\,\vee\, y1\,\neq\, 0\right)\,\vee\, x1\,>\, 0\right)\,\vee\, xy=0\right) 8: rlqe phi1; \mathrm{false} The PROBLEM is that redcsl returns FALSE (which is not correct). The formula phi I wanted to prove is: x=1.0 and y=1.0 and x<=1.0 imply x=y (which should be correct). Note that x<=1.0 is indeed redudant due to x=1.0. However, if we omit x<=1.0, the outcome is correct. 4: phi2:=rlall(((((x <> 1.)) or ((y <> 1.))) or ((x = y)))); \phi\mathrm{:=}\forall x\forall y\left(\left(x1\,\neq\, 0\,\vee\, y1\,\neq\, 0\right)\,\vee\, xy=0\right) 5: rlqe phi2; \mathrm{true} However, if I use the older version of redlog in another machine of mine, then the REDLOG DEVELOPMENT VERSION, Wed Jan 12 16:27:06 2011 (C) 19952009 A. Dolzmann and T. Sturm http://www.redlog.eu/ Then, I got the correct result for "rlqe phi1;" which is TRUE. Would it be the case that the latest version of redlog from SVN is errorprone? THank you so much for your help. Best regards, Khanh 