PIE——基于一阶逻辑的证明、插值与时态消去环境

Christoph Wernhard

PIE——基于一阶逻辑的证明、插值与时态消去环境

人工智能 2019-08-30 v1 计算机科学中的逻辑

作者: Christoph Wernhard

摘要

PIE 是一个嵌入 Prolog 的、基于一阶逻辑的自动推理环境。它包含一个通用的公式宏系统，并支持创建交织宏定义、推理器调用以及 LaTeX 格式自然语言文本的文件。它支持调用多种推理器：外部证明器以及 PIE 的子系统，后者包括预处理器、一个基于 Prolog 的一阶证明器、Craig 插值方法以及二阶量词消去方法。

关键词

一阶逻辑自动推理 Prolog Craig 插值量词消去公式宏证明辅助器

引用

@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}
}

备注

Part of DECLARE 19 proceedings

PIE——基于一阶逻辑的证明、插值与时态消去环境

摘要

关键词

引用

备注

相关论文