# Facets of the PIE Environment for Proving, Interpolating and Eliminating on the Basis of First-Order Logic

arXiv: https://arxiv.org/abs/2002.10892 · HTML: https://mlsanity.com/paper/2002.10892/

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 24 Feb 2020.

## Built on by (most cited first, 6 of 6)

- [Learning from Lukasiewicz and Meredith: Investigations into Proof Structures (Extended Version)](https://mlsanity.com/paper/2104.13645/) (2021)
- [CD Tools -- Condensed Detachment and Structure Generating Theorem Proving (System Description)](https://mlsanity.com/paper/2207.08453/) (2022)
- [Lemmas: Generation, Selection, Application](https://mlsanity.com/paper/2303.05854/) (2023)
- [Generating Compressed Combinatory Proof Structures -- An Approach to Automated First-Order Theorem Proving](https://mlsanity.com/paper/2209.12592/) (2022)
- [Applying Second-Order Quantifier Elimination in Inspecting G"odel's Ontological Proof](https://mlsanity.com/paper/2110.11108/) (2021)
- [Range-Restricted Interpolation through Clausal Tableaux](https://mlsanity.com/paper/2306.03572/) (2023)

## Abstract (arXiv)

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.