通过 SAT 编码在模态与描述逻辑中进行自动推理：K(m)/ALC 可满足性案例研究
计算机科学中的逻辑
2014-01-16 v1 人工智能
摘要
在过去二十年中，模态逻辑与描述逻辑已被应用于计算机科学的众多领域，包括知识表示、形式化验证、数据库理论、分布式计算，以及近期的语义网和本体。因此，模态逻辑与描述逻辑中的自动推理问题已被深入研究。特别是，已提出许多方法来高效处理核心正规模态逻辑 K(m) 及其记法变体——描述逻辑 ALC 的可满足性问题。尽管 K(m)/ALC 结构简单，但在其上进行推理在计算上非常困难，其可满足性问题是 PSPACE 完全的。在本文中，我们开始探索通过将模态逻辑与描述逻辑中的自动推理任务编码为 SAT 以由 SOTA SAT 工具处理的想法；与大多数先前方法一样，我们从 K(m) 中的可满足性开始研究。我们提出了一种高效的编码，并在广泛的基准集上对其进行了测试，将该方法和主要的 SOTA 工具进行了比较。尽管该编码在最坏情况下必然是指数级的，但从我们的实验中注意到，在实践中该方法能够处理其他方法所能处理的大部分或全部问题，且性能与当前 SOTA 工具相当甚至更优。
引用
@article{arxiv.1401.3463,
title = {Automated Reasoning in Modal and Description Logics via SAT Encoding: the Case Study of K(m)/ALC-Satisfiability},
author = {Roberto Sebastiani and Michele Vescovi},
journal= {arXiv preprint arXiv:1401.3463},
year = {2014}
}