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}
(31) 
_{Nov}
(26) 
_{Dec}

S  M  T  W  T  F  S 

1

2

3

4

5

6

7

8

9

10

11

12
(2) 
13

14

15

16
(3) 
17

18
(1) 
19

20

21

22

23

24

25

26

27

28

29

30






From: Marko Kääramees <Marko.K<aaramees@tt...>  20091118 13:18:49

Thomas, thank you for the insight. marko Dr. Thomas Sturm wrote: > Am 16.11.2009 um 17:25 schrieb Marko Kääramees: > > >> Hi, >> >> I use Reduce and its package Redlog for simplifying the boolean >> combination of linear inequalities. I found that some quite obvious >> simplifications work only one way in the redlog. An example script >> >> load_package redlog; >> rlset pasf; >> c := (x = 1 or x >= 2) and (x = 6 or x <= 5); >> rlsimpl c; >> >> simplifies to >> >> x  1 >= 0 and (x  5 <= 0 or x  6 = 0) >> >> The first disjunction with >= is simplified, but the other with <= is >> not. Could somebody explain the reasons please or guide if it can be >> tuned somehow. >> > > This indeed puzzled me at first glance. In fact there is no simplification at all implemented that would discover this situation. What happens is the following (I am simplifying a bit): > > The atomic formula simplifier has some odd policy about deciding between strict (i.e., ">", "<") and weak (i.e. ">=", "<=") orderings to represent certain constraints. That might be tuned to support the quantifier elimination; I would have to look into that in more detail. > > Now x>=2 internally becomes x>1, and "x=1 or x>1" is something obvious to contract by literal comparison of terms. In contrast, x<=5 is *not* turned into x<6, and the possible simplification is not recognised. > > >> I am working in the finite domains (bounded integers) and >> generate lots of combinations of linear inequalities automatically, >> which should be simplified and converted to a normal form to handle >> complexity. >> >> Although Redlog seems to do exactly what I need, it is not too difficult >> to get to the situation where the system eats up all the memory or does >> not seem to finish the computation any time soon. Redlog seems to be >> quite general tool accepting more complex arithmetics and formulas. >> > > Recall that Presburger arithmetic is triply exponential (lower bound on size of the output and thus also on time). > > >> >> Could anybody point to some other tool which seems to be more suitable >> for such tasks? >> > > If you do not use any addition, then software focussing on on discrete orderings might be more efficient. Redlog does not offer this at present. > > 
From: Dr. Thomas Sturm <sturm@re...>  20091116 18:35:56

Am 16.11.2009 um 18:58 schrieb Dr. Thomas Sturm: > The atomic formula simplifier has some odd policy about deciding between strict (i.e., ">", "<") and weak (i.e. ">=", "<=") orderings to represent certain constraints. That might be tuned to support the quantifier elimination; I would have to look into that in more detail. The implementor of PASF has just confirmed that the selection of strong vs. weak orderings is so that the absolute values of the occurring integers are minimised since these are crucial for the complexity of the elimination. So now you at least understand what is going on. Sorry to have no better news.  Thomas Sturm Departamento de Matematicas, Estadistica y Computacion Universidad de Cantabria, Santander, Spain Avda. Los Castros s/n, Room 1072, +34 693 251058 http://personales.unican.es/sturmt/ 
From: Dr. Thomas Sturm <sturm@re...>  20091116 17:58:27

