arXiv Open Access 2019

PIE -- Proving, Interpolating and Eliminating on the Basis of First-Order Logic

Christoph Wernhard

Lihat Sumber

Abstrak

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.

Topik & Kata Kunci

cs.AI cs.LO

Penulis (1)

Christoph Wernhard

Format Sitasi

APA MLA BibTeX

Wernhard, C. (2019). PIE -- Proving, Interpolating and Eliminating on the Basis of First-Order Logic. https://arxiv.org/abs/1908.11137

Akses Cepat

Lihat di Sumber

Informasi Jurnal

Tahun Terbit: 2019
Bahasa: en
Sumber Database: arXiv
Akses: Open Access ✓