[Axiom-developer] 20080316.02.tpd.patch (CATS verification)

[daly]

CATS (Computer Algebra Test Suite) is an Axiom long term goal intended
to create a set of verified and validated tests for the Axiom
mathematical algorithms. One step toward that goal is to verify and
validate Axiom's results against other computer algebra systems.

This is an initial effort to verify Axiom's results using other 
computer algebra systems. In particular, this patch checks the
results given by Axiom against the results given by Mathematica
for a portion of the differential equation test suite, kamke2.

Tim
=====================================================================
diff --git a/changelog b/changelog
index 443b749..06f1da0 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,4 @@
+20080316 tpd src/input/kamke2.input check results using Mathematica.
 20080316 acr src/algebra/mathml.spad invisibletimes == <mspace width=0.3em>
 20080314 tpd Makefile --enable-maxpage=512*1024 due to kamke2
 20080314 tpd src/input/Makefile add heugcd.input
diff --git a/src/input/kamke2.input.pamphlet b/src/input/kamke2.input.pamphlet
index 2c8be63..7d31b41 100644
--- a/src/input/kamke2.input.pamphlet
+++ b/src/input/kamke2.input.pamphlet
@@ -49,6 +49,11 @@ ode101 := x*D(y(x),x) + x*y(x)**2 - y(x)
 --R                                                     Type: Expression 
Integer
 --E 4
 
+@
+Mathematica gives
+$$y(x)=\frac{2*x}{x^2+2}$$
+which can be substituted and simplifies to 0.
+<<*>>=
 --S 5 of 131
 yx:=solve(ode101,y,x)
 --R
@@ -80,6 +85,12 @@ ode102 := x*D(y(x),x) + x*y(x)**2 - y(x) - a*x**3
 --R                                                     Type: Expression 
Integer
 --E 7
 
+@
+Mathematica gives
+$$\sqrt{a}~x~
+\tanh\left(\frac{1}{2}\left(\sqrt{a}~x^2+2\sqrt{a}~C[1]\right)\right)$$
+which, upon substitution, cannot be simplified to 0.
+<<*>>=
 --S 8 of 131
 yx:=solve(ode102,y,x)
 --R
@@ -202,6 +213,13 @@ ode103 := x*D(y(x),x) + x*y(x)**2 - (2*x**2+1)*y(x) - x**3
 --R                                                     Type: Expression 
Integer
 --E 10
 
+@
+Mathematica gives
+$$\frac{\left(e^{\sqrt{x}~x^2}+\sqrt{2}~e^{\sqrt{2}~x^2}+
+e^{2\sqrt{2}~C[1]}-\sqrt{2}~e^{2\sqrt{2}~C[1]}\right)x}
+{e^{\sqrt{2}~x^2}+e^{2*\sqrt{2}~C[1]}}$$
+which does not simplify to 0 on substitution.
+<<*>>=
 --S 11 of 131
 yx:=solve(ode103,y,x)
 --R
@@ -276,6 +294,11 @@ ode104 := x*D(y(x),x) + a*x*y(x)**2 + 2*y(x) + b*x
 --R                                                     Type: Expression 
Integer
 --E 13
 
+@
+Mathematica gets:
+$$-\frac{1}{ax}-\sqrt{\frac{b}{a}}~\tan\left(a\sqrt{\frac{b}{a}}~x-C[1]\right)$$
+but cannot simplify the substitution to 0.
+<<*>>=
 --S 14 of 131
 yx:=solve(ode104,y,x)
 --R
@@ -368,6 +391,12 @@ ode105 := x*D(y(x),x) + a*x*y(x)**2 + b*y(x) + c*x + d
 --R                                                     Type: Expression 
Integer
 --E 16
 
+@
+Note that this complains about being unable to factor
+$$x^3-3x^2+(-b^2+2b+2)x+b^2-2b$$
+but MMA factors this instantly to be:
+$$-((b-x) (-1+x) (-2+b+x))$$
+<<*>>=
 --S 17 of 131
 yx:=solve(ode105,y,x)
 --R   WARNING (genufact): No known algorithm to factor
