Proving, Interpolating and Eliminating

The PIE system aims at providing an environment for creating complex applications of automated first-order theorem proving techniques, in examples, experiments, benchmarks, and as background machinery in other contexts.

It support aside of first-order theorem proving in the literal sense also related tasks, in particular

- Formula transformations, for example preprocessing operations
- Interpolant computation
- Second-order quantifier elimination

First-order logic with some second-order extensions seems adequate as a general input and presentation format for formalizations. The system supports this with the following:

- Macros with parameters facilitate stepwise and comprehensible construction of complex formalizations
- A formula pretty printer for a Prolog-based format and for LaTeX helps to produce comprehensible presentations
- LaTeX documents with macro definitions embedded in structuring and explanatory text can be generated from documents written in Prolog syntax, yielding a form of “literal formalizing”
- Second-order extensions of the syntax facilitate expression of certain tasks and are useful for interpolation and elimination

The system is embedded in SWI Prolog and accesses other first-order provers and SAT solvers via interfaces and formats such as TPTP and DIMACS syntax. It also comes with a Prolog-based first-order prover, the CM prover.

The system includes most of the facilities of its predecessor ToyElim, which was based on propositional logic. Envisaged application areas that are made possible specifically through interpolation and elimination are

- Definability and construction of definientia based on interpolation
- Studying and applying variants of circumscription and other forms of nonmonotonic reasoning which can be modeled with second-order operators
- Theory modularizations based on the notion of conservative extension, which can be expressed with second-order quantification

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

Currently a development snapshot is available for download:

- The PIE system (latest
development snapshot)

The following documents are also included in the system archive:- System Version | Changelog | ReadMe | License (GNU GPL)
- The PIE System User/Developer Documentation (Draft)
- Draft Examples
- Further Draft Examples

Contact: info@christophwernhard.com