The PIE Environment for First-Order-Based
Proving, Interpolating and Eliminating


The PIE system aims at providing an environment for creating complex applications of automated first-order theorem proving techniques, in examples, experiments, benchmarks, and as background machinery in other contexts.

It support aside of first-order theorem proving in the literal sense also related tasks, in particular

First-order logic with some second-order extensions seems adequate as a general input and presentation format for formalizations. The system supports this with the following:

The system is embedded in SWI Prolog and accesses other first-order provers and SAT solvers via interfaces and formats such as TPTP and DIMACS syntax. It also comes with a Prolog-based first-order prover, the CM prover.

The system includes most of the facilities of its predecessor ToyElim, which was based on propositional logic. Envisaged application areas that are made possible specifically through interpolation and elimination are


The PIE system is published as free software under GNU General Public License.

Currently a development snapshot is available for download: