The PIE Environment for First-Order-Based
Proving, Interpolating and Eliminating

Overview

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.

The system is written and embedded in SWI-Prolog and provides, essentially as a library of Prolog predicates, functionalities like:

• Support for a Prolog-readable syntax of first-order logic formulas.
• Formula pretty-printing in Prolog syntax and in LaTeX.
• A versatile formula macro processor.
• Support for processing documents that intersperse formula macro definitions, reasoner invocations and LaTeX-formatted natural language text.
• Interfaces to external first-order and propositional provers, including Prover9/Mace4, first-order provers supporting the TPTP format such as E, and SAT solvers like MiniSat.
• The built-in Prolog-based first-order theorem prover CM.
• Implemented reasoning techniques that compute formulas:
  • Second-order quantifier elimination on the basis of first-order logic.
  • Computation of first-order Craig interpolants.
  • Formula conversions for use in preprocessing, inprocessing and output presentation

The system is described in more detail in the following papers:

• Facets of the PIE Environment for Proving, Interpolating and Eliminating on the Basis of First-Order Logic
  Christoph Wernhard
  In Petra Hofstedt et al., editors, Declarative Programming and Knowledge Management (DECLARE 2019), Revised Selected Papers, volume 12057 of LNCS (LNAI), pages 160-177.
  Preprint: https://arxiv.org/pdf/2002.10892.pdf
• The PIE System for Proving, Interpolating and Eliminating
  Christoph Wernhard
  In Pascal Fontaine, Stephan Schulz, and Josef Urban, editors, 5th Workshop on Practical Aspects of Automated Reasoning (PAAR), number 1635 in CEUR Workshop Proceedings, pages 125-138, 2016.

Availability

The PIE system is published as free software under GNU General Public License.

• Obtaining the PIE system
  • By cloning its repository:
    $ git clone http://cs.christophwernhard.com/git/pie.git
  • Or downloading an archive of the latest development snapshot
    
• Direct links to documents included in the distribution
  • System Version | Changelog | ReadMe | License (GNU GPL)
  • The PIE System User/Developer Documentation (Draft)
  • Small examples of PIE documents
    • A small example with Proving, Interpolation and Elimination | (Source)
    • Examples from the DECLARE/WLP 2019 presentation | (Source)
  • A workshop paper written as a PIE document
    • Applying Second-Order Quantifier Elimination in Inspecting Gödel's Ontological Proof
      Christoph Wernhard
      In Renate A. Schmidt, Christoph Wernhard and Yizheng Zhao (eds.): Proceedings of the Second Workshop on Second-Order Elimination and Related Topics, SOQE 2021
      (Preprint (extended version) | Source of all versions)
  • Further PIE example documents that illustrate specific aspects
    • Forgetting and Projection | (Source)
    • Definientia | (Source)
    • Access Predicates via Definientia | (Source)
    • Access Predicates via Definientia – Examples from the Literature | (Source)
    • Orderings | (Source)
    • Virtual Classes | (Source)
    • A Macro for TPTP Problems | (Source)
    • Circumscription and Related Operators | (Source)
    • Conservative Extension | (Source)
• Old versions of the PIE system
  

Further Applications

• Synthesizing Answer Set Programs
  Prototypical implementation of the approach described in Jan Heuer and Christoph Wernhard: Synthesizing Strongly Equivalent Logic Programs: Beth Definability for Answer Set Programs via Craig Interpolation in First-Order Logic, 2024.
• CD Tools
  A Prolog library for experimenting with condensed detachment. Includes the novel specialized provers SGCD and CCS.
• On Circumscription by Walter Forkel
  A new generalization of parallel predicate circumscription, compared with original parallel predicate circumscription and with domain circumscription.

Contact: info@christophwernhard.com