Computation of Interpolants for Description Logic Concepts in Hard Cases
本文针对不具备Craig插值性质的描述逻辑及跨逻辑插值难题，首次给出在ALCH和ALCQ本体下计算ALC插值的初等算法，并指出一致插值可能具有非初等大小。
2025-07-21 cs.LO
Logics for Rough Concept Analysis
本文从粗糙概念分析的基本结构的代数观点出发，引入了一些用正规模态算子展开的格，它们可以看作粗糙形式背景的某些子类的自然粗糙代数对应物，并为与这些格相关的逻辑引入了适当的显示演算，它们是可靠的、完备的、具有一致割消和子公式性质。这些结石模块化扩展粗糙代数的多类型结石的“非分配”（即一般格为基础的）设置。
2018-11-17 cs.LO math.LO
Description Logics Go Second-Order -- Extending EL with Universally Quantified Concepts
University of Ulm（乌尔姆大学）
本文提出描述逻辑EL的全称量化概念扩展，定义模式与二阶两种语义，证明有用片段中两种语义结论一致，并给出多项式可判定性，可表达角色链公理等。
2023-08-29 cs.AI cs.LO
On the Power and Limitations of Examples for Description Logic Concepts
Institute for Logic, Language and Computation (ILLC), University of Amsterdam（阿姆斯特丹大学逻辑、语言与计算研究所）；University of Bergen（卑尔根大学）；University of Oslo（奥斯陆大学）
本文研究了标注示例在描述描述逻辑概念方面的能力与局限性，系统探讨了介于EL和ALCQI之间的多种描述逻辑在有无DL-Lite本体论下有限特征化的存在性与高效可计算性，为概念调试和精确学习提供了理论基础。
2024-12-23 cs.LG 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
Dual Logic Concepts based on Mathematical Morphology in Stratified Institutions: Applications to Spatial Reasoning
在不同类型的逻辑中，几个逻辑运算符被定义为对偶对。这种对偶算子对也出现在其他代数理论中，如数学形态学。基于这一观察，本文提出了定义，在抽象层次的制度，一对抽象的对偶和逻辑运算符作为形态侵蚀和膨胀。标准的量词和模态，然后从这两个抽象的逻辑运算符。这些运营商都研究了一套状态和一套模型。为了应付缺乏明确的一套制度的国家，建议的抽象逻辑对偶算子定义在机构的扩展，分层机构，考虑到开放的句子，其中的满意度是参数化的状态集的概念。还提供了一个提示的空间推理的建议框架的潜在利益。
2017-10-16 cs.LO
Formal Concept Analysis and Resolution in Algebraic Domains
我们涉及两个以前独立的领域：形式概念分析和逻辑领域。我们将建立一个上下文属性逻辑之间的对应关系的形式背景。概念格和一个子句逻辑上的连贯代数CPOS。我们展示了如何识别域理论设置中的形式概念的概念。特别是，我们表明，从域逻辑的决议规则的一个特殊的例子与概念闭包算子从形式概念分析。结果揭示了使用上下文和域的知识表示和推理的目的。
2003-05-01 cs.AI cs.LO
Learning Concepts Described by Weight Aggregation Logic
RWTH Aachen University（亚琛工业大学）；Humboldt-Universität zu Berlin（柏林洪堡大学）
我们考虑加权结构，它通过将权重（即来自特定组或环的元素）分配给结构中存在的元组来扩展普通关系结构。我们引入一阶逻辑的扩展，允许聚合元组的权重，比较这些聚合，并使用它们来构建更复杂的公式。我们提供的局部性的片段的逻辑，包括Feferman-Vaught分解和Gaifman范式的片段称为FOW 1，以及局部化定理的一个更大的片段称为FOWA 1。该片段可以表达来自各种机器学习场景的概念。使用的局部性，我们表明，在FOWA 1中定义的概念在加权背景结构的最多polylogarithmic度是不可知的PAC学习的polylogarithmic时间后，伪线性时间预处理。
2020-09-22 cs.AI cs.LG cs.LO
Modal Logics for Topological Spaces
在这篇论文中，我们将提出两个逻辑系统，MP和MP，用于推理知识和努力。这些逻辑系统将在空间背景下进行解释，因此，知识和努力的抽象概念将由具体的数学概念来定义。
2000-07-26 cs.AI cs.LO
An effective characterization of the alternation hierarchy in two-variable logic
本文用恒等式刻画了二元一阶逻辑量词交替层次中各个层次的语言。这意味着个人水平的可决定性。更一般地，我们证明了一个可判定簇与簇J的双边半直积是可判定的。
2012-05-22 cs.LO
Constructive Interpolation and Concept-Based Beth Definability for Description Logics via Sequents
Institute of Artificial Intelligence, Technische Universität Dresden（德累斯顿工业大学人工智能研究所）
本文提出基于矢列系统的构造性方法，首次证明高表达力描述逻辑RIQ具有基于概念的Beth可定义性，并可从证明中计算插值式以提取隐式概念的显式定义。
2024-10-18 cs.AI cs.DB cs.LO
TAR: Neural Logical Reasoning across TBox and ABox
KAUST（阿卜杜拉国王科技大学）；University of Notre Dame（圣母大学）；Beihang University（北京航空航天大学）
许多本体，即，描述逻辑（DL）知识库已经被开发以提供关于各个领域的丰富知识。本体由ABox组成，即，两个实体之间或概念与实体之间的断言公理，以及TBox，即，两个概念之间的术语公理。神经逻辑推理（Neural Logic Reasoning，NLR）是探索这种知识库的基本任务，其目的是基于查询和答案的分布式表示，用逻辑运算回答多跳查询。虽然以前的NLR方法可以给出特定的实体级答案，即，ABox答案，它们不能提供描述性的概念级答案，即，TBox回答，其中每个概念是对一组实体的描述。换句话说，以前的NLR方法只对本体的ABox进行推理，而忽略了TBox。特别地，提供TBox答案使得能够利用描述性概念来推断每个查询的解释，这使得用户能够理解答案，并且在应用本体领域中非常有用。在这项工作中，我们制定了跨TBox和ABox（TA-NLR）的神经逻辑推理问题，解决这一问题需要解决在概念上合并，表示和操作的挑战。我们提出了一个原始的解决方案命名为TAR的TA-NLR。首先，我们结合描述逻辑的本体公理提供概念的来源。然后，我们将概念和查询表示为模糊集，即，集合，其元素具有隶属度，以将概念和查询与实体联系起来。此外，我们设计的操作员涉及的概念上的模糊集表示的概念和查询的优化和推理。在两个真实数据集上的大量实验结果证明了TAR对TA-NLR的有效性。
2022-08-16 cs.AI cs.LG cs.LO
Learning Permutation-Invariant Embeddings for Description Logic Concepts
Paderborn University（帕德博恩大学）
概念学习涉及从背景知识和输入示例中学习描述逻辑概念。我们的目标是学习一个涵盖所有正面例子的概念，而不是涵盖任何负面例子。这个非平凡的任务通常被表述为在无限准序概念空间内的搜索问题。虽然国家的最先进的模型已经成功地应用于解决这个问题，他们的大规模应用已严重阻碍，由于他们的过度探索，导致不切实际的运行时。在这里，我们提出了一个补救措施，这一限制。我们重新制定的学习问题作为一个多标签分类问题，并提出了一个神经嵌入模型（NERO），学习排列不变的嵌入的例子集量身定制的预测$F_1$分数预先选定的描述逻辑概念。通过以预测得分的降序排列这些概念，可以在很少的检索操作内检测到可能的目标概念，即，不要过度探索。重要的是，排名靠前的概念可以用于在概念空间的多个有利区域中开始最先进的符号模型的搜索过程，而不是在最一般的概念$\top$中开始它。我们在5个基准数据集上进行的770个学习问题的实验坚定地表明，NERO在$F_1$得分，探索概念的数量和总运行时间方面显着（p值<1%）优于最先进的模型。我们提供了我们的方法的开源实现。
2023-03-03 cs.AI cs.LG 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
Gradual Classical Logic for Attributed Objects - Extended in Re-Presentation
我们对事物的理解是概念性的。通过陈述我们对对象进行推理，事实上我们操纵的不是对象，而是涉及它们的概念。现在，只要我们承认一个对象所从属的无限延伸的概念，如空间、时间、大小、颜色等，简言之，任何合理的性质，就不可能在涉及对象的概念中肯定原子性。然而，形式/符号逻辑通常假定其他表达式建立在其上的原子实体。我们能把我们对概念的直觉反映到形式/符号逻辑上吗？我保证我们可以，但是关于原子性的通常观点需要检查。在这项工作中，我提出了渐进的逻辑，具体化的观察，我们不能区分是否被视为原子实体是原子或只是原子足以不被认为是非原子。其动机是捕捉自然发生在具有属性的概念周围的某些现象，包括预设和反义词。我提出的逻辑细节的逻辑，然后映射到形式语义。两个语言学上有趣的语义将被考虑。可决定性已经显现。
2015-04-19 cs.AI cs.CL cs.LO
Enabling Verification of Deep Neural Networks in Perception Tasks Using Fuzzy Logic and Concept Embeddings
Continental AG（大陆集团）；University of Bamberg（班贝格大学）
用于安全关键应用的深度卷积神经网络（CNN）的一个主要缺点是其黑盒性质。这使得在已经训练好的计算机视觉CNN上很难验证或监控复杂的符号要求。在这项工作中，我们提出了一个简单而有效的方法来验证一个CNN符合与视觉概念相关的符号谓词逻辑规则。这是第一个：（1）不修改CNN，（2）可以使用没有CNN输入或输出特征的视觉概念，以及（3）可以利用连续的CNN置信度输出。为了实现这一目标，我们新结合了可解释的人工智能和逻辑的方法：首先，使用监督概念嵌入分析，CNN的输出是事后丰富的概念输出。其次，来自先验知识的规则被建模为接受CNN输出的真值函数，并且可以以很少的计算开销进行评估。我们在这里研究模糊逻辑的使用，即，连续的真值，以及适当的输出校准，这在理论上和实际上都显示出轻微的好处。在三个验证用例的最先进的对象检测器上证明了适用性，其中对违反规则的监控可以揭示检测错误。
2022-03-13 cs.CV cs.LG cs.LO
Logic and Concepts in the 2-category of Topoi
该研究在topoi 2-范畴中用Kan内射性公理化概念，引入几何逻辑片段并建立对应松弛幂等伪单子，证明其代数有分类topos且给出Diaconescu型结果，定义了概念完全的几何逻辑片段。
2025-05-21 cs.LO math.CT math.LO
On syntactic concept lattice models for the Lambek calculus and infinitary action logic
本研究将Wurm提出的句法概念格语义扩展到带Kleene迭代的Lambek演算无穷版本（无穷动作逻辑），证明其强完备性及相关推论，还探讨了常元问题并强化了原有结果以纳入常元。
2025-10-28 cs.LO
A Modal Logic for Possibilistic Reasoning with Fuzzy Formal Contexts
Institute of Information Science, Academia Sinica（学术院信息科学研究所）
本文提出了一种用于模糊形式背景的可能性推理的双类型加权模态逻辑，实现了对模糊概念的扩展，并展示了逻辑的表达能力和扩展可能性。
2025-12-31 cs.AI cs.LO
Triadic Concept Analysis for Logic Interpretation of Simple Artificial Networks
Brandenburgische Technische Universität Cottbus-Senftenberg（勃兰登堡技术大学科特博-森ftenberg）
本文提出通过三元概念分析将简单人工神经网络转换为可解释的逻辑树结构，以提升模型的可解释性同时保持分类性能。
2026-01-09 cs.AI cs.LG cs.LO
Partial Awareness
我们开发了一种模态逻辑来捕获部分意识。该逻辑有三个构建块：对象、属性和概念。属性是对象上的一元谓词;概念是属性的布尔组合。如果一个主体意识到了一个概念，但不知道定义它的属性，我们就认为她部分地意识到了这个概念，这种逻辑允许对对象和属性进行量化，这样主体就可以对自己的不意识进行推理。然后，我们将逻辑应用于合同，我们将其视为句法对象，根据公式的真实性决定结果。我们发现，当代理不知道一些相关的属性，引用的概念，代理只有部分知道，可以提高福利。
2018-11-14 cs.LO
Signature-Based Abduction with Fresh Individuals and Complex Concepts for Description Logics (Extended Version)
Technische Universität Dresden（德累斯顿工业大学）
给定一个知识库和一个观察作为一组事实，ABox溯因旨在计算一个假设，当添加到知识库时，足以引起观察。在基于签名的ABox绑架中，进一步要求该假设仅使用给定集合中的名称。这种形式的溯因可以应用于诊断、知识库修复或解释缺失的蕴涵。只有当我们承认使用新的个体和/或从给定签名构建的复杂概念时，给定观察的假设才可能存在，这是迄今为止大多数ABox绑架方法不支持或仅支持限制的。在本文中，我们调查的计算复杂性的这种形式的绑架-允许新鲜的个人，复杂的概念，或两者兼而有之-为各种描述逻辑，并给出大小界限的假设，如果它们存在。
2021-05-01 cs.AI cs.LO
Many concepts and two logics of algorithmic reduction
在为可计算性逻辑的各个部分寻找公理化的程序中，早先证明了交互式图灵归约逻辑正是海廷直觉主义演算的蕴涵片段。这种简化允许对前件所表示的计算资源进行无限的重用。然而，一种至少同样基本和自然的算法简化是不允许这种重用的。本文表明，把第一类归约的逻辑转变为第二类归约的逻辑，只需要从它的根岑式公理化中删除收缩规则。第一种（图灵）交互式约简也有三种自然版本。虽然这三个版本彼此非常不同，但它们的逻辑行为（孤立地）是无法区分的，而这种共同行为被隐含的直觉主义逻辑精确地捕获。在本文的其他贡献是一个非正式的介绍了一系列新的-有限和有界-版本的递归操作和相关的减少操作。有关可计算性逻辑的在线资源可在http://www.cis.upenn.edu/~giorgi/cl.html上找到
2008-10-12 cs.LO math.LO
Efficient Concept Induction for Description Logics
Wright State University（莱特州立大学）
概念归纳是指创建复杂描述逻辑类描述的问题（即，TBox公理）的实例（即，ABox数据）。在本文中，我们特别关注的情况下，既有一组积极的和一组消极的情况下，并寻求复杂的类表达式下，积极的，但不是消极的例子。概念归纳已经在本体工程中找到了应用，但是现有的算法在某些情况下具有基本的性能问题，主要是因为通常需要大量的外部描述逻辑推理机的调用。在本文中，我们提出了一个新的算法，这个问题大大减少了所需的推理机调用的数量。虽然这是在一个更有限的遍历的搜索空间的代价，我们表明，我们的方法提高了执行时间高达几个数量级，而输出的正确性，测量的输入实例的正确覆盖量，在许多情况下仍然相当高。因此，我们的方法应该为现有系统提供一个强有力的替代方案，特别是在其他系统非常缓慢的情况下。
2018-12-08 cs.AI cs.LO
Rethinking Epistemic Logic with Belief Bases
CNRS-IRIT（法国国家科学研究中心-图卢兹计算机科学研究所）；Toulouse University（图卢兹大学）
我们引入了一个新的语义逻辑的显式和隐式的信念的基础上的概念，多智能体的信念基础。与现有的Kripke式认知逻辑语义学中可能世界和doxastic/epistemic alternative的概念是原始的不同，在我们的语义学中，它们是非原始的，但从信念基础的概念定义。我们提供了一个完整的公理化和证明我们的逻辑通过有限模型参数的可判定性。我们还提供了一个多项式嵌入我们的逻辑到Fagin & Halpern的一般意识的逻辑，并建立一个复杂性的结果，我们的逻辑通过嵌入。
2018-12-17 cs.AI 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
Separating Data Examples by Description Logic Concepts with Restricted Signatures
我们研究了分离的积极和消极的数据的例子中存在的本体论的描述逻辑概念。与以前的工作相比，我们添加了一个签名，指定了一个子集的符号，可用于分离，我们承认在该签名中的个人名称。我们认为弱和强的版本所产生的问题，不同的负面的例子是如何对待，我们区分分离和没有帮助符号。在这个框架内，我们比较了不同语言的分离能力和调查的复杂性，决定可分性。虽然弱可分性被证明是密切相关的保守扩展，强烈分离的概念与克雷格插值，适当定义的编码的数据和本体。这使我们能够将这些领域的已知结果转化为可分性。相反，我们得到原来的结果可分性，可以向后转移。例如，相当令人惊讶的是，ALCO中的保守扩张和弱可分性都是3ExpTime完全的。
2021-07-12 cs.LO
Category-theoretical Semantics of the Description Logic ALC (extended version)
范畴论可以用来陈述一阶逻辑中的公式，而不需要使用集合成员。逻辑学中的几个显著结果，如连续统假设的证明，可以在范畴论中优雅地重写。本文提出用范畴语言重新表述描述逻辑$\mathcal{ALC}$通常的集合论语义。在这种设置中，ALC概念被表示为对象，概念包含被表示为箭头，并且成员关系被表示为类别的对象和箭头上的逻辑量词。这种范畴理论语义提供了$\mathcal{ALC}$的语义的更模块化的表示和设计用于推理的算法的新方法。
2022-04-18 cs.LO
The logic of interactive Turing reduction
本文从可计算性逻辑的语义出发，将直觉蕴涵理解为交互式算法约简，给出了直觉演算的蕴涵片段的可靠性和完备性证明。这个概念--更准确地说，是归约的相关概念--是图灵归约从传统的输入/输出问题到任意交互程度的计算任务的概括。请访问http://www.cis.upenn.edu/~giorgi/cl.html以获得关于可计算性逻辑的全面在线资源。
2006-02-11 cs.AI cs.LO math.LO
Reasoning in the Description Logic ALC under Category Semantics
Université Sorbonne Paris Nord（索邦巴黎北大学）；INSERM（法国国家健康与医学研究院）
本文提出了一种用范畴语言用一般的T盒重新表述描述逻辑$\mathcal{ALC}$的通常的集合论语义。在此设置中，$\mathcal{ALC}$概念表示为对象，概念包含表示为箭头，成员关系表示为类别的对象和箭头上的逻辑量词。这种基于类别的语义提供了$\mathcal{ALC}$的语义的更模块化的表示。这个特性允许我们通过去掉存在性和普遍性限制之间的相互作用来定义$\mathcal{ALC}$的子逻辑，这将导致空间中的指数复杂度。这样一个子逻辑是不可定义的，在通常的集合论语义，我们表明，这个子逻辑是{ \sc{PSPACE} }，提出了一个确定性的算法检查概念可满足性，它运行在多项式空间。
2022-05-14 cs.AI cs.LO
Entropy-based Logic Explanations of Neural Networks
University of Cambridge（剑桥大学）
提出一种端到端可微的基于熵准则的方法，用一阶逻辑从神经网络中自动提取简洁形式化解释，并在四类任务中取得优于白盒、媲美黑盒的准确率。
2022-01-31 cs.AI cs.CV cs.LG
Temporal Description Logic for Ontology-Based Data Access (Extended Version)
Free University of Bozen-Bolzano（博尔扎诺自由大学）；University of Liverpool（利物浦大学）；Birkbeck, University of London（伦敦大学伯贝克学院）
我们的目标是调查基于本体的数据访问时间的有效性时间和本体能够时间概念建模的时态数据。为此，我们设计了一个时态描述逻辑，TQL，扩展了标准的本体语言OWL 2 QL，提供了基本的手段，时间概念建模，并确保一阶重写适当定义的数据实例的有效期的合取查询。
2013-04-30 cs.AI cs.LO
A Semantic Similarity Measure for Expressive Description Logics
提出了一种完全语义的度量方法，该方法能够计算概念描述之间、概念描述与个体之间或以表达性描述逻辑表达的个体之间的相似度值。它适用于符号描述，尽管它使用数值方法进行演算。考虑到描述逻辑是本体知识表示和推理的理论框架，该方法可以有效地应用于语义Web领域的凝聚和分割聚类任务。
2009-11-26 cs.AI cs.LO
Learning Concepts Definable in First-Order Logic with Counting
该研究将多对数度结构上一阶逻辑可定义分类器的亚线性时间学习结果推广至带计数的一阶逻辑FOCN，拓展到特定度界的不可知PAC学习，并证明无界度下亚线性学习不可行。
2025-07-24 cs.AI cs.LG cs.LO
Description logics as polyadic modal logics
我们研究标准描述逻辑到多元模态逻辑框架的扩展。我们通过一般关系代数，可以用来定义操作的关系，所有的arities促进一个自然的方法，这样的逻辑。作为一个具体的系统来说明我们的方法，我们调查的多元版本的ALC扩展与关系置换运算符和元组计数。本文的重点是概念性的，而不是技术性的。
2021-08-19 cs.LO
Global Explainability of GNNs via Logic Combination of Learned Concepts
University of Trento（特伦托大学）；Fondazione Bruno Kessler（布鲁诺·凯塞勒基金会）；University of Cambridge（剑桥大学）
本文提出GLGExplainer，首次将局部解释聚类为图形概念并组合成任意布尔逻辑公式，为GNN提供准确、可解释且忠实于模型预测的全局解释，并可用于诊断模型学到的错误规则。
2023-04-11 cs.AI cs.LG 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
On Free Description Logics with Definite Descriptions
明确描述是“该$x$使得$φ$”形式的短语，用于指代上下文中的单个实体。它们通常比单独的名称对用户更有意义，特别是在通过本体建模或查询数据时。我们研究自由描述逻辑与个人的名字和明确的描述作为语言的条款，同时也占他们可能缺乏外延。我们专注于扩展的$\mathcal{ALC}$和，分别，$\mathcal{EL}$与名词，普遍的作用，和明确的描述。我们表明，在这些扩展中的标准推理并不比原来的语言更难，我们使用一个合适的互模拟概念来描述相对于一阶公式的概念的表达能力。此外，我们奠定了基础，通过研究的复杂性，决定存在的明确的描述下的本体论的个人自动支持确定的描述生成。最后，我们提供了一个多项式时间减少的推理在其他自由描述逻辑语言的基础上的双域语义部分解释的情况下。
2021-06-29 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
Using Tableau to Decide Description Logics with Full Role Negation and Identity
本文提出了一种确定具有完全角色否定和角色恒等式的表达性描述逻辑的表方法。我们考虑的描述逻辑ALBOid，这是扩展的ALC与布尔角色操作符，逆的角色，身份的角色，并包括完全支持个人和单例概念。ALBOid在表达上等价于一阶逻辑的两变量片段，并包含布尔模态逻辑。在本文中，我们定义了一个健全的和完整的表演算的ALBOid，提供了一个基础，决策程序的逻辑及其所有的子逻辑。我们的方法的一个重要的新颖性是使用一个通用的无限制的阻塞机制。基于概念上简单的规则，无限制分块执行两个个体是否相等的情况区分和等式推理以找到有限模型。阻塞机制将Tableau导子的终止性证明与ALBOid的有限模型性质联系起来。
2016-11-28 cs.LO
A Parameterized Complexity View on Description Logic Reasoning
Institute for Logic, Language and Computation（逻辑、语言与计算研究所）；University of Amsterdam（阿姆斯特丹大学）
描述逻辑是一种知识表示语言，它被设计成在表达性和计算易处理性之间取得平衡。许多不同的描述逻辑已经被开发出来，并且这些逻辑的许多计算问题由于它们的计算复杂性而被研究。然而，基本上所有的复杂性分析的推理问题的描述逻辑使用的经典复杂性理论的一维框架。参数化复杂性理论的多维框架能够提供推理问题复杂性的更详细的图像。在本文中，我们认为，参数化复杂性的框架有很多可以提供的描述逻辑推理问题的复杂性分析-当一个人需要一个渐进的和前瞻性的观点参数化的复杂性工具。我们通过三个案例研究来证实我们的论点。第一个案例研究的问题是概念可满足的逻辑ALC关于近无环的TBox。第二个案例研究关注ALC概念的可满足性，其参数由联合算子的出现次数和完全存在量化的出现次数来确定。第三个案例研究从参数化复杂性的角度对数据复杂性结果进行了批判性的审视。这三个案例研究代表了描述逻辑问题的参数化复杂性方法的广泛应用。
2018-08-11 cs.AI cs.CC cs.LO
Nominalistic Logic (Extended Abstract)
名物化逻辑（NL）是对保罗·吉尔摩的内涵类型论（ITT）的一种新的表述，它是一种逻辑演算和一个简洁的名物化公理（N），在某些情况下，它允许谓词的名称作为个体。该逻辑有一个灵活的理解公理，但没有外延性公理和无穷公理，尽管公理N是导出自然数的皮亚诺公设的关键。
2008-12-28 cs.LO
Teaching Functional Programmers Logic and Metatheory
我们提出了一种新的教学方法，逻辑和逻辑元理论的学生谁有一些经验的函数式编程。我们将逻辑中的概念定义为证明助手Isabelle/HOL语言中的一系列函数程序。这使我们能够使教科书中经常不清楚的概念变得精确，通过执行它们来实验定义，并详细证明元理论定理。我们调查了学生对我们教学方法的看法，以确定其有用性，并发现学生认为我们的形式化帮助他们理解逻辑中的概念，并将其作为学习工具进行实验。然而，这种方法不足以让学生对自己设计和实现正式系统的能力充满信心。需要进一步的研究来确认和推广我们的调查结果，但我们的初步结果似乎很有希望。
2022-07-26 cs.LO cs.PL
A New Tractable Description Logic under Categorical Semantics
Université Sorbonne Paris Nord, Sorbonne Université, INSERM, Limics（巴黎-萨克雷大学、索邦大学、国家医学研究院、Limics）
本文提出一种扩展EL的逻辑，通过弱化否定来保留可计算性，同时引入范畴语义以处理负知识。
2026-03-19 cs.AI cs.LO
Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle?
当面对如何在形式证明系统中表示属性的问题时，任何用户都必须做出设计决策。我们已经证明了三个定理，从马斯金的2004年调查文章拍卖理论使用伊莎贝尔/HOL系统，我们已经产生了验证代码的组合Vickrey拍卖。一个基本的问题是如何表示一些基本概念：由于集合论在Isabelle/HOL中可用，当引入新的定义时，通常会出现平衡集合论对象和使用更典型的高阶逻辑（如函数或列表）表示的对象的数量的问题。同样，用户经常必须回答是否使用建设性定义或非建设性定义的问题。这样的决定有后果的证明发展和可用性的形式化。例如，集合通常更接近经济学家使用和识别的表示，而其他对象更接近计算内容的提取。在本文中，我们给出了这些方法的优点和缺点及其关系的例子。此外，我们提出了相应的伊莎贝尔图书馆的定义和定理，最突出的是那些处理关系和约束。
2014-06-01 cs.LO
Aleatoric Description Logic for Probailistic Reasoning (Long Version)
The University of Western Australia（西澳大学）
描述逻辑是描述本体知识库的有力工具。也就是说，它们从个人、概念和关系的角度对世界进行了事实性的描述。在存在不确定性的情况下，这种事实说明是不可行的，需要采取主观或认识的方法。随机描述逻辑通过掷骰子将世界中的不确定性建模为随机事件，其中代理人对这些骰子的偏见具有主观信念。这提供了一个主观的贝叶斯描述逻辑，其中命题和关系根据理性代理人会下什么注来分配概率，给定可能的个体和骰子的配置。任意描述逻辑一般化的描述逻辑ALC，可以看出，描述的概率空间的解释的限制ALC的所有角色的功能。考虑了几个计算问题，并提出了模型检验和一致性检验算法。最后，任意描述逻辑被证明能够建模学习，其中代理能够根据观察结果对骰子的偏见进行调节。
2021-08-30 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 Description Logic Primer
University of Oxford（牛津大学）
本文提供了一个自包含的第一次介绍描述逻辑（DL）。文中首先举例说明了DL SROIQ的主要概念和特点，然后详细定义了DL SROIQ的语法和语义。附加部分回顾了轻量级DL语言，讨论了与Web本体语言OWL的关系，并给出了进一步阅读的指针。
2013-06-03 cs.AI cs.LO
The Logic of Approximate Dependence
我们扩展处理的函数相关，依赖逻辑的基本概念，包括依赖的可能性与有限数量的例外。我们称之为近似依赖。本文的主要结果是近似依赖原子的完备性定理。我们指出了一些有问题的特点，这表明我们应该考虑多个团队，而不仅仅是团队。
2014-08-19 cs.LO math.LO
