## 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.

- Completely modular
- 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

- libxml2 (at least version 2.6.7)
- libxml++2 (minimum version 2.10)
- The Spirit parsing framework (minimum version 1.8.5 miniboost)
- CERes

Download alpha 3 of ATP here.

- ATP depends on an existing installation of CERes. Please update configure.ac file to point to the src folder of CERes (CERES_SRC_ROOT)
- Please also apdate the Spirit framework installation directory in configure.ac (SPIRIT_ROOT)
- ./builconf.sh
- ./configure
- make
- The executable is Prover/src/Prover

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.## Showcase

ATP will read the file and display (in prolog notation) the 3 clauses together with indices:

(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.
## Documentation

## Links

## Contact

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`