Re: How can I make FullSimplify work for user-defined functions?
- To: mathgroup at smc.vnet.net
- Subject: [mg52603] Re: [mg52569] How can I make FullSimplify work for user-defined functions?
- From: Andrzej Kozlowski <akoz at mimuw.edu.pl>
- Date: Fri, 3 Dec 2004 03:54:45 -0500 (EST)
- References: <79344CBB6297454F86DD3106ADCC76CC82F077@mail3.nwfwmd.state.fl.us>
- Sender: owner-wri-mathgroup at wolfram.com
On 2 Dec 2004, at 23:55, Gilmar Rodriguez wrote:
>
>> It's simply that FullSimplify knows nothing at all about Prime or
>> PrimePi
>> and can't decide even the simplest facts about them, for example:
>
>
> FullSimplify must know something about primes since:
>
> FullSimplify[Prime[n] ? 1 + (3n + n^2)/4, Element[n, Integers] && n ?
> 1]
> Gives "True" as an answer.
Yes, it does know some isolated facts (in fact more than I expected)
but that was not really my point. It still can't "manipulate" such
facts, which is what you want. For example just replace n by n+1 in the
above formula
FullSimplify[Prime[n + 1] <=
1 + (3*(n + 1) + (n + 1)^2)/4, Element[n, Integers] && n >= 2]
4 Prime[n+1]â?¤n (n+5)+8
It is easy to add any number of simple rules to Simplify and
FullSimplify but that will not do much for you unless they can be
combined wiht other rules in a useful way to lead to results that are
not entirely obvious.
>
>> You can use Mathematica to answer questions about concrete integers,
>> but it won't prove any theorems for you.
>
> Mathematica might be capable (in the future) of proving theorems, or
> detecting errors in a logical argument in the future. A lot of effort
> is been contributed by a lot of researchers to build meta-programs
> that examine the logical sentences in the body of a Mathematical
> proof, to detect flaws in it.
Mathematica can of course already do this for certain type of
statements, basically those that can be reduced to an algebraic
inequality. A trivial example:
Simplify[n^2>2m+1,n>m&&n>2]
True
or
Resolve[ForAll[n, n â?? Reals, Exists[m, m â?? Reals,
m < n + 1]]]
True
and one can do even more (well, one would hope so!) like finding
limits using the epsilon-delta approach in the case of rational
functions. But as I wrote, there are not enough general algorithmic
rules of this kind for dealing with primes for this sort of thing to be
useful.
As for the latest research on "examine the logical sentences in the
body of a mathematical proof", I am quite aware of its existence but I
have not heard of anything that would be significantly useful in a
general purpose program like Mathematica. Implementing anything has a
cost and the pleasure of seeing a computer program do something that
you could almost equally easily do yourself does nto really justify
this cost.
Andrzej Kozlowski
Chiba, Japan
http://www.akikoz.net/~andrzej/
http://www.mimuw.edu.pl/~akoz/