Analytica is a theorem prover written in Mathematica. It was developed by prof. Edmund Clarke and Xudong Zhao.

Download Analytica here (hold the Shift key while you click on the link).

This version will run on Mathematica 2.0 and with minor modifications on 3.0. It writes typeset proofs into TeX files "outXX.tex" which you can view with a TeX previewer.

You can start up Analytica by loading the file "index.all" with the Mathematica command "<<index.all".

Examples are in the subdirectory examples.