  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. Starting from various examples, the paper discusses features and
application possibilities of PIE along with current limitations and issues for
future research.
