The PIE Environment
Proving, Interpolating and
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
- Support for a Prolog-readable syntax
of first-order logic formulas.
- Formula pretty-printing in
Prolog syntax and in LaTeX.
- A versatile formula macro
- Support for processing
documents that intersperse formula macro
definitions, reasoner invocations and LaTeX-formatted natural
- Interfaces to external first-order
and propositional provers,
first-order provers supporting
the TPTP format such
as E, and SAT solvers
- The built-in Prolog-based
- Implemented reasoning techniques that compute
- Second-order quantifier
elimination on the basis of first-order logic.
- Computation of first-order Craig interpolants.
- Formula conversions for
use in preprocessing, inprocessing and output presentation
The system is described in more detail in the following papers:
Salvador Abreu, Petra Hofstedt, Ulrich John, Herbert Kuchen, and
Dietmar Seipel, editors, Declarative Programming and Knowledge
Management (DECLARE 2019), Revised Selected Papers, LNCS
(LNAI), 2020. To appear.
The PIE system is published as
software under GNU General Public
Circumscription by Walter Forkel
A new generalization of
parallel predicate circumscription, compared with original
parallel predicate circumscription and with domain