PIE -- Proving, Interpolating and Eliminating on the Basis of First-Order Logic

TL;DR

PIE is an integrated Prolog environment for automated first-order logic reasoning, supporting macro systems, multiple reasoners, and document generation with LaTeX and natural language.

Contribution

It introduces a versatile macro system and integrates various reasoners, including external provers and specialized modules, within a Prolog-based environment.

Findings

Supports multiple reasoners including external and internal provers

Enables creation of documents with embedded reasoning and LaTeX text

Provides tools for Craig interpolation and second-order quantifier elimination

Abstract

PIE is a Prolog-embedded environment for automated reasoning on the basis of first-order logic. It includes a versatile formula macro system and supports the creation of documents that intersperse macro definitions, reasoner invocations and LaTeX-formatted natural language text. Invocation of various reasoners is supported: External provers as well as sub-systems of PIE, which include preprocessors, a Prolog-based first-order prover, methods for Craig interpolation and methods for second-order quantifier elimination.