二元道义逻辑在 HOL 中的忠实语义嵌入
人工智能
2018-03-06 v2 计算机科学中的逻辑
逻辑
摘要
本文给出了 Carmo 与 Jones 的二元道义逻辑在经典高阶逻辑中的浅层语义嵌入。该嵌入被证明是可靠且完备的，即忠实的。此处呈现的工作为在现成的高阶定理证明器与证明助手中实现并自动化二元道义逻辑提供了理论基础。
引用
@article{arxiv.1802.08454,
title = {Faithful Semantical Embedding of a Dyadic Deontic Logic in HOL},
author = {Christoph Benzmüller and Ali Farjami and Xavier Parent},
journal= {arXiv preprint arXiv:1802.08454},
year = {2018}
}
备注
23 pages, 3 figures