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:
Petra Hofstedt et al., editors, Declarative Programming and Knowledge
Management (DECLARE 2019), Revised Selected Papers
, volume 12057 of LNCS
(LNAI), pages 160-177.
The PIE system is published as
software under GNU General Public
- Synthesizing Answer Set Programs
Prototypical implementation of the approach described in Jan Heuer
and Christoph Wernhard: Synthesizing Strongly Equivalent Logic
Programs: Beth Definability for Answer Set Programs via Craig
Interpolation in First-Order Logic, 2024.
A Prolog library for experimenting with condensed
detachment. Includes the novel specialized provers SGCD and CCS.
Circumscription by Walter Forkel
A new generalization of
parallel predicate circumscription, compared with original
parallel predicate circumscription and with domain