The PIE Environment
for FirstOrderBased
Proving, Interpolating and
Eliminating
Overview
PIE is a Prologembedded environment for automated reasoning on the
basis of firstorder 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 secondorder
quantifier elimination and Craig interpolation. It supports a workflow
based on documents that intersperse macro definitions, invocations
of reasoners, and LaTeXformatted natural language text.
The system is written and embedded
in SWIProlog and provides,
essentially as a library of Prolog predicates, functionalities
like:
 Support for a Prologreadable syntax
of firstorder logic formulas.
 Formula prettyprinting in
Prolog syntax and in LaTeX.
 A versatile formula macro
processor.
 Support for processing
documents that intersperse formula macro
definitions, reasoner invocations and LaTeXformatted natural
language text.
 Interfaces to external firstorder
and propositional provers,
including Prover9/Mace4,
firstorder provers supporting
the TPTP format such
as E, and SAT solvers
like MiniSat.
 The builtin Prologbased
firstorder theorem
prover CM.
 Implemented reasoning techniques that compute
formulas:
 Secondorder quantifier
elimination on the basis of firstorder logic.
 Computation of firstorder Craig interpolants.
 Formula conversions for
use in preprocessing, inprocessing and output presentation
The system is described in more detail in the following papers:

Christoph Wernhard
In
Petra Hofstedt et al., editors,
Declarative Programming and Knowledge
Management (DECLARE 2019), Revised Selected Papers, volume 12057 of LNCS
(LNAI), pages 160177.
Preprint:
https://arxiv.org/pdf/2002.10892.pdf

Christoph Wernhard
Availability
The PIE system is published as
free
software under GNU General Public
License.
Further Applications
 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 FirstOrder Logic, 2024.
 CD
Tools
A Prolog library for experimenting with condensed
detachment. Includes the novel specialized provers SGCD and CCS.
 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