[Date Index] [Thread Index] [Author Index]

Re: LessEqual vs Inequality, was ..Re: Replacement Rule with Sqrt in denominator

• To: mathgroup at smc.vnet.net
• Subject: [mg114734] Re: LessEqual vs Inequality, was ..Re: Replacement Rule with Sqrt in denominator
• From: Andrzej Kozlowski <akoz at mimuw.edu.pl>
• Date: Tue, 14 Dec 2010 06:57:33 -0500 (EST)
• References: <ie2971$mqh$1@smc.vnet.net> <4D050013.8050105@cs.berkeley.edu> <928BCB32-AEF9-4D13-87E0-BDDACF1BF878@mimuw.edu.pl> <4D055126.6080209@cs.berkeley.edu> <ie4mt7$9a7$1@smc.vnet.net> <4D0645BE.6000205@cs.berkeley.edu> <7F38BE28-6AE1-4BBC-A115-14B9CA3D9BF0@mimuw.edu.pl> <4D06C7C9.8030803@cs.berkeley.edu>

 Well, you have worn me out, so basically I quit. Not that I agree with 
much. Your long post consist of a mixture of the obvious, which you seem 
to believe is a revelation and other things that reveal your own 
ignorance of Mathematica and even certain areas of algorithmic algebra. 
I will point out just one:
>
> You are asserting that "Refine" can be used.  Thus Refine, in the 
computer algebra terminology, is
> a Zero Equivalence algorithm.   (or a Logical Tautology algorithm, in 
some sense).
>

Not at all. Refine does not deal with logical tautologies or booleans. 
In fact Mathematica has EquivalentQ and Tautology for this purpose:

Equivalent[a && (b || c), a && b || a && c] // TautologyQ

True

What Refine does (Like Simplify and FullSimplify) is to perform 
simplifications of what are called first order formulas in the language 
of real fields with parameters in the real numbers. For example  
x^2>y>z+1 is such a formula and so is
z<y-1<x^2-1. But (x^2>y>z+1) - (z<y-1<x^2-1) is not a forumla but a 
meaningless construct, a kind of accidental consequence of the way 
Mathematica language is constructed. It does not make sense to write

Simplify[x^2>y>z+1 - z<y-1<x^2-1]; even when this sort of thing seems to 
work sometimes, it is by accident (it will work when the two expressions 
that you are subtracting evaluate to the same thing but not otherwise 
since Mathematica will not assign any meaning to the difference. On the 
other hand


Refine[x^2 > y > z, z - 1 < y - 1 < x^2 - 1] &&
 Refine[z - 1 < y - 1 < x^2 - 1, x^2 > y > z]

True

but it is certainly not a "logical tautology" algorithm. It belongs to 
the same "field" as the Tarski-Seidneberg Theorem, Quantifier 
Elimination, Cylindirical ALgebraic Decomposition etc. I am not sure if 
this is "computer science" but there are advantages to an education that 
includes such things which apparently you have not benefitted from.