描述逻辑 EL 扩展中的插值子与显式定义
计算机科学中的逻辑
2022-05-31 v2
摘要
我们证明绝大多数描述逻辑 的扩展都不具备 Craig 插值性质，也不具备射影 Beth 可定义性性质。例如， 带个体名、 带全角色、 带形如 的角色包含公理，以及 均是如此。特别地，由此可得概念或个体名的显式定义的存在性不能通过隐式可定义性归约为包含检查。我们证明，尽管如此，对于 的标准易处理扩展（如 ），插值子与显式定义的存在性可在多项式时间内判定；对于 及各种扩展则在 ExpTime 内判定。由此可见，这些存在性问题的难度不高于包含问题，这与表达性强的描述逻辑（DL）的情况形成鲜明对比。我们还获得了插值子与显式定义的大小以及计算它们的复杂度的紧界：对于 的标准易处理扩展为单指数，对于 及扩展为双指数。最后我们讨论了 Horn-DL，如 Horn-。
引用
@article{arxiv.2202.07186,
title = {Interpolants and Explicit Definitions in Extensions of the Description Logic EL},
author = {Marie Fortin and Boris Konev and Frank Wolter},
journal= {arXiv preprint arXiv:2202.07186},
year = {2022}
}