Scifaro

中文

FMLtoHOL (版本 1.0)：利用 LEO-II 及其伙伴自动化一阶模态逻辑

计算机科学中的逻辑 2012-07-31 v1 人工智能

作者: Christoph Benzmueller , Thomas Raths

在 arXiv 上查看 ↗ PDF ↗

摘要

本文介绍了一种从一阶模态逻辑到经典高阶逻辑的转换器。该工具使得现成的高阶定理证明器和模型查找器能够应用于一阶模态逻辑内的推理。该工具支持关于常域、变域和累积域语义的逻辑 K、K4、D、D4、T、S4 和 S5。

关键词

一阶模态逻辑高阶逻辑定理证明模型查找 LEO-II 逻辑转换域语义

引用

@article{arxiv.1207.6685,
  title  = {FMLtoHOL (version 1.0): Automating First-order Modal Logics with LEO-II and Friends},
  author = {Christoph Benzmueller and Thomas Raths},
  journal= {arXiv preprint arXiv:1207.6685},
  year   = {2012}
}

备注

4 pages