pietercollins
commented
4 years ago We could try systems where the solution is a polynomial, since here at some point the remainder is zero, and maybe CORA misses this. However, then the right-hand-side is non-polynomial
e.g.dx/dt=sqrt(x), x(0)=1 has solution x=4t^2
Alternatively, we could try a polynomial right-hand-side
e.g. dx/dt=-x^2, x(0)=1 has solution x=1/(1+t)
or both
e.g. dx/dt=x-t, x(0)=1 has solution x=t+1
Compare the results obtained from CORA, which is non-rigorous, and Ariadne. AIm to show CORA makes (truncation and roundoff) errors, but Ariadne always gives correct bounds for the result.