将ALC连接证明转换为ALC序列
Converting ALC Connection Proofs into ALC Sequents
摘要：
由于其简单、高效和合理的内存使用，连接方法在自动定理证明领域赢得了良好的声誉。这种方法已被应用于最近在自动证明的原因，在描述逻辑ALC编写的本体。然而，由连接演算生成的证明很难理解。证明的可读性在很大程度上是由转换到析取范式应用于公式证明损失。这样的证明模型，尽管是有效的，但会阻止基于它的推理系统有效地提供推理中使用的步骤的证明和/或描述。为了解决这个问题，在本文中，我们提出了一种方法，将ALC连接方法生成的矩阵证明转换为ALC连接证明，这是更容易理解，其翻译为自然语言是更直接的。我们还描述了一个演算，接受输入公式在一个非子句ALC格式，简化了翻译。
英文摘要：
The connection method has earned good reputation in the area of automated theorem proving, due to its simplicity, efficiency and rational use of memory. This method has been applied recently in automatic provers that reason over ontologies written in the description logic ALC. However, proofs generated by connection calculi are difficult to understand. Proof readability is largely lost by the transformations to disjunctive normal form applied over the formulae to be proven. Such a proof model, albeit efficient, prevents inference systems based on it from effectively providing justifications and/or descriptions of the steps used in inferences. To address this problem, in this paper we propose a method for converting matricial proofs generated by the ALC connection method to ALC sequent proofs, which are much easier to understand, and whose translation to natural language is more straightforward. We also describe a calculus that accepts the input formula in a non-clausal ALC format, what simplifies the translation.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
