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.