10.1184/R1/6610202.v1 Edmund M Clarke Edmund M Clarke Michael Kohlhase Michael Kohlhase Joel Ouaknine Joel Ouaknine Klaus Sutner Klaus Sutner System Description: Analytica 2 Carnegie Mellon University 2007 computer sciences 2007-03-01 00:00:00 Journal contribution https://kilthub.cmu.edu/articles/journal_contribution/System_Description_Analytica_2/6610202 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 1990's 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.