Facets of the PIE Environment for Proving, Interpolating and Eliminating on the Basis of First-Order Logic
This tool addresses the need for structured automated reasoning workflows in formal logic, but it is incremental as it builds on existing Prolog and logic frameworks.
The paper introduces PIE, a Prolog-embedded environment for automated reasoning in first-order logic, focusing on formula manipulation for tasks like second-order quantifier elimination and Craig interpolation, and demonstrates its features through examples while noting current limitations.
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.