A Survey on how Description Logic Ontologies Benefit from Formal Concept Analysis
SAP Research Center Dresden(SAP德累斯顿研究中心)
虽然概念作为共享某些属性的对象的集合的概念和概念层次的概念是形式概念分析和描述逻辑的基础,但这两个研究领域之间描述和获得概念的方式有很大不同。尽管存在这些差异,但已经有几次尝试弥合这两种形式主义之间的差距,并尝试将一个领域的方法应用于另一个领域。本文综述了描述逻辑与形式概念分析相结合的研究成果。
2011-07-14 cs.AI cs.LO
Faithful Logic Embeddings in HOL -- Deep and Shallow
Otto-Friedrich-Universität Bamberg(巴马克大学);Freie Universität Berlin(柏林自由大学)
本文提出一种在经典高阶逻辑中同时实现深嵌入与浅嵌入的方法,支持交互式与自动化定理证明、反例查找及忠实性证明,对逻辑教育、研究与应用有益。
2025-06-01 cs.AI cs.LO math.LO
Explainability via Short Formulas: the Case of Propositional Logic with Implementation
Tampere University(坦佩雷大学)
我们概念化的逻辑和公式大小的可解释性,给出了一些相关的定义,在一个非常一般的设置的可解释性。我们的主要兴趣是所谓的特殊解释问题,其目的是解释输入模型中输入公式的真值。解释是最小尺寸的公式,其(1)与输入模型上的输入公式一致,并且(2)将所涉及的真值全局地传输到输入公式,即,在每一个模型。作为一个重要的例子,我们研究命题逻辑在这种情况下,并表明,特殊的可解释性问题是完整的第二层次的多项式。我们还提供了一个实现这个问题的答案集编程和调查的能力,解释答案的n-皇后和支配集问题。
2022-10-25 cs.AI cs.LO
Sequential composition of propositional logic programs
本文研究命题逻辑程序的顺序组合与分解,证明无环程序可分解为单规则程序,并利用组合表示直接后果算子以计算最小模型,从而弥合语法与语义的鸿沟。
2023-10-11 cs.AI cs.DB cs.DM
A uniform approach to logic programming semantics
逻辑编程和非单调推理的部分理论涉及这些范式的不动点语义研究。在过去的二十年里,已经提出了几种不同的语义,其中一些比其他的更成功和更受认可。这些不同的语义背后的原理是多种多样的,这取决于一个人的观点,这可能是一个程序员的观点,也可能是受常识推理的启发,因此导致这些语义的结构在技术上是非常多样的,它们之间的确切关系还没有被完全理解。在本文中,我们提出了一个概念上的新方法,基于层次映射,它允许提供统一的表征不同的语义逻辑程序。我们将展示我们的方法,给出新的和统一的一些主要的语义,更特别的最小模型的语义明确的程序,拟合语义,和良好的基础语义的表征。弱完美模型语义的一个新的表征也将提供。
2003-11-12 cs.AI cs.LO
Orthologics for Cones
University of Lübeck(吕贝克大学);University of Bamberg(班贝格大学)
在使用知识表示(KR)技术的应用中,特别是那些结合数据驱动和逻辑方法的应用中,对象的域不是抽象的非结构化域,而是呈现出几何对象的专用的深层结构。一个例子是用于在概念空间中对自然概念建模的凸集类,它也通过凸优化技术与机器学习联系起来。在本文中,我们研究这种几何结构的逻辑。使用机器的格理论,我们描述了一个扩展的最小正交与部分模块规则,适用于封闭凸锥。该逻辑将可行的数据结构(利用凸性/圆锥性)与足够的表达性(包括完全正交负性(利用圆锥性))相结合。
2020-08-07 cs.AI cs.LO
The DL-Lite Family and Relations
Free University of Bozen-Bolzano(博尔扎诺-博岑自由大学);Birkbeck College(伯贝克学院)
最近推出的一系列描述逻辑下的共同绰号DL-Lite引起了关注的描述逻辑和语义Web社区,由于低计算复杂性的推理,一方面,和能力,以表示概念建模形式主义,另一方面。本文的主要目的是沿着五个轴对原始DL-Lite逻辑的扩展中的推理进行全面而系统的研究:通过(i)将布尔连接词和(ii)数量限制添加到概念构造,(iii)允许角色层级,(iv)允许角色不相交性、对称性、不对称性、自反性、非自反性和传递性约束,以及(v)采用或放弃唯一的相同假设。我们分析了所得到的逻辑的可满足性的组合复杂度,以及实例检查和回答肯定存在查询的数据复杂度。我们的方法是基于嵌入DL-Lite逻辑在合适的片段的一个变量的一阶逻辑,这提供了有用的见解,他们的属性,特别是计算行为。
2014-01-15 cs.AI cs.LO
A Decidable Very Expressive Description Logic for Databases (Extended Version)
KRDB Research Centre, Free University of Bozen-Bolzano(博岑-博尔扎诺自由大学 KRDB 研究中心)
我们介绍$\mathcal{DLR}^+$,扩展的n元命题封闭的描述逻辑$\mathcal{DLR}$处理属性标记的元组(概括的位置符号),关系的投影,以及全球和本地的关系对象化,能够表示包含,功能,关键,和外部的唯一性依赖。该逻辑配备了TBox和ABox公理。我们展示了如何一个简单的语法限制共享共同属性的投影在$\mathcal{DLR}^+$知识库的外观,使推理的语言决定与$\mathcal{DLR}$相同的计算复杂性。所得到的$\mathcal{DLR}^\pm$ n元描述逻辑能够更彻底地编码概念数据模型,如EER,UML和ORM。
2017-07-25 cs.AI
Should Terminology Principles be re-examined?
Condillac Research Group - Listic Lab(孔狄亚克研究小组 - Listic 实验室);Université de Savoie(萨瓦大学)
信息技术应用术语的可操作化使奥斯特方法复活。概念维度在让位于专门的词典编纂之后再次占据主导地位。术语学中本体论的出现证明了这一点。虽然Felber手册和ISO标准中定义的术语原则仍然是传统术语的核心,但它们的计算实现提出了一些问题。在这篇文章中,在重申它们的重要性的同时,我们将从双重视角重新审视这些原则:数学意义上的逻辑和知识论意义上的认识论。因此,我们将澄清和描述其中的一些,以考虑到知识工程(本体论)和形式系统(逻辑)的进步。本体术语的概念,其概念系统是一个正式的本体,结果从这种方法。
2016-09-16 cs.AI
The Information Flow Foundation for Conceptual Knowledge Organization
The Ontology Consortium(本体联盟)
不同话语社区之间的本体共享使他们能够将自己的信息结构与共享共同术语和语义的其他社区的信息结构进行比较-本体共享促进了在线知识组织之间的互操作性。本文演示了本体共享是如何形式化的信息流(IF)的概念知识模型。信息流间接地表示通过可指定的本体扩展层次结构与同义类型等效增强的共享-两个本体通过各自扩展的公共通用本体共享术语和含义。使用形式化为IF逻辑的参与者社区本体、形式化为IF理论的公共共享可扩展本体、从公共本体到可形式化为IF理论解释的参与者社区本体的参与者社区规范链接的范式,本文认为本体共享集中在社区连接的虚拟本体中,并且演示了该虚拟本体如何可计算为参与本体的融合-参与本体之和模本体共享结构的商。
2018-10-19 cs.AI cs.DL
Inseparability and Conservative Extensions of Description Logic Ontologies: A Survey
Free University of Bozen-Bolzano(博岑-博尔扎诺自由大学);University of Liverpool(利物浦大学);University of Bremen(不来梅大学);Birkbeck, University of London(伦敦大学伯贝克学院)
一个本体是否可以安全地被另一个可能更简单的本体替换的问题是许多本体工程和维护任务的基础。例如,它支持本体版本化、本体模块化、遗忘和知识交换。安全替换的含义取决于本体的预期应用。例如,如果它被用来查询数据,那么任何相关的本体中介查询的答案应该在任何相关的数据集上都是相同的;相反,如果本体被用于概念推理,那么概念表达式之间的必然包含应该一致。这就产生了不同的概念,本体不可分离,如查询不可分离和概念不可分离,推广相应的保守扩展的概念。我们调查结果的描述逻辑本体论的背景下,各种概念的不可分割性,讨论他们的应用程序,有用的模型理论的表征,算法确定是否两个本体是不可分割的(有时,计算它们之间的差异,如果他们不是),和这个问题的计算复杂性。
2018-04-20 cs.AI
Neuro-Conceptual Artificial Intelligence: Integrating OPM with Deep Learning to Enhance Question Answering Quality
Tokushima University(德岛大学);Technion – Israel Institute of Technology(以色列理工学院)
本文提出 NCAI 框架,利用 OPM 概念建模与上下文内学习增强深度学习问答系统,并通过透明度指标验证其在推理透明性和答案准确性上的优势。
2025-02-12 cs.AI cs.CL
Conceptual completeness for subgeometric logics
University of Gothenburg(哥德堡大学);Université Paris Cité, CNRS, IRIF(巴黎西岱大学、法国国家科学研究中心、信息与随机研究所);University of Cambridge(剑桥大学)
研究几何逻辑片段的“概念完备性”,通过理论与拓扑斯之间的对偶刻画,证明相干逻辑等片段在完整几何逻辑中保守嵌入,并等价于基于集合模型的传统重构定理。
2026-07-03 cs.LO math.CT math.LO
Counting Distinctions: On the Conceptual Foundations of Shannon's Information Theory
范畴逻辑已经表明,现代逻辑本质上是子集逻辑(或“子子集”)。划分是子集的对偶,因此存在划分的对偶逻辑,其中“区别”[来自全域U的不同元素(u,u ')的有序对]是“元素”的对偶。在子集中的元素类似于U上的划分p,从而进行区分,即,如果u和u'在p的不同块中。子集逻辑通过将(拉普拉斯)概率作为有限论域的每个子集事件的归一化大小而导致有限概率论。划分逻辑中的类似步骤是将划分的区分数分配给划分,该区分数由来自有限论域的有序对|UxU|的总数归一化。这就产生了划分的“逻辑熵”概念和“逻辑信息论”。“逻辑理论直接计算分区中的(标准化)区别数量,而香农的理论给出了做出这些相同区别所需的二进制分区的平均数量。因此,逻辑理论被看作是为香农的理论提供了一个概念性的基础上的逻辑概念的“区别”。“(即将发表于《综合》)
2009-02-11 cs.IT cs.LO math.IT
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
Description logics as polyadic modal logics
我们研究标准描述逻辑到多元模态逻辑框架的扩展。我们通过一般关系代数,可以用来定义操作的关系,所有的arities促进一个自然的方法,这样的逻辑。作为一个具体的系统来说明我们的方法,我们调查的多元版本的ALC扩展与关系置换运算符和元组计数。本文的重点是概念性的,而不是技术性的。
2021-08-19 cs.LO
Specification-Driven Data Architecture Reconstruction: From Physical Code to Logical and Conceptual Specifications
EPAM Systems
本研究提出溯源感知、确定性优先的流水线,从Oracle DDL重构逻辑与概念数据规范,区分观察事实、推导与LLM建议;在249个样本上完成97.99%,LLM候选父表可接受率仅约17.5%,验证了防止模型假设被静默提升的架构基线。
2026-09-15 cs.DB cs.LO cs.SE
Terminating Tableaux for Graded Hybrid Logic with Global Modalities and Role Hierarchies
我们提出了一个具有全局模态、自反性、传递性和角色层次的分级混合逻辑的终止表演算。系统的终止是通过基于模式的阻塞实现的。以前的相关逻辑方法都依赖于基于链的阻塞。除了在概念上简单,适合高效的实现,基于模式的方法给我们一个NExpTime的决策过程的复杂性。
2011-03-22 cs.LO
Reactive Temporal Logic
虽然标准的处理时间逻辑是足够的封闭系统,没有运行时与他们的环境相互作用,他们没有反应系统,通过同步的动作与他们的环境进行交互。本文介绍了反应时态逻辑,一种适用于反应系统研究的时态逻辑形式。我说明了它的使用,应用它来制定一个公平的调度定义,和一个正确的互斥协议。这些概念之前的定义在概念上更加复杂或不太精确,导致了关于给定协议是否满足隐含要求的争论。
2020-08-31 cs.LO
On the Lattice of Conceptual Measurements
University of Kassel(卡塞尔大学)
本文提出了一种基于形式概念分析的尺度度量的数据集尺度度量方法,封闭系统之间的连续映射,并导出一个规范表示。此外,我们还证明了所述标度测度关于闭包系统是格序的。这使得通过使用meet和join操作来探索尺度度量集成为可能。此外,我们表明,格的规模措施是同构的子闭包系统,从原始数据产生的格。最后,我们提供了另一种表示的规模措施,使用命题逻辑的数据集的功能。我们的理论研究结果进行了讨论的例子。
2020-12-09 cs.AI cs.LG cs.LO
Classical logic, classical probability, and quantum mechanics
我们给出了一个概述和概念上的讨论,我们的一些结果的上下文和非局部性。我们特别关注与伊塔马尔Pitowsky的工作相关多面体,贝尔不等式,布尔的“条件可能的经验”的连接。
2020-10-23 cs.LO math.PR quant-ph
Impure Simplicial Complex and Term-Modal Logic with Assignment Operators
本文提出一种带有赋值运算的术语模态逻辑,用于解决不纯单纯复形中死亡智能体表达式的问题,并通过双射概念证明两种语义等价,同时提供完整的公理化体系。
2025-11-27 cs.LO cs.MA
Towards Syntactic Epistemic Logic
本文提出句法认识逻辑(SEL),将认识情境视为句法条件集合,以捕捉不完整描述,并填补认识博弈论中句法与语义表示之间的鸿沟。
2022-12-30 cs.LO
Gradual Classical Logic for Attributed Objects - Extended in Re-Presentation
我们对事物的理解是概念性的。通过陈述我们对对象进行推理,事实上我们操纵的不是对象,而是涉及它们的概念。现在,只要我们承认一个对象所从属的无限延伸的概念,如空间、时间、大小、颜色等,简言之,任何合理的性质,就不可能在涉及对象的概念中肯定原子性。然而,形式/符号逻辑通常假定其他表达式建立在其上的原子实体。我们能把我们对概念的直觉反映到形式/符号逻辑上吗?我保证我们可以,但是关于原子性的通常观点需要检查。在这项工作中,我提出了渐进的逻辑,具体化的观察,我们不能区分是否被视为原子实体是原子或只是原子足以不被认为是非原子。其动机是捕捉自然发生在具有属性的概念周围的某些现象,包括预设和反义词。我提出的逻辑细节的逻辑,然后映射到形式语义。两个语言学上有趣的语义将被考虑。可决定性已经显现。
2015-04-19 cs.AI cs.CL cs.LO
Tableau-based decision procedure for the multi-agent epistemic logic with all coalitional operators for common and distributed knowledge
Roskilde University(罗斯基勒大学);Technical University of Denmark(丹麦技术大学);University of Johannesburg(约翰内斯堡大学);University of the Witwatersrand(威特沃特斯兰德大学)
我们开发了一个概念清晰,直观,可行的决策程序,用于测试可满足性在充分的多智能体认知逻辑CMAEL(CD)与运营商的共同和分布式知识的语言中提到的所有联盟的代理。为此,我们引入了CMAEL(CD)的Hintikka结构,并证明了在这种结构中的可满足性等价于标准模型中的可满足性。使用该结果,我们设计了一个增量的tableau建设过程,最终构建一个令人满意的Hintikka结构的CMAEL(CD)的公式的每一个可满足的输入集,并关闭每一个不可满足的输入集的公式。
2012-01-25 cs.AI cs.LO math.LO
Using Tableau to Decide Description Logics with Full Role Negation and Identity
本文提出了一种确定具有完全角色否定和角色恒等式的表达性描述逻辑的表方法。我们考虑的描述逻辑ALBOid,这是扩展的ALC与布尔角色操作符,逆的角色,身份的角色,并包括完全支持个人和单例概念。ALBOid在表达上等价于一阶逻辑的两变量片段,并包含布尔模态逻辑。在本文中,我们定义了一个健全的和完整的表演算的ALBOid,提供了一个基础,决策程序的逻辑及其所有的子逻辑。我们的方法的一个重要的新颖性是使用一个通用的无限制的阻塞机制。基于概念上简单的规则,无限制分块执行两个个体是否相等的情况区分和等式推理以找到有限模型。阻塞机制将Tableau导子的终止性证明与ALBOid的有限模型性质联系起来。
2016-11-28 cs.LO
Logic, Individuals and Concepts
这个扩展的摘要给出了描述和变量概念之间的联系的简要概述。因此,概念的概念被扩展到包括语法和语义特征。使用中的评估图通过一种计算环境(索引)进行参数化,从而产生索引概念。这些概念通过高阶逻辑的描述而被植入语言之中。一般来说,对象作为函子的思想应该有助于设计者以概念性的外壳风格来概述编程工具。
2001-06-12 cs.DB cs.DM 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
Correct-by-Construction G-Code Generation: A Neuro-Symbolic Approach via Separation Logic
SLING AI Inc.(SLING AI 公司)
本文提出了一种神经符号框架,通过分离逻辑证明器将GLLM方法的神经生成能力与形式验证相结合,利用几何数据构建两组件架构,将物理碰撞转化为逻辑空间数据 race,从而生成自我校正的G代码生成系统,减少人工监督,提高自主制造的安全性和验证性。
2026-05-20 cs.LO cs.SE
Learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes
University of Trieste(的里雅斯特大学);Saarland University(萨尔兰大学);Technical University of Munich(慕尼黑工业大学);University of Technology, Vienna(维也纳技术大学)
本文在信号时序逻辑(STL)公式上引入了一个相似度函数。它以核函数的形式出现,在机器学习中作为一种概念上和计算上高效的工具而闻名。相应的核技巧使我们能够绕过复杂的特征提取过程,即(通常是手动)努力识别公式的决定性属性,以便可以应用学习。我们证明了这一结果及其在预测STL公式对随机过程的(定量)满意度的任务上的优势:使用我们的内核和内核技巧,我们学习(i)计算效率高(ii)实际上精确的满意度预测器,(iii)避免困难的任务,找到一种方法,以合理的方式显式地将公式转化为数字向量。我们通过理论上合理的PAC保证来支持我们在实验中实现的高精度,确保我们的程序有效地提供接近最佳的预测器。
2022-01-24 cs.LG cs.LO
Logical Modelling in CS Education: Bridging the Natural Language Gap
针对逻辑形式化中选择词汇表这一被忽视的步骤,提出包含丰富语言和NLP检查反馈的概念框架,在Iltis系统中实现并验证了其有效性。
2025-04-30 cs.CY cs.LO