Redundancy in Logic III: Non-Mononotonic Reasoning
Paolo Liberatore
给出了限制理论和缺省理论的冗余性结果。特别是，建立一个给定的理论是否是冗余的复杂性。
Results about the redundancy of circumscriptive and default theories are presented. In particular, the complexity of establishing whether a given theory is redundant is establihsed.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
Redundancy in Logic II: 2CNF and Horn Propositional Formulae
我们报告的复杂性结果的冗余公式的2CNF形式。我们首先考虑的问题，检查冗余，并显示一些算法，略优于平凡的。然后，我们分析了相关的问题，找到非冗余等价子集（I.E.S.）一个给定的集合。循环性的概念被证明与这些问题的复杂性有关。给出了Horn公式的一些结果。
Generalizing Redundancy in Propositional Logic: Foundations and Hitting Sets Duality
从合取范式（CNF）中的命题公式中检测和消除冗余子句是包括人工智能在内的许多应用领域的基本问题，并且已经成为广泛研究的主题。此外，一些最近的应用程序激发了这个问题的各种扩展。例如，不可满足的公式划分为不相交的子句子集（所谓的组），通常需要通过删除冗余组来简化，或者可能包含冗余变量，而不是子句。在这份报告中，我们提出了一个广义的理论框架标记CNF公式，统一的冗余检测和删除问题的各种扩展，并允许推导出一些结果，substanion和扩展以前的工作。后续报告包含了一些额外的理论结果和算法的各种计算问题的背景下，提出的框架。
On Natural Deduction for Herbrand Constructive Logics III: The Strange Case of the Intuitionistic Logic of Constant Domains
常域逻辑是直觉主义逻辑，它用所谓的全移位公理（forall-shift axiom）进行了扩展，这是一个经典有效的命题，蕴涵了可判定公式上的排中律。令人惊讶的是，这种逻辑是建设性的，到目前为止，这已经证明了削减消除特设的结石。在这里，我们使用自然演绎和Curry-Howard对应的方法来提供一个简单的计算解释的逻辑。
Extensional Higher-Order Paramodulation in Leo-III
Leo-III是一个自动化的定理证明器，用于扩展类型论，具有Henkin语义和选择。通过将基于调节的证明搜索适应于高阶逻辑来启用具有原始等式的推理。证明器可以与多个外部专家推理系统（诸如一阶证明器和SMT求解器）协作。Leo-III与TPTP/TSTP框架兼容，用于输入格式，报告结果和证明，以及推理系统之间的标准化通信，例如，从证明助手（如Isabelle/HOL）内部进行证明重建。Leo-III支持多态一阶和高阶逻辑，所有正常的量化模态逻辑以及不同的道义逻辑中的推理。它的发展开始了TPTP基础设施的不断扩展，以在非经典逻辑中进行推理。
The Higher-Order Prover Leo-III (Extended Version)
给出了一个基于Henkin语义和选择的经典高阶逻辑自动定理证明器Leo-III。Leo-III是基于扩展的高阶调节，并接受每一个常见的TPTP方言（FOF，TFF，THF），包括他们最近的扩展秩1多态性（TF 1，TH 1）。此外，证明器本身支持几乎所有正常的高阶模态逻辑。Leo-III与一阶推理工具合作，使用多种一阶逻辑的翻译，并产生可验证的证明证书。证明器在异构基准集上进行评估。
SCL(EQ): SCL for First-Order Logic with Equality
我们提出了一个新的演算SCL（EQ）的一阶逻辑与平等，只学习非冗余条款。遵循CDCL（Conflict Driven Clause Learning）和SCL（Clause Learning from Simple Models）的思想，使用基本文字模型假设指导推理，保证推理的非冗余性。Reddit是相对于从地面文字模型假设导出的动态变化的排序来定义的。我们证明SCL（EQ）的声音和完整的，并提供了例子，我们的演算改进叠加。
A System of Interaction and Structure III: The Complexity of BV and Pomset Logic
本文证明 Pomset logic 与 BV 这两种逻辑并不相同的猜想是错误的，并揭示了两者在可证明性复杂度上的巨大差距：BV 是 NP 完全的，而 Pomset logic 是 $Σ_2^p$-完全的。
Formal Verification of Proofs from Automated Theorem Provers for Higher-Order Logic
本文提出一种在Dedukti框架中验证高阶逻辑自动定理证明器证明的通用方法论，应用于EP演算并集成至Leo-III，实现约80%证明步骤自动重构，成为首个支持独立可检查证明重构的高阶证明器。
Outlier detection in default logics: the tractability/intractability frontier
在默认理论中，离群值表示具有意外属性的文字集。在以前的论文中，我们定义了缺省逻辑中的离群点，并研究了它们的形式性质。具体来说，我们已经研究了异常值检测问题的计算复杂性，并证明，虽然它们通常是棘手的，有趣的易处理的情况下，可以挑选出来。根据这些结果，我们在这里研究离群点检测问题的易处理性边界，通过分析它（i）考虑离群点检测问题，（ii）参考默认逻辑片段，（iii）采用离群点的概念。对于第（i）点，我们将考虑三个日益复杂的问题，分别称为离群点-证人识别，离群点识别和离群点存在。至于第（ii）点，当我们寻找可以有效地进行离群点检测的条件时，注意力将限于无析取命题缺省理论的子集。至于第（iii）点，我们将参考[ABP 08]的离群值概念和一个新的更具限制性的概念，称为强离群值。在复杂性结果的基础上，我们提出了一个多项式时间算法来计算拟无循环正态一元缺省理论中所有有界强离群点。我们的一些易处理性的结果依赖于增量引理，提供了条件的一个contrult逻辑片段具有单调的行为。最后，为了表明我们处理的DL的简单片段仍然足够丰富，以解决有趣的问题，因此，我们证明的易处理性结果不仅在理论方面是有趣的，这些片段的表达能力的见解，通过显示正常的一元理论表达所有NL查询，从而间接回答了考茨和塞尔曼提出的问题。
A Syllogistic Probe: Tracing the Evolution of Logic Reasoning in Large Language Models
本研究通过三段论测试揭示大型语言模型在逻辑推理演变中的特性，发现模型规模、思考机制和基础模型对逻辑发展有重要影响。
The DL-Lite Family and Relations
最近推出的一系列描述逻辑下的共同绰号DL-Lite引起了关注的描述逻辑和语义Web社区，由于低计算复杂性的推理，一方面，和能力，以表示概念建模形式主义，另一方面。本文的主要目的是沿着五个轴对原始DL-Lite逻辑的扩展中的推理进行全面而系统的研究：通过（i）将布尔连接词和（ii）数量限制添加到概念构造，（iii）允许角色层级，（iv）允许角色不相交性、对称性、不对称性、自反性、非自反性和传递性约束，以及（v）采用或放弃唯一的相同假设。我们分析了所得到的逻辑的可满足性的组合复杂度，以及实例检查和回答肯定存在查询的数据复杂度。我们的方法是基于嵌入DL-Lite逻辑在合适的片段的一个变量的一阶逻辑，这提供了有用的见解，他们的属性，特别是计算行为。
Generative Logic: A Deterministic Reasoning Engine
生成逻辑（GL）是一种确定性架构，通过用户提供的公理定义生成可配置的演绎邻域，通过逻辑块和统一的哈希推理引擎实现证明生成与知识生成，实验验证其在数论中的应用及CAS系统潜力。
The Ditmarsch Tale of Wonders - The Dynamics of Lying
我们提出了一个动态的说谎逻辑，其中一个“说谎，φ”（其中φ是一个公式的逻辑）是一个动作的意义上的动态模态逻辑，这是解释为一个状态Transformer相对于公式φ。被转换的状态是指向的Kripke模型，编码了代理人对他们信念的不确定性。谎言可以是关于事实命题的，也可以是关于模态公式的，比如其他代理人的信念或其他代理人谎言的信念后果。我们区分（i）一个外部观察者对系统中建模的代理人撒谎，（ii）一个代理人对另一个代理人撒谎，并且两者都在系统中建模。对于这两种情况，我们进一步区分了（iii）相信它被告知的一切（即使以不一致为代价）的代理人，（iv）只相信它被告知的与其当前信念一致的代理人，以及（v）通过不断修改其当前信念来相信它被告知的一切的代理人。逻辑有完整的公理化，这可以通过它们嵌入到所谓的动作模型逻辑或该逻辑的扩展到信念修正中来最优雅地显示。
Bivalent semantics, generalized compositionality and analytic classic-like tableaux for finite-valued logics
本文是一个贡献的理论基础和有效的自动化证明程序的非经典逻辑的实际建设。我们在这里集中在有限值逻辑的情况下，并展示：（i）一种机制，用于产生一个类似经典的描述，他们在一个有效的各种二价语义;（ii）用于从如此获得的二价语义中提取均匀（classically-labeled）cut-免费的标准分析表格与可能的分支可逆规则，并与证明策略配对，旨在保证终止的相关的证明程序;（iii）一种机制，也提供了相同的逻辑，统一的削减为基础的表系统与线性规则。后者的表系统被证明是足够的，即使限制到分析削减，他们也被证明多项式模拟真值表，一个功能，是不享有的前标准类型的表系统（甚至在2值的情况下）。结果是基于有用的概括的概念的分析性和组合性，并说明了一个理论，适用于许多其他类别的非经典逻辑。
Continuous Modal Logical Neural Networks: Modal Reasoning via Stochastic Accessibility
本文提出连续模态逻辑神经网络，通过随机可及性实现模态推理，结合逻辑公式指导神经网络生成符合逻辑属性的解决方案。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。