从计算逻辑视角看海因里希·贝曼对二阶量词消去的贡献
计算机科学中的逻辑
2017-12-20 v1 人工智能
摘要
对于关系一元公式（Löwenheim 类），二阶量词消去（与一致插值、投影和遗忘——这些目前在知识处理中备受关注的操作密切相关）总是成功的。海因里希·贝曼于 1922 年针对该类给出的可判定性证明明确地通过保持等价性的公式重写进行消去。在此我们详细重构贝曼发表中的结果，并讨论在现代计算逻辑中二阶量词消去方法背景下相关的议题。此外，我们提供了贝曼遗物中涉及二阶量词消去的信件和手稿的广泛文献记录，包括带评注的目录以及德文原始文献的英文摘要（侧重于技术内容）。在 1920 年代后期，贝曼试图为谓词元数大于一的公式计算开发基于消去的决策方法。他的手稿以及与威廉·阿克曼的通信展示了至今仍具意义的技术细节，并揭示了阿克曼 1935 年奠基性论文《数学逻辑的消去问题研究》的成因，该文奠定了两种主流的现代二阶量词消去方法。
引用
@article{arxiv.1712.06868,
title = {Heinrich Behmann's Contributions to Second-Order Quantifier Elimination from the View of Computational Logic},
author = {Christoph Wernhard},
journal= {arXiv preprint arXiv:1712.06868},
year = {2017}
}