PIE -- Proving, Interpolating and Eliminating on the Basis of First-Order Logic
Artificial Intelligence
2019-08-30 v1 Logic in Computer Science
Abstract
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.
Keywords
Cite
@article{arxiv.1908.11137,
title = {PIE -- Proving, Interpolating and Eliminating on the Basis of First-Order Logic},
author = {Christoph Wernhard},
journal= {arXiv preprint arXiv:1908.11137},
year = {2019}
}
Comments
Part of DECLARE 19 proceedings