@@ -389,6 +418,10 @@ ode106 := x*D(y(x),x) + x**a*y(x)**2 + (a-b)*y(x)/2 + x**b
 --R                                                     Type: Expression 
Integer
 --E 18
 
+@
+Mathematica gets
+$$e^{-\frac{1}{2}a\log(x)+\frac{1}{2}b\log(x)}\tan\left(\frac{2x^{\frac{a+b}{2}}}{a+b}-C[1]\right)$$
+<<*>>=
 --S 19 of 131
 yx:=solve(ode106,y,x)
 --R
@@ -420,7 +453,11 @@ ode108 := x*D(y(x),x) - y(x)**2*log(x) + y(x)
 --R
 --R                                                     Type: Expression 
Integer
 --E 22
-
+@
+Mathematica gets:
+$$\frac{1}{1+xC[1]+\log(x)}$$
+which, on substitution, simplifies to 0.
+<<*>>=
 --S 23 of 131
 yx:=solve(ode108,y,x)
 --R
@@ -455,6 +492,11 @@ ode109 := x*D(y(x),x) - y(x)*(2*y(x)*log(x)-1)
 --R                                                     Type: Expression 
Integer
 --E 25
 
+@
+Mathematica gets
+$$\frac{1}{2+xC[1]+2\log(x)}$$
+which simplifies to 0 on substitution.
+<<*>>=
 --S 26 of 131
 yx:=solve(ode109,y,x)
 --R
@@ -539,6 +581,13 @@ ode113 := x*D(y(x),x) + a*sqrt(y(x)**2 + x**2) - y(x)
 --R                                                     Type: Expression 
Integer
 --E 34
 
+@
+Mathematica gets
+$$x*\sinh(C[1]+\log(x))$$
+If we choose $C[1]=0$ this simplifies to 
+$$\frac{1}{2}(-1+x^2)$$
+However, Mathematica cannot simplify either substition to 0.
+<<*>>=
 --S 35 of 131
 yx:=solve(ode113,y,x)
 --R
@@ -556,6 +605,11 @@ ode114 := x*D(y(x),x) - x*sqrt(y(x)**2 + x**2) - y(x)
 --R                                                     Type: Expression 
Integer
 --E 36
 
+@
+Mathematica gets
+$$x\sinh(x+C[1])$$
+but cannot simplify the substituted expression to 0.
+<<*>>=
 --S 37 of 131
 yx:=solve(ode114,y,x)
 --R
@@ -573,6 +627,10 @@ ode115 := x*D(y(x),x) - x*(y(x)-x)*sqrt(y(x)**2 + x**2) - 
y(x)
 --R                                                     Type: Expression 
Integer
 --E 38
 
+@
+Mathematica claims that the equations appear to involve the variables
+to be solved for in an essentially non-algebraic way.
+<<*>>=
 --S 39 of 131
 yx:=solve(ode115,y,x)
 --R
@@ -590,6 +648,12 @@ ode116 := x*D(y(x),x) - x*sqrt((y(x)**2 - 
x**2)*(y(x)**2-4*x**2)) - y(x)
 --R                                                     Type: Expression 
Integer
 --E 40
 
+@
+Mathematica says that a potential solution of ComplexInfinity was possibly
+discarded by the verifier and should be checked by hand, possibly using
+limits. And the equations appear to involve the variables to be solved
+for in an essentially non-algebraic way.
+<<*>>=
 --S 41 of 131
 yx:=solve(ode116,y,x)
 --R
@@ -608,6 +672,13 @@ ode117 := x*D(y(x),x) - x*exp(y(x)/x) - y(x) - x
 --R                                                     Type: Expression 
Integer
 --E 42
 
+@
+Mathematica says that inverse functions are being used by Solve, so some
+solutions may not be found and to use Reduce for complete solution
+information. It gets the answer:
+$$-x\log\left(-1+\frac{e^{-C[1]}}{x}\right)$$
+which simplifies to 0.
+<<*>>=
 --S 43 of 131
 yx:=solve(ode117,y,x)
 --R
@@ -624,6 +695,13 @@ ode118 := x*D(y(x),x) - y(x)*log(y(x))
 --R                                                     Type: Expression 
Integer
 --E 44
 
