The PIE Environment
for FirstOrderBased
Proving, Interpolating and
Eliminating
Overview
The PIE system aims at providing an environment for creating
complex applications of automated firstorder theorem proving techniques, in
examples, experiments, benchmarks, and as background machinery in other
contexts.
It support aside of firstorder theorem proving in the literal sense
also related tasks, in particular
 Formula transformations, for example
preprocessing operations
 Interpolant computation
 Secondorder quantifier elimination
Firstorder logic with some secondorder
extensions seems adequate as a general input and presentation
format for formalizations. The system supports this with the
following:
 Macros with parameters facilitate
stepwise and comprehensible construction of complex formalizations
 A formula pretty printer for a Prologbased
format and for LaTeX helps to produce
comprehensible presentations
 LaTeX documents with macro definitions embedded in
structuring and explanatory text can be generated from documents written in Prolog syntax, yielding
a form of “literal formalizing”
 Secondorder extensions of the syntax
facilitate expression of certain tasks and are useful for interpolation
and elimination
The system is embedded in SWI Prolog and
accesses other firstorder provers and SAT solvers via interfaces and
formats such as TPTP and DIMACS
syntax. It also comes with a Prologbased firstorder 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
 Definability and construction of definientia based on
interpolation
 Studying and applying variants of circumscription and other forms
of nonmonotonic reasoning which can be modeled with secondorder
operators
 Theory modularizations based on the notion of conservative
extension, which can be expressed with secondorder quantification
The system is described in more detail in

Christoph Wernhard
In
Pascal Fontaine, Stephan Schulz, and Josef Urban, editors,
5th
Workshop on Practical Aspects of Automated Reasoning (PAAR),
number 1635 in
CEUR Workshop Proceedings, pages
pages 125138, Aachen, 2016.
Availability
The PIE system is published as free
software under GNU General Public
License.
Applications
 On
Circumscription by Walter Forkel
A new generalization of
parallel predicate circumscription, compared with original
parallel predicate circumscription and with domain
circumscription.
Contact: info@christophwernhard.com