论文标题
饼环境的方面，以证明，插值和消除一阶逻辑
Facets of the PIE Environment for Proving, Interpolating and Eliminating on the Basis of First-Order Logic
论文作者
论文摘要
PIE是基于一阶逻辑的序言，用于自动推理的环境。它的主要重点是公式，作为通过公式宏构建的复杂形式化的组成部分，以及作为推理任务的输出，例如二阶量化器消除和CRAIG插值。它支持基于文档的工作流程，该文档插入了宏观定义，理由的调用以及乳胶形式的自然语言文本。从各种示例开始，本文讨论了PIE的功能和应用可能性以及当前的局限性和未来研究的问题。
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.
