Jun, 2022

描述逻辑的统一模块化序列系统

PDF
TL;DR我们介绍了一个能够构建表达式描述逻辑 ALC 扩展的序列系统的框架。我们的框架不仅涵盖了各种常见的描述逻辑，而且还允许获取具有特殊公式的扩展描述逻辑的序列系统，我们称之为 “角色关系公理”。所有的序列系统都是声音和完整性，并具有高度保持常见结构规则的可容许性和高度保持规则的可逆性。
发现论文，激发创造
  • 用于非常表达性描述逻辑的实用推理

    本文介绍了一种算法，能够在考虑一般性概念包含公理和角色层级的情况下，决定具有传递和逆角色以及功能约束的 DL ALC 的可满足性，同时研究了这类 DL 的可决定性的限制，并描述了一系列优化技术，这些技术对于获得具有实际问题良好性能的决策过程实现至关重要。

    May, 2000

  • 表达能力描述逻辑的实际推理

    本文提出了一个算法，用于决定具有传递性和逆作用的角色，角色层次结构和限定数量限制的 A LC 的可满足性，并研究了这种 DL 族的决策能力极限。

    May, 2000

  • 描述逻辑进入二阶：使用全量量化概念扩展 EL

    该论文涉及描述逻辑的特性，首次引入普遍量化的概念，提出两种扩展的语义模型，包括模态逻辑中的公理原型和二阶逻辑中的量词的替代。研究表明，在某些扩展的语义中，所得出的结论与经典的描述逻辑相符，并证明了某种程度上用于这种扩展的算法的多项式可判定性。

    Aug, 2023

  • ALC 本体的通用模块的高效计算（扩展版）

    该论文提出了一种用于提取适用于描述逻辑 ALC 的本体的通用模块的方法，该方法基于均匀插值，可以比目前最先进的方法更快地计算通用模块和统一插值。

    May, 2023

  • 基于概念语义的描述逻辑 ALC 推理

    本文通过使用范畴语言重新表达了具有一般 TBox 的描述逻辑 ALC 通常的集合论语义，从而为 ALC 的语义提供了一种更模块化的表示。我们展示了一个多项式空间的确定性算法用于检查概念满足性的子逻辑，该子逻辑在传统的集合论语义中是无法定义的。

    May, 2022

  • 基于 SAT 编码的模态逻辑和描述逻辑的自动推理：K (m)/ALC - 可满足性的案例研究

    本文提出了将模态逻辑和描述逻辑自动推理任务编码为 SAT 的方法，并测试表明这种方法可以处理大多数或所有的问题，并且性能与现有的最先进工具相当甚至更好。

    Jan, 2014

  • 抽象辩证框架的编码转换为高阶逻辑

    提出了一种将抽象辩证框架及其语义编码为经典高阶逻辑的方法，通过证明助手 Isabelle/HOL 来正式编码并证明重要性质和语义关系。这种方法允许在统一逻辑环境中使用自动化和交互式推理工具对抽象辩证框架进行计算机辅助分析。示例应用包括形式分析和验证元理论性质以及在特定语义约束下生成解释和扩展。

    Dec, 2023

  • 探索命题动态逻辑的非正则扩展与描述逻辑特征

    在扩展 ALC 描述逻辑的决定性满足性检查和查询中，我们研究了非规则路径表达式的影响。我们重点研究了 ALCreg 和 ALCvpl，它们是使用正则和可见推动语言的路径表达式的扩展。

    Jul, 2023

  • 一维均匀片段

    论文探讨了一维统一片段（U1）的性质，以及 U1 与适应更高元关系的描述逻辑（DLR_reg）的关系，并定义了一个描述逻辑版本的 U1 变体，并证明了与 U1 和其他相关逻辑的表现力有关的一系列新结果。

    Apr, 2016

  • Datalog 程序的模块化实现

    本文提出一种基于模块化框架的材料化计算和维护的方法，该方法使用半朴素算法处理少数规则，同时可使用两种算法计算关系的传递闭包，实验表明，与现有的方法相比，本方法可以处理任意的 datalog 程序，而且性能也要高得多。

    Nov, 2018