
Re: can your CAS help proving inequalities?
Posted:
Mar 10, 2013 1:57 PM


"Nasser M. Abbasi" schrieb: > > On 3/9/2013 6:07 AM, A N Niel wrote: > > > > What CAS did you use, and what does {} mean for it? > > > > Mathematica. It has a special command called > > "FindInstance[expr, vars] > > finds an instance of vars that makes the statement expr be True. > gives results in the same form as Solve: if an instance exists, > and {} if it does not. " > > http://reference.wolfram.com/mathematica/ref/FindInstance.html > > So that is what I used: > >  > Remove["Global`*"] > r[a_, b_, c_, d_] := (a  c)*(a  d)*(b  c)*(b  d) > s[a_, b_, c_, d_] := (a + b)*(c + d)  2*(a*b + c*d)  > Abs[(a  b)*(c  d)] > t[a_, b_, c_, d_] := (a + b)*(c + d)  2*(a*b + c*d) + > Abs[(a  b)*(c  d)] >  > > and now > >  > FindInstance[ > Min[r[a, b, c, d], r[a, c, b, d], r[a, d, c, b]] > 0, {a, b, c, d}] > > {} > > FindInstance[ > Min[r[a, b, c, d], r[a, c, b, d], r[a, d, c, b]] > 0, {a, b, c, d}] > > {} > > FindInstance[ > Min[t[a, b, c, d], t[a, c, b, d], t[a, d, c, b]] > 0, {a, b, c, d}] > > {} >  > > But I was not sure this qualifies as "proof" that is why I asked > first. >
Since the Mathematica variables are complex by default, they must here perhaps be explicitly restricted to real. Judging form the "Notes On Internal Implementation" it looks like Mathematica's Reduce[] might be able to do reduce such inequalities: among other techniques, it fields cylindrical algebraic decomposition (CAD).
Martin.

