PIE -- Proving, Interpolating and Eliminating on the Basis of First-Order Logic
This provides a specialized tool for researchers and practitioners in automated reasoning and logic, but it is incremental as it builds upon existing Prolog and first-order logic methods.
The authors tackled the problem of automated reasoning in first-order logic by developing PIE, a Prolog-embedded environment that integrates macro definitions, reasoner invocations, and LaTeX-formatted text, resulting in a versatile tool supporting external provers and subsystems for tasks like proving, interpolation, and quantifier elimination.
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.