ATP (Automated Theorem Prover) is a free and open-source modular theorem prover designed to enable you to have more control on the computation process.
ATP allows you to switch between automatic and manual sessions easily. The modularity of the prover makes it possible to extend it both on the control level and on the algorithmic leve.
ATP is cross-platform and it works on Mac OS X, Windows and Linux.
Here are some key features of "ATP":
· Capable of supporting type theory
· The different components are wired together using a startup xml file
· Supports simple interaction with the user
· Contains a simple command input support which can be extended into a full UI
· Has implementations for several factorization and paramodulation approaches
· Supports easily extendable refinements
· The output is in the proofdatabase XML format and can be visualized using ProofTool
Requirements:
· Java
Find us on Google+
