ECA-RuleML: An Approach combining ECA Rules with temporal interval-based KR Event/Action Logics and Transactional Update Logics
事件驱动架构（EDA）中需要解决的一个重要问题是如何正确有效地捕获和处理基于事件/动作的逻辑。本文致力于弥合之间的差距的知识表示（KR）方法的基础上持久的事件/动作和事件演算等形式主义，一方面，和事件-条件-动作（ECA）反应规则扩展的主动数据库的方法，查看事件的瞬时发生和/或事件序列，另一方面。我们提出了基于反应规则（ECA规则）和一种新的基于间隔的事件逻辑的形式主义，并提出了具体的基于规则ML的语法，语义和实现。我们进一步评估这种方法的理论，实验和一个例子来自常见的行业用例，并说明其好处。
2006-11-10 cs.AI cs.LO cs.MA
Combining Event Calculus and Description Logic Reasoning via Logic Programming
本文介绍了一种在逻辑程序设计框架下将事件演算与描述逻辑相结合的知识表示语言。其目的是为用户提供一种表达语言，用于建模和分析随时间演变的系统。该方法的例子与逻辑程序设计语言中实现的Fusarium系统。本文扩展了Fusarium的规则语言与描述逻辑$\cal ALCIF$的弱DL-安全接口，并使事件演算适应这种扩展语言。通过这种方式，带时间戳的ABOX可以在事件演算中作为流畅项进行操作。这一切都是在福柯的时间分层概念的框架内进行的。本文件酌情提供了健全性和完整性的条件。使用一个详细的例子，它演示了事件演算，描述逻辑和逻辑编程规则的相互作用，用于计算可能的模型作为合理的解释的建模系统的当前状态。
2021-09-10 cs.LO
Combining Logic Programs and Monadic Second Order Logics by Program Transformation
本文提出了一种基于展开/折叠变换规则的程序合成方法，该方法可用于从一个后继者的弱一元二阶理论（WS 1 S）的公式导出可终止的确定性逻辑程序。这种综合方法也可作为WS_（1 S）封闭公式的判定过程的证明方法。我们应用我们的综合方法翻译CLP（WS 1 S）程序到逻辑程序，我们也使用它作为一种证明方法来验证无限状态系统的安全性。
2003-11-27 cs.LO cs.PL
Combining First-Order Classical and Intuitionistic Logic
本文从证明论的角度研究了Humberstone（1979）和del Cerro and Herzig（1996）研究的直觉主义和经典命题逻辑组合C+J的一阶展开。C+J同时具有经典蕴涵和直觉蕴涵，而我们的一阶扩展在C+ J中增加了经典和直觉全称量词以及一个存在量词.本文为我们的一阶直觉逻辑和经典逻辑的结合提供了一个多后继的代数演算G（FOC+J）.我们的正则演算G（FOC+J）将直觉蕴涵和直觉全称量词的正确规则的上下文限制在特定形式的公式中。为了保证子公式的性质，建立了割消定理。作为推论，G（FOC+J）在一阶直觉逻辑和经典逻辑上都是保守的。通过一个典范模型论证证明了G（FOC+J）的强完备性.
2022-04-14 cs.LO
Combining fragments of classical logic: When are interaction principles needed?
我们研究了经典逻辑片段的组合，作为通过添加新的连接词来保守扩展给定布尔逻辑的一种方式，并且我们精确地描述了这样的组合在包含来自两个片段的连接词的签名上产生相应的经典逻辑片段的情况。作为输入。如果由此产生的组合片段只是不完全地被作为输入的成分所表征，这意味着来自一个成分的连接词需要与来自另一个成分的连接词相互作用，从而产生相互作用原则。主要的贡献强烈依赖于（众所周知的）描述的2值克隆后，（不那么知名）公理化程序的2值矩阵奠定了劳滕贝格，并对阿夫隆的非确定性矩阵，这已（最近）被用来产生一个显着的进步理解的语义fibring。
2018-10-16 cs.LO
Decidable Logics Combining Word Equations, Regular Expressions and Length Constraints
在这项工作中，我们考虑的可满足性问题的逻辑，结合字方程的字符串变量表示的话的无限长度，正则语言的话属于Presburger限制的话的长度。我们提出了一种新的决策过程，在两个可决策的片段，包括二次字方程（即，每个字符串变量最多出现两次）。所提出的过程减少了问题解决的Presburger算法的可满足性。该过程结合了两个主要组成部分：（i）一个算法，以获得一个完整的一组所有的解决方案的词方程和正则表达式的连接;和（ii）两种方法，以精确计算关系约束的字符串长度所隐含的所有solutions.We已经实现了一个原型工具，并评估了一组可满足性问题的逻辑。实验结果表明，该工具是有效和高效的。
2018-05-23 cs.LO
Combining Global and Local Merges in Logic-based Entity Resolution
Bordeaux INP（波尔多国立理工学院）；Sapienza University of Rome（罗马第一大学）；Cardiff University（卡迪夫大学）
本文扩展 Lace 框架以支持数据值的局部合并，从而在全局实体引用识别之外更自然地处理同一字符串在不同上下文中指向不同实体的情况，并研究了新形式体系的计算性质。
2023-05-29 cs.AI cs.DB cs.LO
Combining swap structures: the case of Paradefinite Ivlev-like modal logics based on FDE
本文提出基于快照叠加的交换结构组合新方法，将四值Ivlev型模态系统与FDE的四值扩展IDM4结合，得到6种保守扩张的六值超有限模态逻辑，给出其希尔伯特公理系统与Prolog判定程序。
2024-04-18 cs.LO math.LO
Combining Deduction Modulo and Logics of Fixed-Point Definitions
归纳和共归纳规范在计算系统的形式化中有着广泛的应用。这样的规范在支持定点定义的逻辑中有一个自然的再现。另一个有用的形式化手段是递归规范。这些规范不直接由定点推理技术补充，相应地，不必满足强单调性限制。我们将展示如何将重写功能到逻辑的定点定义对另外支持递归规范。特别是，我们描述了一个自然的演绎演算，增加了一种形式的“封闭世界”的平等-一个关键的成分，以支持定点定义-演绎模，一个框架，用于扩展一个逻辑与重写层操作公式。我们表明，我们的演算具有很强的规范化时，重写系统满足一般属性，我们证明了它的有用性，在指定和推理基于语法的描述。将封闭世界等式整合到演绎模中，使我们重新配置了这种形式的等式的消除原理，第一次解决了关于归约下有限证明的稳定性问题。
2012-04-27 cs.LO
Automating Access Control Logics in Simple Type Theory with LEO-II
Garg和Abadi最近证明了著名的访问控制逻辑可以以一种合理和完整的方式转换为模态逻辑S4。我们之前已经概述了正常的多模态逻辑，包括单峰逻辑K和S4，可以嵌入简单的类型论（也称为高阶逻辑），我们已经证明了高阶定理证明器LEO-II可以自动推理。在本文中，我们结合这些结果，并描述了一个声音和完整的嵌入不同的访问控制逻辑在简单的类型论。采用这个框架，我们表明，现成的定理证明LEO-II可以应用于自动推理突出的访问控制逻辑。
2009-03-04 cs.AI cs.LO
Combining generic judgments with recursive definitions
程序设计语言的许多语义方面，如它们的操作语义和它们的类型赋值演算，都是通过描述适当的证明系统来指定的。最近的研究已经确定了两个证明理论的功能，允许直接的，基于逻辑的推理这样的描述：原子判断的治疗固定点（递归定义）和编码的约束结构通过通用的判断。然而，包含这两个特征的逻辑迄今为止一直在正交地处理它们：也就是说，它们不提供定义对象逻辑属性的能力，这些属性本身依赖于绑定的内在处理。我们提出了一个新的和简单的集成这些功能的直觉逻辑增强与感应自然数，我们表明，由此产生的逻辑是一致的。集成的关键好处是，它允许递归定义不仅编码简单的，传统形式的原子判断，而且还捕获与这些判断有关的通用属性。这种逻辑的有用性说明了它如何可以提供优雅的处理对象逻辑的情况下，出现在证明涉及类型演算和任意级联的替代，发挥作用，在reductionalarguments。
2008-04-14 cs.LO
How to combine diagrammatic logics
本文是竞赛的投稿：如何结合逻辑？在2010年的世界大会和学校的普遍逻辑III。我们主张，如果这些事物可以被看作一个范畴的对象，那么组合“事物”，无论这些事物是什么，都会变得更容易。我们定义了图解逻辑的范畴，使得范畴构造可以用于组合图解逻辑。作为一个例子，使用opfibration逻辑的组合，为了研究计算的副作用，由于在执行命令式程序的状态的演变。
2009-11-19 cs.LO math.CT
Transaction Logic with (Complex) Events
CENTRIA - Dep. de Informática（人工智能与计算机科学研究中心）
这项工作涉及的问题相结合的反应功能，如响应事件和定义复杂事件的能力，在一般的知识库（KBs）的事务的执行。以此为目标，我们建立在事务逻辑（TR）上，这是一种精确设计的逻辑，用于在任意逻辑理论定义的KB中建模和执行事务。在它中，事务以逻辑编程风格编写，通过将通用KB上的原始更新操作与通常的逻辑编程连接词和一些额外的连接词相结合，例如用于表达动作序列。虽然TR是处理事务的自然选择，但TR是否可以用于表示复杂事件，以及同时处理复杂事件的检测和事务的执行仍然是一个问题。在本文中，我们表明，前者是可能的，而后者是不。为此，我们首先说明TR如何表达复杂事件，特别是如何在逻辑中翻译SNOOP事件表达式。之后，我们展示了为什么TR不能同时处理这两个问题，并提出了带事件的事务逻辑，它的语法，模型理论和执行语义来解决预期的问题。所实现的解决方案是TR的非单调扩展，它保证了在事务中检测到的每个复杂事件都必须得到响应。
2014-05-15 cs.AI cs.LO
Combining Representation Learning with Logic for Language Processing
University College London（伦敦大学学院）
许多自然语言处理和自动化知识库完成任务的当前技术水平由表示学习方法保持，该方法经由基于梯度的优化来学习符号的分布式向量表示。它们只需要很少或根本不需要手工制作的功能，从而避免了大多数预处理步骤和特定于任务的假设。然而，在许多情况下，表示学习需要大量带注释的训练数据来很好地推广到看不见的数据。这种标记的训练数据由人类注释者提供，注释者通常使用形式逻辑作为用于指定注释的语言。本文研究了不同的组合表示学习方法与逻辑，以减少需要的注释训练数据，并提高泛化。
2017-12-27 cs.CL cs.LG cs.LO
Quantified Multimodal Logics in Simple Type Theory
German Research Center for Artificial Intelligence (DFKI GmbH)（德国人工智能研究中心（DFKI GmbH））；International University of Germany（德国国际大学）；Jacobs University Bremen（不来梅雅各布大学）；Universität des Saarlandes（萨尔大学）
我们提出了一个简单的嵌入量化多模态逻辑的简单类型论，并证明其可靠性和完备性。模态算子被一类可能世界上的量化所取代。我们提出了简单的实验，使用现有的高阶定理证明，证明嵌入允许自动证明这些逻辑中的语句，以及它们的Meta属性。
2009-05-14 cs.AI cs.LO
Automating Quantified Multimodal Logics in Simple Type Theory -- A Case Study
German Research Center for Artificial Intelligence (DFKI GmbH)（德国人工智能研究中心（DFKI 有限公司））；International University of Germany（德国国际大学）；Jacobs University Bremen（不来梅雅各布大学）；Universität des Saarlandes（萨尔大学）
在一个案例研究中，我们调查是否现成的高阶定理证明器和模型生成器可以用来自动推理和量化的多模态逻辑。在我们的实验中，我们利用新的TPTP基础设施的经典高阶逻辑。
2009-05-27 cs.AI cs.LO
A Two-Level Approximate Logic Synthesis Combining Cube Insertion and Removal
近似计算是降低容错系统设计复杂度的一种有吸引力的范例，从而提高性能并节省功耗。在这项工作中，我们提出了一个新的两级近似逻辑综合方法的基础上立方体插入和删除过程。实验结果表明，显着的文字计数和运行时间减少相比，国家的最先进的方法。该方法的可扩展性示出了一个高的错误阈值在大型基准电路。所得到的解决方案已提出了文字数减少高达38%，56%和93%，相对于出错率为1%，3%和5%，分别。
2021-11-22 cs.AR cs.LO cs.OH
How to Be Both Rich and Happy: Combining Quantitative and Qualitative Strategic Reasoning about Multi-Player Games (Extended Abstract)
我们提出了一个逻辑框架，结合了对多人博弈中代理人通过优化收益或结果偏好来实现定量目标的能力的博弈论研究，以及对玩家实现玩家定性目标的能力的逻辑分析，即，达到或保持具有期望属性的游戏状态。我们丰富的并发游戏模型与支付的范式游戏与模型的状态，并提出了一个定量扩展的逻辑ATL*，使定量和定性推理相结合。
2013-03-04 cs.LO cs.MA
Combining Logic with Large Language Models for Automatic Debugging and Repair of ASP Programs
本文提出 FormHe，融合逻辑故障定位、程序变异与 LLM，自动识别并修复学生提交的错误 ASP 程序，实验显示故障检测准确率达 94%、修复成功率达 58%。
2024-10-28 cs.LO cs.SE
Differentiable Probabilistic Logic Networks
SingularityNET Foundation（SingularityNET基金会）；ITMO University（ITMO大学）
概率逻辑推理是OpenCog等认知架构的核心组件。然而，作为一个综合架构，OpenCog通过混合不同的推理方法促进认知协同。在本文中，我们介绍了一个可微版本的概率逻辑网络，规则操作张量真值的方式，一个链的推理步骤构建一个计算图的张量，接受真值的前提知识库作为输入，并产生真值的结论作为输出。这允许通过结合子符号优化和符号推理的反向传播来学习前提的真值和规则的公式（以具有可训练权重的形式指定）。
2019-07-10 cs.AI cs.LO
SCTL: Towards Combining Model Checking and Proof Checking
模型检验和自动定理证明是形式化方法的两大支柱。本文从自动定理证明的角度研究模型检验，旨在将自动定理证明的表达性和模型检验的完全自动性结合起来。本文的重点是Kripke模型的时序逻辑性质的验证。本文的主要贡献是：首先定义了一个允许多元谓词符号的扩展计算树逻辑，然后以Kripke模型为参数，为该逻辑设计了一个证明系统，然后设计了一个用于该演算的证明搜索算法和一个新的自动定理证明器来实现它。验证过程是完全自动的，并且在属性不成立时产生一个反例，或者证书实验结果比较以及现有的国家的最先进的工具，在一些基准，包括应用到空中交通管制和设计选择，导致这种效率进行了讨论。
2017-09-30 cs.LO
A Simple Doxastic Deontic Logic for Norm-Guided Decision Making
TU Wien（维也纳工业大学）
本文提出一种简单的信念道义逻辑，用于在冲突规范和不完整信息下进行决策，并定义了信念规范合规优化问题，区分主观与客观优化，并给出可归约为加权部分MaxSAT的条件。
2026-10-02 cs.AI cs.LO
The Logic of XACML - Extended
我们研究了XACML 3.0国际标准描述安全访问控制策略的组合方式。我们的主要贡献是得到一个逻辑，准确地捕捉背后的标准的想法，并正式定义语义的政策结合算法的XACML。为了防止建模文物，我们提供了一种替代的方式来表征的政策结合算法，我们正式证明这些方法的等价性。这使我们能够查明以前的方法的缺点，形式化的基础上，无论是在贝尔纳普逻辑或D-代数。
2011-10-17 cs.CR cs.LO
Undecidability of a Very Simple Modal Logic with Binding
我们展示了什么可以说是最简单的非子布尔模态逻辑的约束力的隐式概念的可满足性问题的不可判定性。这一工作丰富了从混合逻辑到记忆逻辑的关于模态逻辑不可判定性的一系列已有结果。
2015-08-14 cs.LO
A Logic-Independent IDE
作者的MMT系统提供了一个定义和实现逻辑系统的框架。通过将MMT与jEdit文本编辑器相结合，我们获得了一个逻辑独立的IDE。IDE功能包括一些高级功能，如上下文相关的自动完成、搜索和更改管理。
2014-10-30 cs.HC cs.LO
On Combining Linear-Based Strategies for Tabled Evaluation of Logic Programs
表求值是一种公认的、功能强大的技术，它克服了传统Prolog系统在处理递归和冗余子计算方面的局限性。我们可以区分两个主要类别的制表机制：基于悬浮的制表和线性制表。虽然基于挂起的机制通常被认为获得更好的结果，但它们具有更多的存储空间需求，并且比线性制表机制更复杂和更难实现。可以说，SLDT和RSDT策略是标准线性表格评估的两个最成功的扩展。在这项工作中，我们提出了一个新的战略，命名为DRS，我们提出了一个框架，顶部的雅普系统，支持所有这三个战略的组合。我们的实现共享底层执行环境和用于在Yap中实现制表的大多数数据结构。因此，我们认为，所有这些共同的特点，使我们能够在这些不同的线性制表策略之间进行第一次和公平的比较，因此，更好地了解各自的优点和缺点，当单独使用或与其他组合。
2011-07-26 cs.LO
Combining Proofs for Description Logic and Concrete Domain Reasoning (Technical Report)
本文针对扩展有理数具体域的轻量级描述逻辑，提出可提取证明的推理过程，并将其与纯DL推理结合，生成同时解释DL与CD推理的集成证明。
2023-08-07 cs.LO
Lexicographic Logic: a Many-valued Logic for Preference Representation
University of Athens（雅典大学）
逻辑形式主义提供了一种自然和简洁的方式来指定和推理偏好。在本文中，我们提出了词典逻辑，经典命题逻辑的扩展，可以表达各种偏好，最显着的词典。建议的逻辑支持一个简单的新的连接，其语义可以定义在有限的真值列表。我们证明，尽管众所周知的理论限制，构成障碍的词典偏好的定量表示，存在一个子集的有理数，建议的新的连接可以自然地定义。词典逻辑可以用来以简单的方式定义一些众所周知的优先运算符，如“$A$和如果可能的话$B$“和“$A$或失败的$B$“。此外，许多其他层次优先运营商可以使用系统的方法来定义。我们认为，新的逻辑是一个有效的形式主义排名查询结果，根据用户的喜好满意度。
2020-12-20 cs.AI cs.LO
Can Graph Neural Networks Help Logic Reasoning?
Georgia Tech（佐治亚理工学院）；Siemens（西门子）；UIUC（伊利诺伊大学厄巴纳-香槟分校）；Ant Financial（蚂蚁金服）
有效地结合逻辑推理和概率推理一直是机器学习的长期目标：前者具有利用小训练数据进行概括的能力，而后者提供了处理噪声数据的原则框架。然而，现有的方法结合两个世界的最佳典型的计算密集型。在本文中，我们专注于马尔可夫逻辑网络，并探讨使用图神经网络（GNNs）表示概率逻辑推理。从我们的分析中可以看出，GNN的表示能力不足以完成这样的任务。相反，我们提出了一个更具表达力的变体，称为MAGNN，它可以执行有效的概率逻辑推理，同时能够扩展到大量的实体。我们通过几个基准数据集证明了BEGGNN具有将概率逻辑推理推进到下一阶段的潜力。
2019-09-20 cs.LG cs.LO stat.ML
A state vector algebra for algorithmic implementation of second-order logic
我们提出了一个数学框架映射到一个简单的状态向量代数的二阶逻辑关系。利用这种代数，集合论的基本定理可以用算法的方式证明，因此可以用专家系统证明。我们用简单的例子说明了代数的使用，并表明，原则上，基本集合论的所有定理都可以用初等的方法恢复。所开发的技术可用于一阶和二阶逻辑的自动定理证明。
2015-11-18 cs.AI cs.LO
Bound Propagation meets Constraint Simplification: Improving Logic-based XAI for Neural Networks
Department of Computer Science, Instituto Federal do Ceará (IFCE)（计算机科学系，巴西塞阿拉联邦大学（IFCE））
本文通过结合边界传播与约束简化，显著提升了基于逻辑的神经网络可解释性方法的效率，减少了高达89.26%的解释时间。
2026-03-02 cs.LG cs.LO
A simple sequent calculus for nominal logic
名词逻辑是一阶逻辑的变体，它支持抽象语法中的绑定名称的推理。名词逻辑的一个关键特征是新量词，它对新名称（迄今为止未出现在任何值中的名称）进行量化。以前的尝试已经作出了开发方便的规则推理与新的量词，但我们认为，这些尝试都是不完全令人满意的。在这篇文章中，我们开发了一个新的numerical演算的名义逻辑中的规则，新的量词是比以前的尝试简单得多。我们还证明了几个结构和元理论的性质，包括削减消除，一致性，和等价的皮茨公理化的名义逻辑。
2013-12-17 cs.LO
Combining Axiomatic Models for Refinement Proofs
Sabancı University（萨班哲大学）
研究精化证明如何与公理程序逻辑交互，通过模拟关系传递状态安全属性，并将模拟义务简化为现成功能逻辑中的三元组。
2026-06-29 cs.LO
Combining Rules and Embeddings via Neuro-Symbolic AI for Knowledge Base Completion
IBM Research（IBM研究院）
最近对知识库补全（KBC）的兴趣导致了基于强化学习、归纳逻辑程序设计和图嵌入的大量方法。特别是，基于规则的KBC导致了可解释的规则，同时在性能上与图嵌入相当。即使在基于规则的KBC中，也存在不同的方法，导致不同质量的规则，以前的工作并不总是精确地突出这些差异。困扰大多数基于规则的KBC的另一个问题是关系路径的不一致性：一些关系序列出现在非常少的路径中，而另一些关系序列出现得非常频繁。在本文中，我们证明了并非所有基于规则的KBC模型都是相同的，并提出了两种不同的学习方法：1）混合关系和2）混合路径。当在神经符号AI之上实现时，后者通过将布尔逻辑扩展到实值逻辑来学习规则，后者模型在平均倒数排名方面的KBC准确性优于最先进的基于规则的KBC 2-10%。此外，为了解决关系路径的不一致性，我们将基于规则的KBC与图嵌入相结合，从而进一步改善了我们的结果，并实现了两全其美。
2021-09-16 cs.AI cs.LG cs.LO
DeepLogic: Towards End-to-End Differentiable Logical Reasoning
Imperial College London（帝国理工学院）
将机器学习与基于逻辑的专家系统相结合，以获得两个世界的最佳效果，正变得越来越流行。然而，机器学习在多大程度上可以学习基于规则的知识进行推理仍然是一个悬而未决的问题。在本文中，我们将探讨如何符号逻辑，定义为逻辑程序在字符级别，学习表示在一个高维向量空间使用基于RNN的迭代神经网络进行推理。我们创建了一个新的数据集，定义了12类逻辑程序，举例说明增加了逻辑推理的复杂性，并以端到端的方式对网络进行训练，以了解逻辑程序是否需要给定的查询。我们分析了如何学习推理算法产生的原子，文字和规则的表示在逻辑程序和评估对增加长度的谓词和常量符号，以及增加多跳推理的步骤。
2019-03-07 cs.AI cs.LO cs.NE
Another Combination of Classical and Intuitionistic Conditionals
一方面，经典逻辑是一个非常成功的理论，即使不是完美的。另一方面，直觉主义逻辑无疑是最重要的非经典逻辑之一。但是，一种逻辑的支持者如何看待另一种逻辑？本文着重讨论其中一个方向，即古典主义者如何看待直觉主义逻辑。为此，我们引入了积极的直觉主义逻辑的扩展，语义和证明理论，并建立健全和强完备性。此外，我们还讨论了析取的有趣地位，以及经典逻辑与最小逻辑结合的可能性。我们还比较了我们的系统与卡尔斯鲁厄和拉莫斯的系统。
2022-04-14 cs.LO
Reasoning in Non-normal Modal Description Logics
非正规模态逻辑，解释的邻域模型，概括了通常的关系语义，已发现应用在几个领域，如认识论，道义，和联盟推理。在这里，我们提出了初步的结果推理的模态描述逻辑的一个家庭，通过结合ALC与非正规模态算子。首先，我们提供了一个框架的终止，正确的，和完整的Tableau算法来检查满足性的公式在这样的逻辑与语义的基础上变化的域。然后，我们调查的可满足性问题，这些语言的片段，通过限制应用程序的模态算子的公式，并解释模型与常数域，提供紧密的复杂性结果。
2022-06-30 cs.LO
A Simple Logic of Functional Dependence
本文提出了一个简单的可判定逻辑的功能依赖LFD，在经典命题逻辑的依赖原子和依赖量词作为模态处理的基础上，一阶逻辑的广义赋值语义的设置。探讨了LFD的表达强度、完备证明演算和元性质。各种语言扩展，以及，不可判定模态风格的独立性和动态逻辑的变化依赖模型。最后，更具体的设置相关性进行了讨论：连续依赖的拓扑模型，线性依赖的向量空间，时间依赖的动力系统和游戏。
2021-03-27 cs.LO math.LO
A simple combinatorial proof for small model property of two-variable logic
给出了二变量逻辑的{ \em小模型性质}的另一个证明。据我们所知，现有的证明这一性质严重依赖于模型理论的概念。相比之下，我们的是纯粹的组合，只使用了一个非常简单的计数参数，我们发现这是相当直观和优雅的。
2020-06-02 cs.CC cs.LO
Lilac: A Modal Separation Logic for Conditional Probability
本文提出分离逻辑 Lilac，用分离合取刻画概率独立性，并基于分解理论引入条件概率推理模态，成功形式化验证了依赖条件独立结构的加权采样算法。
2023-05-26 cs.LO cs.PL
A First-Order Logic for Reasoning about Knowledge and Probability
我们提出了一个一阶概率认知逻辑，它允许结合运营商的知识和概率在一组可能无限多的代理。所提出的框架是Fagin和Halpern（J.ACM 41：340- 367，1994）的逻辑的一阶扩展.我们定义了它的语法和语义，并证明了相应的公理系统的强完备性。
2019-01-21 cs.LO
About the unification type of simple symmetric modal logics
正规模态逻辑中的统一问题是确定给定公式F，是否存在替换s使得s（F）在该逻辑中。在这种情况下，s是F的一个统一子。我们将说，一个可统一公式F的一组统一子是完备的，如果对于F的所有统一子s，在该组中存在F的一个统一子t，使得t比s更一般。当一个可统一公式没有最小完备的统一子集时，这个公式是空的。本文证明了KB、KDB和KTB具有零值公式。
2019-02-11 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
Simple example of weak modal logic based on intuitionistic core
在本文中，我们提出了一个简单的命题逻辑的例子，它有一个模态算子，是基于直觉的核心。这个系统在模态意义上是非常弱的-例如规则性或单调性不成立。它具有完备的语义，由具有邻域和预序关系的可能世界构成。我们讨论了对这些结构施加的某些限制。此外，我们提出的特征公理4已知的逻辑S4。
2018-06-25 cs.LO math.LO
Logical Boltzmann Machines
University of Tasmania（塔斯马尼亚大学）；City, University of London（伦敦大学城市学院）
在连接主义系统中表示符号知识的想法是一个长期的努力，最近引起了很多关注，其目标是将机器学习和可扩展的声音推理相结合。早期的研究表明，命题逻辑和对称神经网络之间存在对应关系，但对称神经网络不能很好地随变量的数量而扩展，而且其训练机制效率低下。在本文中，我们介绍了逻辑玻尔兹曼机（LBM），神经符号系统，可以表示任何命题逻辑公式的严格析取范式。我们证明了LBM的能量最小化和逻辑可满足性之间的等价性，从而表明LBM是能够合理推理的。我们评估推理经验表明，LBM是能够找到所有令人满意的分配一类逻辑公式的搜索不到0.75%的可能（约10亿）的分配。我们将LBM中的学习与符号归纳逻辑程序设计系统、最先进的神经符号系统和纯粹基于神经网络的系统进行比较，在七个数据集中的五个数据集中实现了更好的学习性能。
2021-12-10 cs.AI cs.LG 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
LAP: Simple Command-line Tools for Teaching Logic, Algorithms, and Proof in Computer Science
University of Delaware（特拉华大学）
LAP工具集用于计算机科学逻辑教学，提供命题和一阶逻辑标准算法实现，支持自然演绎推导语言，可检查推导、反馈错误或多样显示，用Java编写，代码易读，阐明数据定义和算法。
2026-07-10 cs.LO
Skolemization in Simple Type Theory: the Logical and the Theoretical Points of View
本文梳理简单类型论中斯科伦化问题的研究历程，介绍Andrews、Miller及作者团队的相关研究，以该问题的发展为例阐释简单类型论的逻辑视角与理论视角间的张力，无新技术成果。
2023-05-05 cs.LO
Dualized Simple Type Theory
我们提出了一种新的双直觉类型论，称为对偶类型论（DTT）。它是一个简单的类型论，具有完美的直觉对偶性，并对应于单边极化的微积分。我们证明DTT强正规化，并证明类型保持。DTT基于一种新的命题双直觉逻辑，称为对偶直觉逻辑（DIL），它建立在Pinto和Uustalu的逻辑L之上。DIL是L的一种简化，通过删除几个可接受的推理规则，同时保持一致性和完整性。此外，DIL是使用二元语法定义的，通过用极性标记公式和逻辑连接词，从而减少了定义逻辑所需的推理规则的数量。我们给出了相容性的一个直接证明，但证明完全性是通过约简到L。
2016-08-07 cs.LO
Simulating Linear Logic in 1-Only Linear Logic
线性逻辑是由Girard作为经典逻辑的资源敏感的改进而引入的。事实证明，完全命题线性逻辑是不可判定的（Lincoln，Mitchell，Scedrov和Shankar），因此，它比（模态化的）经典或直觉主义逻辑更具表达力。在本文中，我们专注于研究线性逻辑的最简单的片段，如一个文字和常量只有片段（后者不包含文字在所有）。在这里，我们证明了线性逻辑的所有这些极其简单的片段（单文字，$\bot$ -only，甚至单位-only）与相应的完整版本具有完全相同的表达能力。我们还提出了一个完整的计算解释（在无循环程序与堆栈）的无底直觉线性逻辑。基于这种解释，我们证明了我们的编码的公平性，并建立上述复杂性的结果。
2017-09-09 cs.LO
Logical Reasoning for Higher-Order Functions with Local State
我们介绍了一个扩展的霍尔逻辑调用值高阶函数ML样的本地引用生成。局部引用可以动态生成并导出到其作用域之外，可以存储高阶函数，并且可以用于构造复杂的可变数据结构。这个原语是使用断言引用名称可达性的谓词从可能的高阶数据和隐藏引用上的量词逻辑地捕获的。我们探索的逻辑的描述和推理能力与非平凡的编程例子相结合的高阶程序和动态生成的本地状态。公理的可达性和局部不变发挥核心作用的推理的例子。
2008-10-20 cs.LO cs.PL
Founded Semantics and Constraint Semantics of Logic Rules
Stony Brook University（石溪大学）
逻辑规则和推理是计算机科学的基础，并已得到广泛的研究。然而，逻辑语言的先验语义可能有微妙的含义，甚至在非常简单的程序上也可能存在显著的不一致，包括试图解决着名的罗素悖论。当在递归中使用无限制否定时，这些语义通常是非直观的，难以理解。本文描述了一个简单的新的语义逻辑规则，成立的语义，其直接扩展到另一个简单的新的语义，约束语义，统一的核心不同的先验语义。新的语义支持无限制否定，以及无限制存在和全称量化。它们通过允许关于谓词、规则和推理的假设被明确地指定为简单而精确的二元选择而具有独特的表达性和直观性。它们是完全声明性的，并且与先前的语义干净地相关。此外，所建立的语义可以在地面程序的大小中在线性时间内计算。
2020-03-26 cs.AI cs.DB cs.LO
Beyond Traditional Neural Networks: Toward adding Reasoning and Learning Capabilities through Computational Logic Techniques
University of Pisa（比萨大学）；University of L’Aquila（拉奎拉大学）
针对深度学习模型的局限性，本文提出通过计算逻辑技术改进符号知识注入，并将机器学习与逻辑集成到多智能体系统中，以增强推理与学习能力。
2023-08-30 cs.AI cs.LG cs.LO
Hybrid Type-Logical Grammars, First-Order Linear Logic and the Descriptive Inadequacy of Lambda Grammars
在这篇文章中，我们表明，混合类型逻辑文法是一个片段的一阶线性逻辑。这个嵌入结果有几个重要的后果：它不仅为演算提供了一个简单的新的证明理论，从而澄清了混合类型逻辑文法的证明理论基础，但是，由于翻译是简单和直接的，它也为混合类型逻辑文法提供了几个新的解析策略。其次，混合类型逻辑文法的NP完全性紧随其后。主要的嵌入结果也揭示了新的光与lambda语法/抽象范畴语法的问题，并显示lambda语法/抽象范畴语法遭受的问题的过度生成和问题的语法语义接口不同于任何其他范畴语法。
2014-05-26 cs.CL cs.LO
