The ANALYTICA system is a theorem proving system for 19th century mathematics written on top of the Mathematica computer algebra system. It was developed in the early 1990s by X. Zhao and E. Clarke and has since been dormant. We describe recent work to resurrect the theorem prover and port it to newer versions of Mathematica. The new system ANALYTICA 2 can still prove the same theorems, but has been significantly cleaned up. The code has been restructured and documented, the declarative knowledge has been separated from a logical kernel, and the system is being made available as a MATHWEB service.
Proceedings of CALCULEMUS 03, 2003. 5 pages.
PostScript /
PDF
© 2003 Edmund Clarke, Michael Kohlhase, Joël Ouaknine, and
Klaus Sutner.