       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 >= 0 && C >= 0 && i == 1 + C &&
N == 1 + C + C && iP == 1 + C + C && jP == j - C,
{iP, jP}, Integers]

Element[C | C | C | C | C, Integers] &&
C >= 0 && C >= 0 && C >= 0 && C >= 0 &&
C >= 0 && i == C + 1 &&
N == C + C + C + 1 && C == C &&
C == C + C && iP == C + C + C +
1 && j == C + C - C &&
jP == -C + C - C

This tells you that all solutions over the integers can be found by
choosing any non-negative C,C...C 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 + 1 && N == C + C + C + 1 &&
C == C && C == C + C &&
iP == C + C + C + 1 && j == C + C - C &&
jP == -C + C - C, 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, C},
>   Element[{C, C}, Reals] && C >= 0 && C >= 0 && i == 1 +
> C &&
>    N == 1 + C + C &&
>         iP == 1 + C + C && jP == j - C], {iP, jP},
>  Backsubstitution -> True],
> Element[C | C | 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, C},
>   Element[{C, C}, Integers] && C >= 0 && C >= 0 &&
>    i == 1 + C && N == 1 + C + C && iP == 1 + C + C &&
>    jP == j - C];
>
> 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[]]]
> True
>
> In fact, you can simply what C and C must be, treating the
> condition as a linear system of  equations and inequalities:
>
> Reduce[C >= 0 && C >= 0 && i == 1 + C && N == 1 + C +
> C &&
>  iP == 1 + C + C && jP == j - C && sols[], {C, C,
> iP,
>  jP}, Reals,
>   Backsubstitution -> True]
>
> N == 1 && i == 1 && C == 0 && C == 0 && iP == 1 && jP == j
>
> From which you can see that C and C 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 and C:
>
> Reduce[C >= 0 && C >= 0 && i == 1 + C && N == 1 + C +
> C &&
>  iP == 1 + C + C && jP == j - C && sols[], {C, C,
> iP,
>  jP}, Reals,
>   Backsubstitution -> True]
>
> N > 1 && 1 <= i <= N && C == i - 1 && C == N - i && iP == N &&
> jP == i + j - N
>
>
> This again shows you that provided both N and i are integers, C
> and C 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:= Reduce[Exists[{C, C},
>> Element[{C, C}, Integers] && C >= 0 && C >= 0 &&
>>  i == 1 + C && N == 1 + C + C && iP == 1 + C + C &&
>>  jP == j - C], {iP, jP}, Backsubstitution -> True]
>>
>> During evaluation of In:= Reduce::nsmet: This system cannot be
>> solved with the methods available to \
>> Reduce. >>
>>
>> I have observed that when I remove Element[{C, C}, Integers]
>> && C
>>  >= 0 && C >= 0 like that:
>> In:= Reduce[
>> Exists[{C, C},
>> i == 1 + C && N == 1 + C + C && iP == 1 + C + C &&
>>  jP == j - C], {iP, jP}, Backsubstitution -> True]
>>
>> it gives me an output which is:
>>
>> Out= iP == N && jP == i + j - N
>>
>>
>> I need to keep the information that Element[{C, C}, Integers]
>> &&
>> C >= 0 && C >= 0  but reduce tells me that it cannot solve this
>> system. why and how to deal with this problem?
>> thank you.
>>
>

```

• Prev by Date: Re: problem with reduce
• Next by Date: Re: RandomReal gets stuck
• Previous by thread: Re: problem with reduce
• Next by thread: Re: problem with reduce