Am 16.11.2009 um 17:25 schrieb Marko Kääramees: > > Hi, > > I use Reduce and its package Redlog for simplifying the boolean > combination of linear inequalities. I found that some quite obvious > simplifications work only one way in the redlog. An example script > > load_package redlog; > rlset pasf; > c := (x = 1 or x >= 2) and (x = 6 or x <= 5); > rlsimpl c; > > simplifies to > > x  1 >= 0 and (x  5 <= 0 or x  6 = 0) > > The first disjunction with >= is simplified, but the other with <= is > not. Could somebody explain the reasons please or guide if it can be > tuned somehow. This indeed puzzled me at first glance. In fact there is no simplification at all implemented that would discover this situation. What happens is the following (I am simplifying a bit): The atomic formula simplifier has some odd policy about deciding between strict (i.e., ">", "<") and weak (i.e. ">=", "<=") orderings to represent certain constraints. That might be tuned to support the quantifier elimination; I would have to look into that in more detail. Now x>=2 internally becomes x>1, and "x=1 or x>1" is something obvious to contract by literal comparison of terms. In contrast, x<=5 is *not* turned into x<6, and the possible simplification is not recognised. > I am working in the finite domains (bounded integers) and > generate lots of combinations of linear inequalities automatically, > which should be simplified and converted to a normal form to handle > complexity. > > Although Redlog seems to do exactly what I need, it is not too difficult > to get to the situation where the system eats up all the memory or does > not seem to finish the computation any time soon. Redlog seems to be > quite general tool accepting more complex arithmetics and formulas. Recall that Presburger arithmetic is triply exponential (lower bound on size of the output and thus also on time). > > Could anybody point to some other tool which seems to be more suitable > for such tasks? If you do not use any addition, then software focussing on on discrete orderings might be more efficient. Redlog does not offer this at present.  Thomas Sturm Departamento de Matematicas, Estadistica y Computacion Universidad de Cantabria, Santander, Spain Avda. Los Castros s/n, Room 1072, +34 693 251058 http://personales.unican.es/sturmt/ 
From: Marko Kääramees <Marko.K<aaramees@tt...>  20091116 16:47:18

Hi, I use Reduce and its package Redlog for simplifying the boolean combination of linear inequalities. I found that some quite obvious simplifications work only one way in the redlog. An example script load_package redlog; rlset pasf; c := (x = 1 or x >= 2) and (x = 6 or x <= 5); rlsimpl c; simplifies to x  1 >= 0 and (x  5 <= 0 or x  6 = 0) The first disjunction with >= is simplified, but the other with <= is not. Could somebody explain the reasons please or guide if it can be tuned somehow. I am working in the finite domains (bounded integers) and generate lots of combinations of linear inequalities automatically, which should be simplified and converted to a normal form to handle complexity. Although Redlog seems to do exactly what I need, it is not too difficult to get to the situation where the system eats up all the memory or does not seem to finish the computation any time soon. Redlog seems to be quite general tool accepting more complex arithmetics and formulas. Could anybody point to some other tool which seems to be more suitable for such tasks? Best regards, marko 
From: Arthur Norman <acn1@ca...>  20091112 09:03:03

On Thu, 12 Nov 2009, Bin Gong wrote: > In old version such as reduce 3.6 or 3.7, sqrt(x^22*x+1) gives the > result abs(x1) correctly, but now it turns out to be x1, no matter I > turn the switch PRECISE on or off. A bunch of us have been having a fairly intensive discussion about this both to try to understand why the behaviour had changed since 3.7 and to ensure that a fix would be a real one rather than a mere patch that dealt with just one case but that risked hurting something elsewhere. I hope that in the next weeks some changes that deal with this are checked in, but as of today I can not give you a reliable time promise. Eg our discussion included the observation that if you think in terms of complex arithmetic the insertion of "abs" is not good, and a number of the reduce subpackages explicitly switch "precise" off while they are doing their stuff. So your comment has been heard! Arthur 
From: Bin Gong <twain@it...>  20091112 08:49:40

Hi everybody, My problem is about the operator "sqrt". In old version such as reduce 3.6 or 3.7, sqrt(x^22*x+1) gives the result abs(x1) correctly, but now it turns out to be x1, no matter I turn the switch PRECISE on or off. If I replace the expression in sqrt into "x^2", it gives "abs(x)" correctly. Reduce (Free PSL version), 12Nov2009 ... 1: sqrt(x^22*x+1); x  1 2: sqrt(x^2); abs(x) Does anyone know how to make the operator work properly in current open source version like in reduce 3.7? I am using a psl build of open source version. Looking forward to your reply. Best regards, Twain 