+@
+Mathematics gets
+$$e^{e^{C[1]}x}$$
+which, on substitution simplifies to 
+$$e^x(x-\log(e^x))$$ which, if $log(e^x)$ could simplify to $x$
+then the result would be 0.
+<<*>>=
 --S 45 of 131
 yx:=solve(ode118,y,x)
 --R
@@ -654,6 +732,11 @@ ode119 := x*D(y(x),x) - y(x)*(log(x*y(x))-1)
 --R                                                     Type: Expression 
Integer
 --E 47
 
+@
+Mathematica gets
+$$\frac{1}{x(C[1]-log(log(x)))}$$
+which does not simplify to 0 on substitution.
+<<*>>=
 --S 48 of 131
 yx:=solve(ode119,y,x)
 --R
@@ -671,6 +754,10 @@ ode120 := x*D(y(x),x) - y(x)*(x*log(x**2/y(x))+2)
 --R                                                     Type: Expression 
Integer
 --E 49
 
+@
+Mathematics get:
+$$2e^{-e^{-x} C[1]+e^{-x}{\rm ExpIntegralEi}[x]}x$$
+<<*>>=
 --S 50 of 131
 yx:=solve(ode120,y,x)
 --R
@@ -687,6 +774,10 @@ ode121 := x*D(y(x),x) + sin(y(x)-x)
 --R                                                     Type: Expression 
Integer
 --E 51
 
+@
+Mathematics gets
+$$\frac{\sin(x)}{1+\sin(x)}+x^{-sin(x)}C[1]$$
+<<*>>=
 --S 52 of 131
 yx:=solve(ode121,y,x)
 --R
@@ -703,6 +794,11 @@ ode122 := x*D(y(x),x) + 
(sin(y(x))-3*x**2*cos(y(x)))*cos(y(x))
 --R                                                     Type: Expression 
Integer
 --E 53
 
+@
+Mathematica gets:
+$$\arctan\left(\frac{2x^3+C[1]}{2x}\right)$$
+which, on substitution, simplifies to 0.
+<<*>>=
 --S 54 of 131
 yx:=solve(ode122,y,x)
 --R
@@ -719,6 +815,11 @@ ode123 := x*D(y(x),x) - x*sin(y(x)/x) - y(x)
 --R                                                     Type: Expression 
Integer
 --E 55
 
+@
+Mathematica get:
+$$x^{1+sin(x)}C[1]$$
+which does not simplfy to 0 on substitution.
+<<*>>=
 --S 56 of 131
 yx:=solve(ode123,y,x)
 --R
@@ -735,6 +836,11 @@ ode124 := x*D(y(x),x) + x*cos(y(x)/x) - y(x) + x
 --R                                                     Type: Expression 
Integer
 --E 57
 
+@
+Mathematics gets
+$$2x\arctan(C[1]-\log(x))$$
+which does not simplify to 0 on substitution.
+<<*>>=
 --S 58 of 131
 yx:=solve(ode124,y,x)
 --R
@@ -751,6 +857,11 @@ ode125 := x*D(y(x),x) + x*tan(y(x)/x) - y(x)
 --R                                                     Type: Expression 
Integer
 --E 59
 
+@
+Mathematica gets
+$$\arcsin\left(\frac{e^{C[1]}}{x}\right)$$
+which does not simplify to 0 on substitution.
+<<*>>=
 --S 60 of 131
 yx:=solve(ode125,y,x)
 --R
@@ -767,6 +878,11 @@ ode126 := x*D(y(x),x) - y(x)*f(x*y(x))
 --R                                                     Type: Expression 
Integer
 --E 61
 
+@
+Mathematica gets
+$$\frac{1}{-f(x)-C[1]}$$
+which does not simplify to 0 on substitution.
+<<*>>=
 --S 62 of 131
 yx:=solve(ode126,y,x)
 --R
@@ -782,7 +898,10 @@ ode127 := x*D(y(x),x) - y(x)*f(x**a*y(x)**b)
 --R
 --R                                                     Type: Expression 
Integer
 --E 63
-
+@
+Mathematica gives:
+$$b\left(-\frac{f(x^a)}{a}-C[1]\right)^{-1/b}$$
+<<*>>=
 --S 64 of 131
 yx:=solve(ode127,y,x)
 --R
