TU Logo

Interactive Modular Automated Theorem Prover (ATP) Homepage

ATP is a modular theorem prover which aims on enabling the user to have more control on the computation process, enabling him 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 level.

NEW! ATP is being redeveloped within the General Architecture for Proofs Framework based on the Scala programming language.




Download alpha 3 of ATP here.



Please add the following text into a file called input_file:
p(a). -p(x) | p(f(x)). -p(f(f(a))).
ATP will read the file and display (in prolog notation) the 3 clauses together with indices:
(0) :- p(a)
(1) p(x) :- p(f(x))
(2) p(f(f(a))) :-
Enter tX for automated X steps, sX for displaying all clauses containing X or Please choose two clauses to process:

Now, it is possible either to apply it automatically for X steps using the notation tX or apply resolution/paramodulation on two selected clauses.


The application of CERes to the Prime proof examples required the refutation of an unsatisfiable clause set extracted from the proof. This refutation proved to be impossible to attain using several well known compeletely automatic theorem provers (Otter and Prover9) already on the case of 2 primes, due to its large size. In order to apply CERes on the proof, a partial refutation was created by hand[CERES: An analysis of Fürstenberg's proof of the infinity of primes]. The following report describes the interactive process of validating and completing this manually obtained refutation using ATP for the case of 3 primes.


Please refer to the user manual for more information.


  • Proof Tool is a viewer for LK proofs.
  • CERES is a tool for automated proof analysis.


If you have any questions, feel free to contact us: shaolin |@| logic |.| at

Valid CSS! Valid XHTML 1.1 Viewable With Any Browser