Re: problem with reduce

*To*: mathgroup at smc.vnet.net*Subject*: [mg100400] Re: [mg100347] problem with reduce*From*: Andrzej Kozlowski <akoz at mimuw.edu.pl>*Date*: Tue, 2 Jun 2009 06:48:28 -0400 (EDT)*References*: <200906011111.HAA26170@smc.vnet.net> <4796F603-A315-46FF-B212-4FA8EEF8477C@mimuw.edu.pl>

After posting the message below I noticed that there is also another way (requiring, perhaps, a bit less less user intervention). Reduce[C[1] >= 0 && C[2] >= 0 && i == 1 + C[1] && N == 1 + C[1] + C[2] && iP == 1 + C[1] + C[2] && jP == j - C[2], {iP, jP}, Integers] Element[C[3] | C[4] | C[5] | C[6] | C[7], Integers] && C[3] >= 0 && C[4] >= 0 && C[5] >= 0 && C[6] >= 0 && C[7] >= 0 && i == C[3] + 1 && N == C[3] + C[4] + C[5] + 1 && C[1] == C[3] && C[2] == C[4] + C[5] && iP == C[3] + C[4] + C[5] + 1 && j == C[5] + C[6] - C[7] && jP == -C[4] + C[6] - C[7] This tells you that all solutions over the integers can be found by choosing any non-negative C[3],C[4]...C[7] and defining the values of the variables in terms of them. You can now find the relationship between the variables eliminating the C[i]: Eliminate[i == C[3] + 1 && N == C[3] + C[4] + C[5] + 1 && C[1] == C[3] && C[2] == C[4] + C[5] && iP == C[3] + C[4] + C[5] + 1 && j == C[5] + C[6] - C[7] && jP == -C[4] + C[6] - C[7], Table[C[i], {i, 1, 7}]] i == iP - j + jP && iP == N Andrzej Kozlowski On 1 Jun 2009, at 22:42, Andrzej Kozlowski wrote: > First the reason. This is an example of what is called "quantifier > elimination" (in this case one eliminates the quantifier Exists). > Algorithms for quantifier elimination exist only for polynomial > formulas with real number coefficients (or more generally with > coefficients in real closed fields). This was first shown by the > Polish logician Alfred Tarski, although modern algorithms are much > faster. However, there is no algorithm for quantifier elimination > over the integers. It's not just that one is now known, we know that > there cannot be any general algorithm. Mathematica can, however, do > this in certain special cases by using heuristic methods. > > However, since everything in your system is linear, you can simply > eliminate quantifiers over the reals and then add Simplify using the > assumption that everything is an integer: > > > sols=Simplify[Reduce[ > Exists[{C[1], C[2]}, > Element[{C[1], C[2]}, Reals] && C[1] >= 0 && C[2] >= 0 && i == 1 + > C[1] && > N == 1 + C[1] + C[2] && > iP == 1 + C[1] + C[2] && jP == j - C[2]], {iP, jP}, > Backsubstitution -> True], > Element[C[1] | C[2] | i | j | N | iP | jP, Integers]] > > (N == 1 && i == 1 && iP == 1 && j == jP) || (N > 1 && 1 <= i <= N && > iP == N && > i + j == jP + N) > > > Lets now try to check if these really satisfy the original > conditions. First, the original conditions (over the Integers) were: > > cond = Exists[{C[1], C[2]}, > Element[{C[1], C[2]}, Integers] && C[1] >= 0 && C[2] >= 0 && > i == 1 + C[1] && N == 1 + C[1] + C[2] && iP == 1 + C[1] + C[2] && > jP == j - C[2]]; > > It is easy to verify that the first solution N == 1 && i == 1 && iP > == 1 && j == jP is a solution because now quantifier elimination > over the integers has become trivial: > > Reduce[cond /. ToRules[sols[[1]]]] > True > > In fact, you can simply what C[1] and C[2] must be, treating the > condition as a linear system of equations and inequalities: > > Reduce[C[1] >= 0 && C[2] >= 0 && i == 1 + C[1] && N == 1 + C[1] + > C[2] && > iP == 1 + C[1] + C[2] && jP == j - C[2] && sols[[1]], {C[1], C[2], > iP, > jP}, Reals, > Backsubstitution -> True] > > N == 1 && i == 1 && C[1] == 0 && C[2] == 0 && iP == 1 && jP == j > > From which you can see that C[1] and C[2] are both zero, and zero > is, of course, an integer. So we are sure we have one solution: > > N == 1 && i == 1 && iP == 1 && jP==j > > > In the other case, Reduce still cannot prove that a solution exists > if we try quantifier eleimination, but you can simply again consider > everything as a linear system and find C[1] and C[2]: > > Reduce[C[1] >= 0 && C[2] >= 0 && i == 1 + C[1] && N == 1 + C[1] + > C[2] && > iP == 1 + C[1] + C[2] && jP == j - C[2] && sols[[2]], {C[1], C[2], > iP, > jP}, Reals, > Backsubstitution -> True] > > N > 1 && 1 <= i <= N && C[1] == i - 1 && C[2] == N - i && iP == N && > jP == i + j - N > > > This again shows you that provided both N and i are integers, C[1] > and C[2] will also be integers, so the system has actually been > solved over the integers. So the second solution you want can be > written > > > Element[N, Integers] && Element[i, Integers] && N > 1 && 1 <= i <= > N && iP == N && jP == i + j - N > > > Andrzej Kozlowski > > On 1 Jun 2009, at 20:11, olfa wrote: > >> Hi mathematica community, >> I have to solve this example >> In[88]:= Reduce[Exists[{C[1], C[2]}, >> Element[{C[1], C[2]}, Integers] && C[1] >= 0 && C[2] >= 0 && >> i == 1 + C[1] && N == 1 + C[1] + C[2] && iP == 1 + C[1] + C[2] && >> jP == j - C[2]], {iP, jP}, Backsubstitution -> True] >> >> During evaluation of In[88]:= Reduce::nsmet: This system cannot be >> solved with the methods available to \ >> Reduce. >> >> >> I have observed that when I remove Element[{C[1], C[2]}, Integers] >> && C >> [1] >= 0 && C[2] >= 0 like that: >> In[89]:= Reduce[ >> Exists[{C[1], C[2]}, >> i == 1 + C[1] && N == 1 + C[1] + C[2] && iP == 1 + C[1] + C[2] && >> jP == j - C[2]], {iP, jP}, Backsubstitution -> True] >> >> it gives me an output which is: >> >> Out[89]= iP == N && jP == i + j - N >> >> >> I need to keep the information that Element[{C[1], C[2]}, Integers] >> && >> C[1] >= 0 && C[2] >= 0 but reduce tells me that it cannot solve this >> system. why and how to deal with this problem? >> thank you. >> >

**References**:**problem with reduce***From:*olfa <olfa.mraihi@yahoo.fr>

**Re: problem with reduce**

**Re: RandomReal gets stuck**

**Re: problem with reduce**

**Re: problem with reduce**