利用可达性扩展ALCQIO
Extending ALCQIO with reachability
摘要：
我们介绍了一个描述逻辑ALCQIO_{b,Re}，它增加了可达性断言ALCQIO，一个子逻辑的两个变量片段的一阶逻辑计数量词。ALCQIO_{b,Re}非常适合软件验证和形状分析应用。形状分析需要表达逻辑，它可以表达可达性，并具有良好的计算性能。我们表明，ALCQIO_{b,Re}可以描述复杂的数据结构具有高度的共享，并允许组合物，如列表的树。我们证明了ALCQIO_{b,Re} -公式的有限可满足性和蕴涵问题可以多项式时间约简为ALCQIO-公式的有限可满足性。从而得到了ALCQIO_{b,Re}中的有限可满足性和有限蕴涵是NEXPTIME-完全的。具有传递闭包构造器的描述逻辑以前已经被研究过，但是ALCQIO_{b,Re}是第一个在有限结构上保持可判定性的描述逻辑，同时允许名词，逆角色，计数量词和可达性断言，
英文摘要：
We introduce a description logic ALCQIO_{b,Re} which adds reachability assertions to ALCQIO, a sub-logic of the two-variable fragment of first order logic with counting quantifiers. ALCQIO_{b,Re} is well-suited for applications in software verification and shape analysis. Shape analysis requires expressive logics which can express reachability and have good computational properties. We show that ALCQIO_{b,Re} can describe complex data structures with a high degree of sharing and allows compositions such as list of trees. We show that the finite satisfiability and implication problems of ALCQIO_{b,Re}-formulae are polynomial-time reducible to finite satisfiability of ALCQIO-formulae. As a consequence, we get that finite satisfiability and finite implication in ALCQIO_{b,Re} are NEXPTIME-complete. Description logics with transitive closure constructors have been studied before, but ALCQIO_{b,Re} is the first description logic that remains decidable on finite structures while allowing at the same time nominals, inverse roles, counting quantifiers and reachability assertions,
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
