factorials and binomials simplification - nusum less verbose

The explanations are as you say.

 

I think the interplay between  theorem prover and  CAS  can be at several
levels.

For most people using/writing CAS, the fact that the CAS produced the answer
is, in effect, a constructive proof that the answer is correct.  (Otherwise
the CAS has a bug, which is possible of course, but not very likely if all
that it is doing is, say, polynomial arithmetic). Seeing that HOL cannot
confirm the result doesn't mean it is incorrect. Seeing that HOL confirms
the result means it is correct (Or --- there is a bug in HOL which is
possible too!).

 

 

The more interesting use, to me, is where the CAS is used as a repository of
"advanced" axioms. For example, what can one do with a system that knows
(essentially as an axiom), not only all of arithmetic, but also facts like
lim(sin(x)/x, x,0)=1.

 

Any use of HOL + Maxima is nice to learn about though. Good luck.

RJF

  _____  

From: maxima-admin at math.utexas.edu [mailto:maxima-admin at math.utexas.edu] On
Behalf Of giovanni gherdovich
Sent: Tuesday, July 11, 2006 10:57 AM
To: maxima at math.utexas.edu
Subject: Re: [Maxima] factorials and binomials simplification - nusum less
verbose

 

Thankyou Richard and Robert, you answered completely to my questions.

>matchdeclare([a,b],true);
>defrule(h,binomial(a,b),(a+b)!/a!/b!);
>apply1(., h);
>minfactorial(%);

>will simplify the example you give, 

Just for the sake of understanding:

matchdeclare([a,b],true);

This command makes Maxima able to apply the following rule

defrule(h,binomial(a,b),(a+b)!/a!/b!);

wherever it finds something like "binomial(n,k)", whatever the domain of n
and k is, isn't it?

>> I'd like to avoid the string "Dependent equations eliminated: (1)".
>From looking at the code from which that message originates
>(src/solve.lisp),
>it appears that linsolvewarn : false; should disable that message.
>I didn't try that.

Yes, the command 
linsolvewarn:false
makes the linear solver silent, and it's what I want.

>> I'm using Maxima within the theorem prover Hol Light, through an
>>interface
>> written by John Harrison.

>Hmm, that sounds interesting. Maybe you can tell us more about this.

A theorem prover, like Hol Light, is (roughly speaking) a programming
language in wich the code you write is a mathematical proof. If the code
runs, the proof was correct and you get a theorem (if you agree with the Hol
axioms!).
But it cannot find any result by itself, it can only check if a result is
correct (producing a formal proof of it).
So it's very different from a Computer Algebra System, wich can find the
answers, but without giving the proofs.
A very interesting mix is ask Maxima for the answers, and then check them by
Hol to get formal theorems.
I was encouraged to this approach by the last chapter of the Hol Tutorial
(page 206), http://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial_220.pdf , were
I found the interface I'm using.

Thankyou again.

Giovanni Gherdovich

 Chiacchiera con i tuoi amici in tempo reale! 
http://it.yahoo.com/mail_it/foot/*http://it.messenger.yahoo.com