Re: LessEqual vs Inequality, was ..Re: Replacement Rule with Sqrt in denominator
- To: mathgroup at smc.vnet.net
- Subject: [mg114752] Re: LessEqual vs Inequality, was ..Re: Replacement Rule with Sqrt in denominator
- From: Richard Fateman <fateman at cs.berkeley.edu>
- Date: Wed, 15 Dec 2010 07:53:00 -0500 (EST)
On 12/14/2010 3:57 AM, Andrzej Kozlowski wrote:
> 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.
No, just in some sense.
Refine does not deal with logical tautologies or booleans.
A zero-equivalence algorithm traditionally
tests to see if f1(x,y,..) - f2(x,y,...) is zero for all possible
values of x,y, ....
TautologyQ should be able to test to see if f1(x,y,...) == f2(x,y, ...)
is True for all possible values of x,y, ... in the set {True,False}.
Mathematica is somehow being more sensitive to types here in not
permitting a==b, but requiring the syntax Equivalent[a,b].
So TautologyQ[Equivalent[a,b]] is a zero equivalence algorithm, in some
sense, but for logical expressions. Which is what I said.
[It is trivial in some sense, since one can compute a table of 2^n
entries, where there are n variables. But clearly this method takes
time exponential in n.]
If you were familiar with the terminology of simplification, canonical
forms, zero-equivalence algorithms, the analogy might make sense to
you too.
In answer to another item: Quantifier elimination and cylindrical
algebraic decomposition are not usually part of the undergraduate
curriculum in computer science or mathematics. Depending on
specialization, they may or may not be part of graduate programs either.
A computer scientist studying computer algebra systems would probably
encounter these topics, but even so, might avoid them.
As for whether something is meaningless to Mathematica or not, or
whether Mathematica computes something "by accident", that is a
philosophical issue. My view is that nothing that is computed
deterministically is "by accident". And everything is
meaningless to Mathematica. It is just a program
that is pushing bits around.
Glad to hear I've worn you down. I was about to quit :)
RJF
> 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.
>
>