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.