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


PIE is a Prolog-embedded environment for automated reasoning on the basis of first-order logic. Its main focus is on formulas, as constituents of complex formalizations that are structured through formula macros, and as outputs of reasoning tasks such as second-order quantifier elimination and Craig interpolation. It supports a workflow based on documents that intersperse macro definitions, invocations of reasoners, and LaTeX-formatted natural language text.

The system is written and embedded in SWI-Prolog and provides, essentially as a library of Prolog predicates, functionalities like:

The system is described in more detail in the following papers:


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

Further Applications