@@ -798,7 +917,10 @@ ode128 := x*D(y(x),x) + a*y(x) - f(x)*g(x**a*y(x))
 --R
 --R                                                     Type: Expression 
Integer
 --E 65
-
+@
+Mathematica gives 
+$$e^{\frac{f(x)g(x^{1+a})}{1+a}-a\log(x)}C[1]$$
+<<*>>=
 --S 66 of 131
 yx:=solve(ode128,y,x)
 --R
@@ -814,7 +936,11 @@ ode129 := (x+1)*D(y(x),x) + y(x)*(y(x)-x)
 --R
 --R                                                     Type: Expression 
Integer
 --E 67
-
+@
+Mathematica gives
+$$-\frac{e^{1+x}}{e^{1+x}-eC[1]-exC[1]-{\rm ExpIntegralEi}(1+x)-
+x{\rm ExpIntegralEi}(1+x)}$$
+<<*>>=
 --S 68 of 131
 yx:=solve(ode129,y,x)
 --R
@@ -837,7 +963,11 @@ ode130 := 2*x*D(y(x),x) - y(x) -2*x**3
 --R
 --R                                                     Type: Expression 
Integer
 --E 69
-
+@
+Mathematica gives
+$$\frac{2x^3}{5}+\sqrt{x}C[1]$$
+which simplifies to 0 on substitution.
+<<*>>=
 --S 70 of 131
 ode130a:=solve(ode130,y,x)
 --R
@@ -873,7 +1003,11 @@ ode131 := (2*x+1)*D(y(x),x) - 4*exp(-y(x)) + 2
 --R
 --R                                                     Type: Expression 
Integer
 --E 73
-
+@
+Mathematica gives
+$$\log\left(2+\frac{1}{1+2x}\right)$$
+which simplifies to 0 when substituted.
+<<*>>=
 --S 74 of 131
 yx:=solve(ode131,y,x)
 --R
@@ -904,7 +1038,13 @@ ode132 := 3*x*D(y(x),x) - 3*x*log(x)*y(x)**4 - y(x)
 --R
 --R                                                     Type: Expression 
Integer
 --E 76
-
+@
+Mathematica gives 3 solutions,
+$$\frac{(-2)^{2/3}x^{1/3}}{(3x^2+4C[1]-6x^2\log(x))^{1/3}}$$
+$$\frac{( 2)^{2/3}x^{1/3}}{(3x^2+4C[1]-6x^2\log(x))^{1/3}}$$
+$$\frac{(-1)^{1/3}2^{2/3}x^{1/3}}{(3x^2+4C[1]-6x^2\log(x))^{1/3}}$$
+which do not simplify to 0 on substitution.
+<<*>>=
 --S 77 of 131
 yx:=solve(ode132,y,x)
 --R
@@ -957,7 +1097,11 @@ ode133 := x**2*D(y(x),x) + y(x) - x
 --R
 --R                                                     Type: Expression 
Integer
 --E 79
-
+@
+Mathematica gets:
+$$e^{1/x}C[1]-e^{1/x}{\rm ExpIntegralEi}\left(-\frac{1}{x}\right)$$
+which simplifies to 0 on substitution.
+<<*>>=
 --S 80 of 131
 yx:=solve(ode133,y,x)
 --R
@@ -983,7 +1127,15 @@ ode134 := x**2*D(y(x),x) - y(x) + x**2*exp(x-1/x)
 --R
 --R                                                     Type: Expression 
Integer
 --E 81
-
+@
+Mathematics get
+$$-e^{-\frac{1}{x}+x}+e^{-1/x}C[1]$$
+which does not simplify to 0 on substitution.
+This is curious because the basis element is the same one
+computed by Axiom, which Axiom cannot simplify either. 
+However, Axiom can simplify the particular element to 0
+and Mathematica cannot.
+<<*>>=
 --S 82 of 131
 ode134a:=solve(ode134,y,x)
 --R
@@ -1021,7 +1173,11 @@ ode135 := x**2*D(y(x),x) - (x-1)*y(x)
 --R
 --R                                                     Type: Expression 
Integer
 --E 85
-
+@
+Mathematica gets 
+$$e^{1/x}xC[1]$$
+which simplifies to 0 when substituted.
+<<*>>=
 --S 86 of 131
 ode135a:=solve(ode135,y,x)
 --R
@@ -1054,7 +1210,11 @@ ode136 := x**2*D(y(x),x) + y(x)**2 + x*y(x) + x**2
 --R
 --R                                                     Type: Expression 
Integer
 --E 89
-
+@
+Mathematica gets
+$$\frac{-x-xC[1]+x\log(x)}{C[1]-\log(x)}$$
+which simplifies to 0 on substition.
+<<*>>=
 --S 90 of 131
 yx:=solve(ode136,y,x)
 --R
@@ -1091,7 +1251,11 @@ ode137 := x**2*D(y(x),x) - y(x)**2 - x*y(x)
 --R
 --R                                                     Type: Expression 
Integer
 --E 92
-
+@
+Mathematica gets:
+$$\frac{x}{C[1]-\log(x)}$$
+which simplifies to 0 on substitution.
+<<*>>=
 --S 93 of 131
 yx:=solve(ode137,y,x)
 --R
@@ -1112,7 +1276,11 @@ ode137expr := x**2*D(yx,x) - yx**2 - x*yx
 --R                                         y(x)
 --R                                                     Type: Expression 
Integer
 --E 94
-
+@
+Mathematica get:
+$$x\tan(C[2]+\log(x))$$
+which simplifies to 0 when substituted.
+<<*>>=
 --S 95 of 131
 ode138 := x**2*D(y(x),x) - y(x)**2 - x*y(x) - x**2
 --R
@@ -1199,7 +1367,11 @@ yx:=solve(ode139,y,x)
 --R   (99)  "failed"
 --R                                                    Type: 
Union("failed",...)
 --E 99
-
+@
+Mathematica gets:
+$$-\frac{2}{x}+\frac{1}{x+C[1]}$$
+which does not simplify.
+<<*>>=
 --S 100 of 131
 ode140 := x**2*(D(y(x),x)+y(x)**2) + 4*x*y(x) + 2
 --R
@@ -1602,7 +1774,11 @@ yx:=solve(ode147,y,x)
 --R   (119)  "failed"
 --R                                                    Type: 
Union("failed",...)
 --E 119
-
+@
+Mathematica gets
+$$\frac{{\rm arcsinh}(x)}{\sqrt{1+x^2}}+\frac{C[1]}{\sqrt{1+x^2}}$$
+gives 0 when substituted.
+<<*>>=
 --S 120 of 131
 ode148 := (x**2+1)*D(y(x),x) + x*y(x) - 1
 --R
@@ -1644,7 +1820,11 @@ ode148expr := (x**2+1)*D(yx,x) + x*yx - 1
 --R   (123)  0
 --R                                                     Type: Expression 
Integer
 --E 123
-
+@
+Mathematica gets
+$$\frac{1}{3}(1+x^2)+\frac{C[1]}{\sqrt{1+x^2}}$$
+which simplifes to 0 when substituted.
+<<*>>=
 --S 124 of 131
 ode149 := (x**2+1)*D(y(x),x) + x*y(x) - x*(x**2+1)
 --R
@@ -1683,6 +1863,11 @@ ode149expr := (x**2+1)*D(yx,x) + x*yx - x*(x**2+1)
 --R                                                     Type: Expression 
Integer
 --E 127
 
+@
+Mathematica gets:
+$$\frac{2x^3}{3(1+x^2)}+\frac{C[1]}{1+x^2}$$
+which simplifies to 0 on substitution.
+<<*>>=
 --S 128 of 131
 ode150 := (x**2+1)*D(y(x),x) + 2*x*y(x) - 2*x**2
 --R
@@ -1727,5 +1912,6 @@ ode150expr := (x**2+1)*D(yx,x) + 2*x*yx - 2*x**2
 \eject
 \begin{thebibliography}{99}
 \bibitem{1} {\bf http://www.cs.uwaterloo.ca/$\tilde{}$ecterrab/odetools.html}
+\bibitem{2} Mathematica 6.0.1.0
 \end{thebibliography}
 \end{document}