ExpTime Tableaux with Global Caching for the Description Logic SHOQ
我们给出了第一个ExpTime（复杂性最优）的tableau决策过程，用于检查描述逻辑SHOQ中知识库的可满足性，它扩展了基本描述逻辑ALC，具有传递角色，角色层次，名词和量化数量限制。复杂度是用一元数表示来衡量的。我们的程序是基于全局缓存和整数线性可行性检查。
2014-07-21 cs.LO
Cut-Free ExpTime Tableaux for Checking Satisfiability of a Knowledge Base in the Description Logic SHI
我们给出了第一个无割ExpTime（最优）Tableau决策过程，用于检查描述逻辑SHI中的知识库的可满足性，它扩展了描述逻辑ALC的传递角色，逆角色和角色层次。
2012-07-16 cs.LO
An ExpTime Procedure for Description Logic $\mathcal{ALCQI}$ (Draft)
针对$\mathcal{ALCQI}$中的可满足性问题，给出了一个基于ExpTime表的最坏情况决策过程。一般公理
2007-03-18 cs.LO
Non-Rigid Designators in Modal and Temporal Free Description Logics (Extended Version)
本研究提出带非严格限定摹状词与名称的模态描述逻辑，关联一阶模态逻辑单变量片段可满足性，证明$\n mathbf{S5}^{n}$等逻辑概念可满足性为NEXPTIME完全，还分析了时态逻辑可判定性。
2024-09-10 cs.LO
A Modal Characterization Theorem for a Probabilistic Fuzzy Description Logic
模糊模态'可能'是解释概率类型空间通过采取预期的真值。概率模糊描述逻辑在概率双相似下是不变的，在信息量上是非扩展的。行为距离的概念。在本文中，我们提供了一个表征的表达能力，这种逻辑的基础上观察：我们证明了一个概率模拟的经典范Bentham定理，它指出，模态逻辑正是一阶逻辑的bisimulation-invariant片段。具体地说，我们证明了概率模糊一阶逻辑中的每一个公式都是非扩张的。行为距离可以通过概率模糊描述逻辑中的有界秩的概念来近似。关于同一结果的模态逻辑透视图，请参见arXiv：1810.04722。
2019-06-04 cs.LO
Combining Event Calculus and Description Logic Reasoning via Logic Programming
本文介绍了一种在逻辑程序设计框架下将事件演算与描述逻辑相结合的知识表示语言。其目的是为用户提供一种表达语言，用于建模和分析随时间演变的系统。该方法的例子与逻辑程序设计语言中实现的Fusarium系统。本文扩展了Fusarium的规则语言与描述逻辑$\cal ALCIF$的弱DL-安全接口，并使事件演算适应这种扩展语言。通过这种方式，带时间戳的ABOX可以在事件演算中作为流畅项进行操作。这一切都是在福柯的时间分层概念的框架内进行的。本文件酌情提供了健全性和完整性的条件。使用一个详细的例子，它演示了事件演算，描述逻辑和逻辑编程规则的相互作用，用于计算可能的模型作为合理的解释的建模系统的当前状态。
2021-09-10 cs.LO
Tableaux for Free Logics with Descriptions
本文提供了一个明确的描述表的方法。我们专注于所谓的最小自由描述理论（MFD）的几个形式化通常制定公理化的自由逻辑的设置。我们考虑五个分析表系统对应于不同种类的自由逻辑，包括应用于计算机科学的定义性逻辑和构造性数学处理部分功能（这里称为负准自由逻辑）。Tableau系统基于PFL（正自由逻辑），NFL（负自由逻辑），PQFL和NQFL（前一个的准自由对应物）将MFD形式化。还考虑了逻辑NQFLm，其等价于NQFL，但其语言不包括存在谓词。它表明，所有的tableaux是健全的和完整的这些逻辑的语义。
2021-07-15 cs.LO
Decidability of an Expressive Description Logic with Rational Grading
本文考虑了描述逻辑中实现理性分级的句法对象-概念构造子，即部分限制。部分限制能够表达关于后继集合的合理部分的语句，从本质上丰富了DL的表达能力。我们研究了一个扩展的研究DL ALCQIHR+部分限制，并证明了在扩展逻辑的推理仍然是可判定的。证明使用表格技术与指数技术，旨在处理部分限制。
2019-05-24 cs.LO
Bisimulation-Based Comparisons for Interpretations in Description Logics
我们研究比较描述逻辑的解释方面的“逻辑后果”的形式半积极的概念（如半积极的概念断言）。这种比较的特点是由类似的互模拟的条件。在所考虑的逻辑中最简单的是PDL（命题动态逻辑）的变体。其他的扩展，逻辑与逆角色，名词，量化的数量限制，通用的角色，和/或概念构造器表示的局部自反性的角色。所研究的问题是：关于比较的半正概念的保持，用于比较的Hennessy-Milner性质，以及保持半正概念的解释的最小化。
2013-04-20 cs.LO
Non-Rigid Designators in Epistemic and Temporal Free Description Logics (Extended Version)
本文研究含 nominals、全称角色与限定摹状词的认知和时态描述逻辑，在自由逻辑的部分指称及非严格指示词语义下，分别证明认知情形可满足性为 NExpTime 完全、线性时态情形不可判定。
2023-08-16 cs.LO
Category-theoretical Semantics of the Description Logic ALC (extended version)
范畴论可以用来陈述一阶逻辑中的公式，而不需要使用集合成员。逻辑学中的几个显著结果，如连续统假设的证明，可以在范畴论中优雅地重写。本文提出用范畴语言重新表述描述逻辑$\mathcal{ALC}$通常的集合论语义。在这种设置中，ALC概念被表示为对象，概念包含被表示为箭头，并且成员关系被表示为类别的对象和箭头上的逻辑量词。这种范畴理论语义提供了$\mathcal{ALC}$的语义的更模块化的表示和设计用于推理的算法的新方法。
2022-04-18 cs.LO
SHACL: A Description Logic in Disguise
SHACL是W3C提出的一种语言，用于表达RDF图上的结构约束。近年来，SHACL的知名度迅速上升。这种流行的上升伴随着与其在语义网中的位置相关的问题，特别是关于其与OWL（在Web上表达本体信息的事实标准）和描述逻辑（形成OWL的形式基础）的关系。我们回答这些问题，认为SHACL实际上是一个描述逻辑。一方面，我们的答案出奇的简单，有些人甚至可以说是显而易见的。但另一方面，我们的答案也有争议。通过一劳永逸地解决这个问题，我们建立了描述逻辑领域作为SHACL的坚实形式基础。
2022-06-28 cs.LO
On Free Description Logics with Definite Descriptions
明确描述是“该$x$使得$φ$”形式的短语，用于指代上下文中的单个实体。它们通常比单独的名称对用户更有意义，特别是在通过本体建模或查询数据时。我们研究自由描述逻辑与个人的名字和明确的描述作为语言的条款，同时也占他们可能缺乏外延。我们专注于扩展的$\mathcal{ALC}$和，分别，$\mathcal{EL}$与名词，普遍的作用，和明确的描述。我们表明，在这些扩展中的标准推理并不比原来的语言更难，我们使用一个合适的互模拟概念来描述相对于一阶公式的概念的表达能力。此外，我们奠定了基础，通过研究的复杂性，决定存在的明确的描述下的本体论的个人自动支持确定的描述生成。最后，我们提供了一个多项式时间减少的推理在其他自由描述逻辑语言的基础上的双域语义部分解释的情况下。
2021-06-29 cs.LO
On Bisimulations for Description Logics
我们研究互模拟有用的描述逻辑。所考虑的逻辑中最简单的是$\mathcal{ALC}_{reg}$（PDL的变体）。其他的扩展，逻辑与逆角色，名词，量化的数量限制，通用的角色，和/或概念构造器表示的局部自反性的角色。它们也允许角色公理。我们给出的结果不变性的概念，TBox和ABoxes，保持RBoxes和知识库，和Hennessy-Milner性质w.r.t.在所考虑的描述逻辑的互模拟。使用不变性的结果，我们比较所考虑的描述逻辑w.r.t.概念、TBox和ABoxes。我们关于分离描述逻辑的表达性的结果自然地扩展到当我们有扩展$\mathcal{ALC}$的$\mathcal{ALC}_{reg}$的任何子逻辑而不是$\mathcal{ALC}_{reg}$的情况。我们还提供了最大的自互模拟和商的解释w.r.t.的结果。这种等价关系。这些结果对于描述逻辑中的最小化解释和概念学习是有用的。为了处理最小化解释的情况下，所考虑的逻辑允许量化的数量限制和/或构造函数的局部自反性的作用，我们引入了一个新的概念，称为QS-解释，这是需要获得预期的结果。通过采用Hopcroft的自动机极小化算法和Paige-Tarjan算法，我们给出了计算有限解释最大自互模拟所对应的划分的有效算法。
2015-02-19 cs.LO
Bisequent Calculi for Neutral Free Logic with Definite Descriptions
本文在中性自由逻辑中为带等词与限定摹状词的极小理论构建双矢列式演算，并证明扩展系统中切分规则可容许。
2024-12-02 cs.LO
Reasoning in Non-normal Modal Description Logics
非正规模态逻辑，解释的邻域模型，概括了通常的关系语义，已发现应用在几个领域，如认识论，道义，和联盟推理。在这里，我们提出了初步的结果推理的模态描述逻辑的一个家庭，通过结合ALC与非正规模态算子。首先，我们提供了一个框架的终止，正确的，和完整的Tableau算法来检查满足性的公式在这样的逻辑与语义的基础上变化的域。然后，我们调查的可满足性问题，这些语言的片段，通过限制应用程序的模态算子的公式，并解释模型与常数域，提供紧密的复杂性结果。
2022-06-30 cs.LO
Deciding SHACL Shape Containment through Description Logics Reasoning (Extended Version)
XML约束语言（SHACL）允许对RDF数据图进行形式化约束。形状将RDF图中的节点可以满足的一组约束分组。我们调查的问题之间的SHACL形状的包容性。如果满足第一形状的约束的每个图节点也满足第二形状的约束，则一个形状包含在第二形状中。为了判定形状包容性，我们将SHACL形状图映射到描述逻辑公理中，使得形状包容性可以通过描述逻辑推理来回答。我们确定了几个，越来越严格的语法限制SHACL，这种方法变得健全和完整。
2021-04-22 cs.LO
Non-Normal Modal Description Logics (Extended Version)
该研究提出一族扩展ALC语言的非正规模态描述逻辑，提供变域下NExpTime复杂度的表算法框架，给出部分系统到常域关系模型的归约，并证明限制模态算子应用片段的ExpTime紧复杂度。
2023-07-23 cs.LO
Description Logics with Two Types of Definite Descriptions: Complexity, Expressiveness, and Automated Deduction
Queen Mary University of London（伦敦大学玛丽女王学院）
本文提出两种扩展描述逻辑ALC的确定描述变体，分析其复杂性、表达性及自动推理方法，展示ALCι_G在表达性上的优势及实现的有效性。
2025-12-07 cs.LO
Using Tableau to Decide Description Logics with Full Role Negation and Identity
本文提出了一种确定具有完全角色否定和角色恒等式的表达性描述逻辑的表方法。我们考虑的描述逻辑ALBOid，这是扩展的ALC与布尔角色操作符，逆的角色，身份的角色，并包括完全支持个人和单例概念。ALBOid在表达上等价于一阶逻辑的两变量片段，并包含布尔模态逻辑。在本文中，我们定义了一个健全的和完整的表演算的ALBOid，提供了一个基础，决策程序的逻辑及其所有的子逻辑。我们的方法的一个重要的新颖性是使用一个通用的无限制的阻塞机制。基于概念上简单的规则，无限制分块执行两个个体是否相等的情况区分和等式推理以找到有限模型。阻塞机制将Tableau导子的终止性证明与ALBOid的有限模型性质联系起来。
2016-11-28 cs.LO
The Fusemate Logic Programming System (System Description)
模糊逻辑是一种逻辑编程系统，它实现了析取逻辑程序的可能模型语义。它的输入语言围绕着一个弱的分层概念，上面有理解和聚合运算符。Fusarium在Scala程序设计语言中实现为浅嵌入。这使得Scala数据类型可以作为术语使用，与外部系统的紧密接口，并且它使模型计算可以作为普通的容器数据结构构造器使用。本文描述了上述功能，并证明了他们与一个非平凡的用例，嵌入的描述逻辑$\cal ALCIF$到Fusarium的输入语言这个版本的文件纠正了一个错误的出版版本，其中使用了不合适的版本“阻塞”的$\cal ALCIF$嵌入。
2021-05-19 cs.LO
Efficient Answer Enumeration in Description Logics with Functional Roles -- Extended Version
我们研究了枚举的本体介导的查询的答案时，制定了一个描述逻辑，支持功能的角色和查询是CQ的本体。特别是，我们表明，枚举是可能的线性预处理和恒定的延迟时，一定的扩展CQ（有关的功能角色）是无环和自由连接无环。这既适用于完整答案，也适用于部分答案。我们提供匹配的下限的情况下，查询是自连接自由。
2022-11-28 cs.LO
Repairing Description Logic Ontologies by Weakening Axioms
在移除不想要的结果$α$的意义上，用于修复描述逻辑本体O的经典方法是从O中删除最小数量的公理，使得所得本体O'不具有结果$α$。然而，完全删除公理可能过于粗略，因为它也可能删除实际想要的结果。为了缓解这个问题，我们提出了一种更温和的修复方式，其中公理不一定被删除，而只是被削弱。一方面，我们调查这种温和的修复方法的一般性质。另一方面，我们提出并分析了具体的方法来削弱公理表示的描述逻辑EL。
2018-08-01 cs.LO
Query Answering in Lattice-based Description Logic
本文研究基于格的描述逻辑 LE-ALC 的本体介导查询回答，证明对无环 TBox 知识库可利用或扩展表推演算法高效回答多种查询。
2025-06-06 cs.LO
The Completeness of Reasoning Algorithms for Clause Sets in Description Logic ALC
在语义Web上，元数据和本体被用来使计算机能够读取数据。Web本体语言（OWL）已被提出作为一种标准的本体语言，并已研究了各种推理系统，这种语言。描述逻辑被认为是OWL的理论基础，它们提供了描述本体和知识库的形式语言的语法和语义。此外，描述逻辑的tableau算法已经发展成为可判定问题的标准推理算法。然而，Tableau算法生成低效的推理步骤，由于其不确定性分支的析取以及存在量化的模型规模的增加。在这项研究中，我们提出了合取范式（CNF）的概念，它利用一个平面的概念形式的描述逻辑ALC，以开发算法推理的条款集。我们提出了一个有效的推理算法的条款集，任何ALC的概念转化为一个等价的CNF概念。在理论上，我们证明了CNF概念可满足性推理算法的可靠性、完备性和可终止性。
2022-08-10 cs.LO
The Probabilistic Description Logic $\mathcal{BALC}$
描述逻辑（DL）是著名的知识表示形式主义集中在术语知识的表示。由于它们的一阶语义，这些语言（在其经典形式）不适合表示和处理不确定性。最近提出了一个轻量级DL的概率扩展，用于处理发生在不确定背景下的某些知识。在本文中，我们继续这条线的研究，通过引入贝叶斯扩展\BALC的命题封闭DL \ALC。我们提出了一个基于表格的程序来决定一致性，并适应它来解决其他概率，上下文和一般的推理在这个逻辑。我们还表明，所有这些问题仍然是\ExpTime -完全的，在基本的经典\ALC推理相同。
2020-09-28 cs.LO
A finite basis theorem for the description logic ${\cal ALC}$
本文的主要结果是证明了描述逻辑${\cal ALC}$中有限基的存在性。我们证明了在有限模型中成立的广义概念包含（GCI）的集合总是有一个有限基，即这些GCI可以从多个GCI中导出。这一结果推广了Baader和Distel的一个结果，该结果表明，对于非表达描述逻辑${\cal EL}$和${\cal EL}_{gfp}$，GCI在有限模型中存在有限基。我们还提供了一个算法来计算这个有限基，并证明其正确性。作为一个副产品，我们扩展我们的有限基定理，以任何非线性生成的完全余种（即任何类的模型关闭下态射域，余积和商，并从有限的一组有限模型）。
2017-01-13 cs.LO
A Binary Quantifier for Definite Descriptions in Nelsonian Free Logic
本文在Nelson次协调逻辑N4及其负自由变体中考察并改进了Kürbis的二元量词I，给出嵌入函数、自然演绎系统和Kripke语义，以构造性假和次协调逻辑解决Russell确定描述词解释中的悖论问题。
2024-12-31 cs.LO
Adding the Power-Set to Description Logics
我们探讨描述逻辑和集合论之间的关系。这项研究是进行使用，在集理论方面，一个非常基本的公理集理论欧米茄，只有四个公理特征二元联盟，集差，包括，和权力集。然后定义了ALC的扩展，ALC^Omega，其中概念被自然地解释为生活在Omega模型中的集合。在ALC^Omega中，不仅允许概念之间的隶属关系-甚至允许循环-而且利用幂集构造来增加元建模能力。我们调查翻译的ALC^欧米茄到标准的描述逻辑，以及一套理论的翻译。ALCIO中ALC^Omega的多项式编码证明了有限模型属性的有效性以及概念可满足性复杂度的ExpTime上界。我们开发了一个集合论翻译的ALC^欧米茄在理论欧米茄，利用技术最初提出的正常模态和多模态逻辑转换成欧米茄。最后，我们表明，片段LC^欧米茄的ALC^欧米茄，它不承认的角色和个人的名字，是作为表达的ALC^欧米茄。
2019-11-22 cs.LO
Integrating Context of Statements within Description Logics
我们解决的问题，提供上下文信息的逻辑公式（如出处，有效期，或信心），并表示它在一个逻辑系统。在这种情况下，就需要借助一种高阶的或非标准的形式主义，或者某种具体化的机制。我们探讨了具体化的情况下，形式化的概念，上下文逻辑语句的情况下，描述逻辑。然后，我们定义了几个属性的语境化是可取的。没有任何一种方法能满足所有这些要求。因此，我们定义了一种新的上下文注释语句的方式。它受到NdFluents的启发，NdFluents本身是4dFluents方法的扩展，用于注释具有时间上下文的语句。在NdFluents中，上下文语句中涉及的实例被分割成上下文部分，这样只有同一上下文中的部分才彼此保持关系，目的是更好地保留推论。我们通过定义关系和类的上下文部分来推广这个想法。这种形式构造更好地满足了这些性质，尽管不是完全满足。我们表明，这是一个特殊的情况下，NdFluents也实例化的一般机制，并提出其他变化。
2017-09-14 cs.LO
Towards Syntactic Epistemic Logic
本文提出句法认识逻辑（SEL），将认识情境视为句法条件集合，以捕捉不完整描述，并填补认识博弈论中句法与语义表示之间的鸿沟。
2022-12-30 cs.LO
Computation of Interpolants for Description Logic Concepts in Hard Cases
本文针对不具备Craig插值性质的描述逻辑及跨逻辑插值难题，首次给出在ALCH和ALCQ本体下计算ALC插值的初等算法，并指出一致插值可能具有非初等大小。
2025-07-21 cs.LO
Formal verification of a proof procedure for the description logic ALC
描述逻辑（DL）是一种用于以结构化和形式化的方式表示和推理应用领域知识的语言。为了实现这一目标，已经实施了几个证明器，如RACER和FaCT++，但这些证明器本身尚未获得认证。为了确保这些DL中推导的合理性，有必要正式验证这些推理机应用的推导。形式化方法为证明过程的规范和验证提供了强大的工具，其中包括证明过程的可靠性，完整性和终止性等属性的方法。在本文中，我们提出了一个证明过程的描述逻辑ALC的定义，基于语义tableau方法。我们通过使用Isabelle证明助手证明其可靠性、完备性和终止性来确保证明器的有效性。证明分为两个阶段进行，首先在抽象级别上建立这些属性，然后将它们实例化以用于基于列表的实现。
2013-07-31 cs.LO
Mapping the Object-Role Modeling language ORM2 into Description Logic language DLRifd
近年来，人们已经做出了一些努力，以增强概念数据建模与自动推理，以提高模型的质量，并获得隐含的信息。在实现中实现这一点的一种方法是约束语言。描述逻辑的进步可以帮助选择正确的语言，使其具有最大的表达能力，但仍保留在一阶逻辑的可判定片段内，从而使用DL推理机实现具有良好性能的可行实现。最适合的DL语言似乎是ExpTime-complete DLRifd。为了说明权衡和突出功能的建模语言，我们提出了一个精确的转换非常富有表现力（不可判定）的ORM/ORM 2概念数据建模语言的映射功能，完全DLRifd。虽然不是所有的ORM 2功能都可以被映射，但这是一个有趣的片段，因为它已经表明DLRifd也可以编码UML类图和EER，因此可以促进概念数据模型之间的互操作，并研究建模语言的本体方面。
2009-04-22 cs.LO
Living Without Beth and Craig: Definitions and Interpolants in Description and Modal Logics with Nominals and Role Inclusions
本文针对含名词和角色包含的描述/模态逻辑不具备CIP与PBDP的问题，证明插值元与显式定义存在性仍可判定，明确不同场景下的复杂度，并给出适用于含角色包含描述逻辑的计算算法。
2023-04-28 cs.LO
On $P$-Interpolation in Local Theory Extensions and Applications to the Study of Interpolation in the Description Logics ${\cal EL}, {\cal EL}^+$
本文提出局部理论扩张中计算 $P$-插值项的分层方法，并据此分析带单调算子半格及描述逻辑 ${\cal EL}$、${\cal EL}^+$ 中的序插值性质。
2023-07-17 cs.LO
A Hoare Logic for Domain Specification (Full Version)
针对现有程序规约与验证方法仅关注计算层面正确性的问题，研究提出整合实现与领域断言的双层霍尔逻辑，采用描述逻辑和语义提升方法，通过两类断言转换的演算实现关注点分离并支持验证中使用描述逻辑。
2024-02-01 cs.LO
Logic Column 15: Coalgebras and Their Logics
这篇文章介绍了最近的工作的主题指定的性质的过渡系统。通过给出一个适当的抽象描述的过渡系统作为余代数，它是可能的，以一种优雅的方式来获取这些过渡系统的性质的逻辑。
2006-05-28 cs.LO
Separating Data Examples by Description Logic Concepts with Restricted Signatures
我们研究了分离的积极和消极的数据的例子中存在的本体论的描述逻辑概念。与以前的工作相比，我们添加了一个签名，指定了一个子集的符号，可用于分离，我们承认在该签名中的个人名称。我们认为弱和强的版本所产生的问题，不同的负面的例子是如何对待，我们区分分离和没有帮助符号。在这个框架内，我们比较了不同语言的分离能力和调查的复杂性，决定可分性。虽然弱可分性被证明是密切相关的保守扩展，强烈分离的概念与克雷格插值，适当定义的编码的数据和本体。这使我们能够将这些领域的已知结果转化为可分性。相反，我们得到原来的结果可分性，可以向后转移。例如，相当令人惊讶的是，ALCO中的保守扩张和弱可分性都是3ExpTime完全的。
2021-07-12 cs.LO
On Decidability of Expressive Description Logics with Composition of Roles in Number Restrictions
描述逻辑是一种知识表示的形式化方法，在广泛的应用领域中得到了广泛的应用。由于其吸引人的表现力，我们认为在本文中扩展的著名的概念语言ALC允许复杂的角色表达式的数量限制。这些语言首先由Baader和Sattler作为ALCN（M）语言引入，采用了{o，-，And，Or}的角色构造函数M子集。特别是，他们在1999年证明，虽然ALCN（o）是可判定的，但添加其他算子可能很容易导致不可判定性：事实上，ALCN（o，And）和ALCN（o，-，Or）被证明是不可判定的。在这项工作中，我们进一步研究的计算性能的ALCN家庭，旨在缩小可判定性的差距留下开放的Baader和Sattler的结果。特别是，我们将证明ALCN（o）扩展与逆角色在数量和价值的限制变得不可判定，而它可以安全地扩展与合格的数量限制，而不会失去可判定性。
2003-08-19 cs.LO
A Rational Entailment for Expressive Description Logics via Description Logic Programs
ISTI - CNR（意大利国家研究委员会信息科学与技术研究所）；CAIR - University of Cape Town（开普敦大学CAIR）
Lehmann和Magidor的有理闭包被认为是非单调逻辑领域的一个里程碑，它也在描述逻辑（DL）的背景下被重新表述。我们在这里展示了如何建模的合理形式的蕴涵表达DL，如SROIQ，提供了一种新的推理过程，编译成一个描述逻辑程序（DL程序）的非单调DL知识库。
2021-06-28 cs.AI cs.LO
On the Undecidability of Fuzzy Description Logics with GCIs with Lukasiewicz t-norm
IIIA - CSIC（西班牙国家研究委员会人工智能研究所）；ISTI - CNR（意大利国家研究委员会信息科学与技术研究所）
最近有一些意想不到的结果，模糊描述逻辑（FDLs）与一般概念包含（GCI）。他们表明，与经典的情况下，DL ALC与GCI不具有有限的模型属性下Lukasiewicz逻辑或产品逻辑，具体地说，知识库可满足性是一个不可判定的问题产品逻辑。我们在这里完成的分析表明，知识库可满足性也是一个不可判定的问题Lukasiewicz逻辑。
2011-07-27 cs.AI cs.LO
A Characterization Theorem for a Modal Description Logic
模态描述逻辑的特点是模态，它捕获知识对诸如时间、地点或代理的信息状态等参数的依赖性。例如，在一个示例中，逻辑S5-ALC将标准描述逻辑ALC与可以被理解为认知算子或表示（无向）变化的S5模态相结合。该逻辑嵌入到相应的模态一阶逻辑S5-FOL中。我们证明了一个模态特征定理的嵌入，在类比的结果由范Bentham和罗森有关ALC标准的一阶逻辑：我们表明，S5-ALC只有局部角色是，无论是在有限的和无限制的模型，正是互模拟不变片段的S5-FOL，从而给出了一个精确的描述的表达能力的S5-ALC只有局部角色。
2017-05-23 cs.LO math.LO
Aleatoric Description Logic for Probailistic Reasoning (Long Version)
The University of Western Australia（西澳大学）
描述逻辑是描述本体知识库的有力工具。也就是说，它们从个人、概念和关系的角度对世界进行了事实性的描述。在存在不确定性的情况下，这种事实说明是不可行的，需要采取主观或认识的方法。随机描述逻辑通过掷骰子将世界中的不确定性建模为随机事件，其中代理人对这些骰子的偏见具有主观信念。这提供了一个主观的贝叶斯描述逻辑，其中命题和关系根据理性代理人会下什么注来分配概率，给定可能的个体和骰子的配置。任意描述逻辑一般化的描述逻辑ALC，可以看出，描述的概率空间的解释的限制ALC的所有角色的功能。考虑了几个计算问题，并提出了模型检验和一致性检验算法。最后，任意描述逻辑被证明能够建模学习，其中代理能够根据观察结果对骰子的偏见进行调节。
2021-08-30 cs.AI cs.LO
A Semantic Similarity Measure for Expressive Description Logics
提出了一种完全语义的度量方法，该方法能够计算概念描述之间、概念描述与个体之间或以表达性描述逻辑表达的个体之间的相似度值。它适用于符号描述，尽管它使用数值方法进行演算。考虑到描述逻辑是本体知识表示和推理的理论框架，该方法可以有效地应用于语义Web领域的凝聚和分割聚类任务。
2009-11-26 cs.AI cs.LO
A Description Logic Primer
University of Oxford（牛津大学）
本文提供了一个自包含的第一次介绍描述逻辑（DL）。文中首先举例说明了DL SROIQ的主要概念和特点，然后详细定义了DL SROIQ的语法和语义。附加部分回顾了轻量级DL语言，讨论了与Web本体语言OWL的关系，并给出了进一步阅读的指针。
2013-06-03 cs.AI cs.LO
Evonne: Interactive Proof Visualization for Description Logics (System Description) -- Extended Version
TU Dresden（德累斯顿工业大学）
描述逻辑蕴涵的解释为大型本体的维护提供了重要的支持。在本体编辑器中通常用于此目的的“证明”精确指出本体中负责给定蕴涵的部分。蕴涵的证明使中间的推理步骤变得明确，从而解释了一个结论实际上是如何推导出来的。我们提出了一个交互式的系统，探索描述逻辑证明，称为Evonne，可视化的表达DL写的本体论的后果证明。我们描述了用于计算这些证明的方法，以及一个称为基于签名的证明浓缩的功能。此外，我们使用真实的本体来评估生成的证明的质量。
2022-05-19 cs.AI cs.LO
First steps in the logic-based assessment of post-composed phenotypic descriptions
Universitat Jaume I de Castelló（卡斯特利翁海梅一世大学）；European Bioinformatics Institute（欧洲生物信息研究所）；University of Oxford（牛津大学）
在本文中，我们提出了一个初步的逻辑为基础的评估整合后组成的表型描述与领域本体。评价已经进行了使用描述逻辑推理与可扩展的技术：本体模块化和本体之间的逻辑差异的近似。
2010-12-08 cs.AI cs.LO
An extended description logic system with knowledge element based on ALC
Yunnan Normal University（云南师范大学）；Universidad Politécnica de Cartagena（卡塔赫纳理工大学）
随着知识管理和知识经济的兴起，直接联系和体现知识系统的知识要素成为某些领域的研究热点和热点。现有的知识元表示方法在处理形式、逻辑和推理等方面的功能有限。在描述逻辑ALC和公共知识元模型的基础上，为了描述知识元，对描述逻辑ALC进行了扩展。该概念被扩展为两个不同的概念（即对象知识元概念和属性知识元概念）。将对象知识元概念与属性知识元概念之间的关系扩展为3种（即对象知识元概念与属性知识元概念之间的关系、对象知识元概念之间的关系、属性知识元概念之间的关系），并增加了逆关系构造器，提出了一种描述逻辑KEDL系统。通过论证，得到了所描述的逻辑系统KEDL的完备性、可靠性等有关性质。最后通过实例验证了描述逻辑KEDL系统具有较强的知识元描述能力。
2019-04-16 cs.AI cs.LO
Labelled calculi for quantified modal logics with definite descriptions
本文引入了具有确定描述的量化模态逻辑的标号演算。我们证明了这些演算具有G3型演算的良好结构性质。特别地，所有规则都是保高可逆的，弱化和收缩是保高容许的，割是容许的。最后，我们表明，每个演算给出了相应的模型类的有效性的证明理论表征。
2020-02-12 cs.LO math.LO
Generalized Satisfiability for the Description Logic ALC
基本描述逻辑ALC中的标准推理问题概念可满足性是PSPACE-完全的，并且在存在无限制公理的情况下是EXPTIME-完全的。ALC的几个片段，特别是FL、EL和DL-Lite家族中的逻辑，有一个更容易的可满足性问题;有时它甚至是易于处理的。我们分类的复杂性标准可满足性问题的所有可能的布尔和量词片段的ALC中存在的一般公理。
2011-03-04 cs.CC cs.LO
Undecidability of the unification and admissibility problems for modal and description logics
我们表明，统一问题`是否有一个替代实例的一个给定的公式，是证明在一个给定的逻辑？对于用泛模态扩充的基本模态逻辑K和K_4，因此，推理规则的容许性问题对于这些逻辑也是不可判定的。这些是标准可判定模态逻辑的第一个例子，其中统一和容许问题是不可判定的。我们还证明了不可判定性的统一和容许问题的K和K4至少有两个模态算子和名（而不是通用模态），从而表明这些问题是不可判定的基本混合逻辑。最近，统一已被引入作为一个重要的推理服务的描述逻辑。带名项的K的不可判定性证明可以用来证明带名项的布尔描述逻辑（如ALCO和SHIQO）的统一的不可判定性。对于具有泛模态的K的不可判定性证明可以用来表明，对于具有传递角色、反向角色和角色层次（如SHI和SHIQ）的布尔描述逻辑，与角色盒相关的统一问题是不可判定的。
2006-09-11 cs.AI cs.LO
Description Logics with Fuzzy Concrete Domains
ISTI - CNR（意大利国家研究委员会信息科学与技术研究所）
我们提出了一个模糊版本的描述逻辑与具体领域。主要特点是：（i）概念构造器基于t-范数、t-连续、否定和蕴涵;（ii）具体域是模糊集;（iii）允许模糊修饰符;以及（iv）推理算法基于完成规则和有界混合整数规划的混合。
2012-07-04 cs.AI cs.LO
Reasoning with Individuals for the Description Logic SHIQ
虽然已经有大量的工作，推理算法的发展表达描述逻辑，在大多数情况下，只有Tbox推理被认为是。本文提出了一种在SHIQ描述逻辑中进行Tbox和Abox组合推理的算法。该算法特别令人感兴趣，因为它可用于决定（数据库）合取查询包含w.r. t的问题一种模式。此外，高效实现的实现应该相对简单，因为它可以基于FaCT系统中Tbox算法的现有高度优化的实现。
2000-05-11 cs.AI cs.LO
