Automated Reasoning with Analytic Tableaux and Related Methods
Automated Reasoning with Analytic Tableaux and Related Methods
复制标题
使用分析表和相关方法进行自动推理
DOI：
10.1007/978-3-642-40537-2_17
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Khodadadi M
中科院分区：
文献类型：
--
作者：
Khodadadi M
本文提出了一种具有若干改进的表演算，用于描述逻辑中的推理。微积分使用非标准规则来处理TBox语句。在现有的tableau方法中，使用固定规则处理TBox语句，而我们使用动态生成的一组精炼规则。这种方法已经变得非常实用，因为具有灵活规则集的推理器可以使用表格证明程序生成prototypeMetTel生成。我们还定义和研究了无限制阻塞机制的变化，其中通过有序重写实现相等推理，并通过排除其对固定有限单个项集的应用来控制阻塞规则的应用。以唯一名称假设进行推理，并将ABox个人排除在封锁应用之外，可视为后者的两个独立实例。实验表明，这些改进减少了规则应用，提高了性能。
The paper presents a tableau calculus with several refinements for reasoning in the description logic. The calculus uses non-standard rules for dealing with TBox statements. Whereas in existing tableau approaches a fixed rule is used for dealing with TBox statements, we use a dynamically generated set of refined rules. This approach has become practical because reasoners with flexible sets of rules can be generated with the tableau prover generation prototypeMetTel. We also define and investigate variations of the unrestricted blocking mechanism in which equality reasoning is realised by ordered rewriting and the application of the blocking rule is controlled by excluding its application to a fixed, finite set of individual terms. Reasoning with the unique name assumption and excluding ABox individuals from the application of blocking can be seen as two separate instances of the latter. Experiments show the refinements lead to fewer rule applications and improved performance.