Horn 公式的高效 MUS 枚举及其在公理 pinpointing 中的应用
计算机科学中的逻辑
2015-05-19 v1
摘要
极小不可满足子集（MUSes）的枚举发现了日益增长的实际应用，包括广泛的诊断问题。作为一个具体例子，EL 族描述逻辑（DLs）中的公理 pinpointing 问题可被建模为 Horn 公式的 group-MUSes 枚举。反之，EL 族 DLs 的公理 pinpointing 有重要应用，例如调试医学本体，其中 SNOMED CT 是最著名的例子。本文的主要贡献是开发一个用于 Horn 公式的高效 group-MUS 枚举器 HGMUS，它在 EL 族 DLs 的公理 pinpointing 中找到直接应用。在开发 HGMUS 的过程中，本文也识别了现有解决方案的性能瓶颈。当 Horn 公式的 group-MUS 枚举所针对的问题域是 EL 族 DLs 的公理 pinpointing 时，新算法被证明优于所有替代方法，并采用取自不同医学本体的代表性示例套件。
引用
@article{arxiv.1505.04365,
title = {Efficient MUS Enumeration of Horn Formulae with Applications to Axiom Pinpointing},
author = {M. Fareed Arif and Carlos Mencía and Joao Marques-Silva},
journal= {arXiv preprint arXiv:1505.04365},
year = {2015}
}