Automating Defeasible Reasoning in Law
Singapore Management University（新加坡管理大学）
本文研究基于规则的系统中的可废止推理，特别是关于法律规范和合同。我们确定规则修饰符，指定规则如何交互以及如何覆盖它们。然后，我们定义规则转换，消除这些修饰符，最终导致规则到公式的转换。对于推理和规则，我们对比了两种方法，一种是在经典逻辑与SMT求解器作为证明引擎，一种是在非单调逻辑与答案集编程求解器。
2022-05-15 cs.AI cs.LO
Extending and Automating Basic Probability Theory with Propositional Computability Logic
DongA University（东亚大学）
经典概率论是用集合来表述的。本文用命题可计算性逻辑扩展了经典概率论。与其他形式主义不同，可计算性逻辑建立在事件/博弈的概念上，这是概率论的核心。因此，基于CoL的概率理论是有用的{ \it自动化}不确定性推理。我们描述了这个新的概率论的一些基本性质。我们还讨论了一种新的集合运算和可计算性逻辑运算之间的同构。
2020-06-22 cs.AI math.LO math.PR
Automating Public Announcement Logic with Relativized Common Knowledge as a Fragment of HOL in LogiKEy
University of Bamberg（班贝格大学）；FU Berlin（柏林自由大学）
提出了相对化公共知识的公告逻辑的一种浅语义嵌入。这种嵌入使这个逻辑的第一次自动化与现成的定理证明经典高阶逻辑。它演示了（i）元理论研究如何可以自动化的方式，以及（ii）如何在目标逻辑（公告逻辑）的非平凡的推理，例如，需要获得一个令人信服的编码和自动化的智者之谜，可以实现。所提出的语义嵌入的关键是，评价域被明确建模，并被视为一个额外的参数，在编码的组成部分的嵌入式目标逻辑;在以前的相关工作，例如正常模态逻辑的嵌入，评价域之间的元逻辑和目标逻辑隐式共享。本文中介绍的工作构成了对多元LogiKEy知识工程方法的重要补充，该方法可以同时进行逻辑及其组合，一般和领域知识以及具体用例的实验。
2022-01-27 cs.AI cs.LO math.LO
Solving Quantified Modal Logic Problems by Translation to Classical Logics
本文评估了自动定理证明系统在QMLTP库中的表现，通过将问题翻译为类型一阶和高阶逻辑并使用一阶或高阶逻辑ATP系统求解，发现嵌入方法在使用先进系统时可靠，且在反驳猜想时优于原生模态逻辑系统。
2024-04-29 cs.AI cs.LO
Description Logics Go Second-Order -- Extending EL with Universally Quantified Concepts
University of Ulm（乌尔姆大学）
本文提出描述逻辑EL的全称量化概念扩展，定义模式与二阶两种语义，证明有用片段中两种语义结论一致，并给出多项式可判定性，可表达角色链公理等。
2023-08-29 cs.AI cs.LO
On Quantified Modal Theorem Proving for Modeling Ethics
Rensselaer Polytechnic Institute（伦斯勒理工学院）
在过去的十年中，形式逻辑已被用来模拟广泛的伦理理论和原则，目标是在自治系统中使用这些模型。用于建模伦理理论的逻辑及其自动推理机的要求与用于其他目的的模态逻辑不同，例如用于时间推理。为了满足这些要求，需要研究新的自动化检验方法。特别是，一个量化的模态逻辑，道义认知事件演算（DCEC），已被用来模拟各种版本的学说的双重效果，akrasia和美德伦理。使用一个片段的DCEC，我们概述了这些不同的特点，并提出了一个草图的算法，可以帮助某些方面证明自动化DCEC。
2019-12-30 cs.AI cs.LO
Automating Agential Reasoning: Proof-Calculi and Syntactic Decidability for STIT Logics
Technische Universität Wien（维也纳技术大学）
这项工作提供了证明搜索算法和自动反模型提取一类STIT逻辑。有了这个，我们回答了一个公开的问题，关于STIT逻辑的句法决策程序和无切演算。对至多n个选择的多智能体STIT问题，引入了一类新的无割完全标号演算G3LdmL^m_n.我们通过使用传播规则来精化演算G3LdmL^m_n，并证明其结构规则的可接受性，从而得到辅助演算Ldm^m_nL。在单代理的情况下，我们表明，精炼演算Ldm^m_nL推导定理在一个有限的类（森林状）序列，使我们能够提供证明搜索算法，决定单代理STIT逻辑。我们证明了证明搜索算法的正确性和终止性。
2020-02-15 cs.AI cs.LO cs.MA
Quantified Markov Logic Networks
Cardiff University（卡迪夫大学）；University of Bremen（不来梅大学）；KU Leuven（鲁汶大学）
马尔可夫逻辑网络（MLN）非常适合于表达诸如“吸烟者以高概率认识另一吸烟者”的统计数据，但不适合于表达诸如“存在认识大多数其他吸烟者的吸烟者”的陈述，这对于建模（例如，社交网络中的影响者）是必要的。为了克服这一缺点，我们研究量化的MLNs，通过引入统计全称量词来概括MLNs，允许以原则性的方式表达后一种类型的统计数据。我们的主要技术贡献是表明，在量化的MLN，最大后验概率和边际推理的标准推理任务，可以减少到各自的MLN对应的多项式时间。
2018-08-21 cs.AI cs.LG cs.LO
Counterfactual Conditionals in Quantified Modal Logic
Rensselaer Polytechnic Institute（伦斯勒理工学院）
我们提出了一种新的形式化的反事实条件在一个量化的模态逻辑。反事实条件句在伦理和道德推理中起着至关重要的作用。先前的研究表明，道德推理系统（更一般地说，心理理论推理系统）至少应该像一阶（量化）模态逻辑（QML）一样具有良好的表现力。虽然现有的道德推理工作集中在反事实的QML道德推理，我们提出了一个完全指定和实现的正式系统，包括反事实条件。我们用两个项目来验证我们的模型。在第一个项目中，我们证明了我们的系统可以用来模拟一个复杂的道德原则，双重效果的学说。在第二个项目中，我们使用该系统来构建一个包含我们理论许可的真实和虚假反事实的数据集，我们相信这对其他研究人员来说可能很有用。该项目还表明，我们的模型在计算上是可行的。
2017-11-02 cs.AI
Automating Reasoning with Standpoint Logic via Nested Sequents
TU Dresden（德累斯顿工业大学）
立场逻辑是最近提出的形式主义的背景下，知识的整合，它提倡一个多视角的方法，允许推理的选择不同的，可能相互冲突的立场，而不是强迫他们的统一。在本文中，我们介绍了嵌套的立场逻辑-证明系统，操纵树的节点是多套公式-并展示了如何自动化的立场推理的非确定性证明搜索算法。为了获得最坏情况下的复杂性最优的证明搜索，我们介绍了一种新的技术，在嵌套序列的上下文中，被称为“着色”，其中包括一个公式作为输入，猜测一定的着色其子公式，然后运行证明搜索在嵌套的递归演算上的彩色输入。我们的技术可以让我们决定的有效性，在CoNP的立场公式，因为证明搜索只产生一个部分的证明相对于每个允许的着色的输入。我们展示了如何将所有部分证明融合在一起，以构建一个完整的证明时，输入是有效的，以及如何某些部分证明可以转化为一个反模型时，输入是无效的。这些“证明”（即证明和反模型）作为输入有效性的解释。
2022-05-05 cs.AI cs.DS cs.LO
Interactions between Knowledge and Time in a First-Order Logic for Multi-Agent Systems: Completeness Results
Imperial College London（伦敦帝国理工学院）
研究了一类用于多智能体系统推理的一阶时间认知逻辑。我们编码系统的典型属性，包括完美的回忆，同步性，无学习，并具有独特的初始状态的变量的量化解释系统，解释系统的一阶扩展。我们确定了几个单音节片段的一阶时间认知逻辑，并显示其完整性相对于其相应的类的量化解释系统。
2014-01-23 cs.AI cs.LO cs.MA
Strength Factors: An Uncertainty System for a Quantified Modal Logic
Rensselaer Polytechnic Institute（伦斯勒理工学院）
我们提出了一个新的系统S，用于处理量化模态逻辑（一阶模态逻辑）中的不确定性。该系统是基于概率论和证明理论。这一体系源于奇泽姆的认识论。我们具体化奇泽姆的系统接地他的未定义的和原始的（即基础）的概念，在概率和证明理论的reasonablene。S在必须与人类交互的系统中很有用，并为它们的不确定性提供理由。作为系统的一个演示，我们应用该系统提供了一个解决彩票悖论。该系统的另一个优点是，它可以用来提供反事实陈述的不确定性值。反事实是一个代理人知道肯定是假的陈述。在其他情况下，反事实在系统必须向用户解释其行为时很有用。对反事实的无知自然地从我们的系统中消失。在简单的一阶逻辑中进行有效的推理是一个难题。基于分辨率的一阶推理系统在过去几十年中在构建解决非平凡任务（甚至是数学中未解决的问题）的系统方面取得了重大进展。我们提出了一种新的推理算法，扩展一阶分辨率的草图。最后，虽然有许多命题逻辑、一阶逻辑和命题模态逻辑的不确定性系统，但在构建一阶模态逻辑的不确定性系统方面的工作很少。下文所述的工作正在进行中;完成后将解决这一缺陷。
2018-05-28 cs.AI
Planning with Incomplete Information in Quantified Answer Set Programming
New Mexico State University（新墨西哥州立大学）；Omaha State University（奥马哈州立大学）；University of Potsdam（波茨坦大学）
我们提出了一个通用的方法来规划与不完全信息的答案集编程（ASP）。更确切地说，我们考虑的问题，符合和条件规划与感知行动和假设。我们表示规划问题，使用一个简单的形式主义，其中逻辑程序描述的状态，初始状态和目标状态之间的过渡函数。为了解决规划问题，我们使用量化答案集编程（QASP），ASP的扩展与原子上的存在和通用量词类似于量化布尔公式（QBF）。我们定义了量化的逻辑程序的语言，并用它来表示符合和条件规划的不同变体的解决方案。在实践方面，我们提出了一个基于约束的QASP求解器，量化的逻辑程序转换成QBF，然后执行QBF求解器，我们实验评估的方法一致性和条件规划基准。正在考虑接受TPLP。
2021-08-13 cs.AI
Simple Type Theory as Framework for Combining Logics
Articulate Software
简单类型论适合作为结合经典和非经典逻辑的框架。这种说法是基于这样的观察：各种突出的逻辑，包括（量化的）多模态逻辑和直觉主义逻辑，可以优雅地嵌入简单的类型论中。此外，简单类型论对于嵌入逻辑的组合建模具有足够的表达力，并且具有很好的语义理解。现成的简单类型论的推理系统存在，可以统一地用于推理内和关于逻辑的组合。
2010-04-30 cs.AI cs.LO
A first-order Temporal Logic for Actions
Université de la Méditerranée（地中海大学）
我们提出了一个多模态动作逻辑与一阶模态，其中包含的条款，可以统一与后续公式中的条款，可以量化。这使得同时处理时间和状态成为可能。我们讨论这种语言的应用，行动理论，它是可能的，以表达许多时间方面的行动，例如，开始，结束，时间点，延迟的先决条件和结果，持续时间和许多其他。我们提出了一个可判定的片段，这个逻辑的表格规则。
2007-05-14 cs.AI cs.LO
Bundled fragments of first-order modal logic: (un)decidability
Institute of Mathematical Sciences, Homi Bhabha National Institute（数学科学研究所，霍米·巴巴国家研究所）；Peking University（北京大学）
量化模态逻辑为模态态度的推理提供了一种自然的逻辑语言，即使在保留量化的丰富性的同时，也可以引用域上的谓词。但是，在许多模型类上，逻辑的大多数片段都是不可判定的。多年来，只有少数片段（例如单声部）被证明是可判定的。在本文中，我们研究的片段，捆绑量词和模态在一起，知识/为什么/什么的认知逻辑的早期工作的启发。与量化模态逻辑一样，域是否在世界上保持相同会产生重大差异。特别是，我们表明，束$\forall \Box$是不可判定的恒定域的解释，即使只有一元谓词，而$\exists \Box$束是可判定的。另一方面，在增加域解释，我们得到的可判定性与$\forall \Box$和$\exists \Box$束与不受限制的谓词。在这些情况下，我们还获得了在\PSPACE中运行的基于tableau的过程。我们进一步表明，$\exists \Box$束不能区分恒定域和增加域的解释。
2018-03-28 cs.AI cs.LO math.LO
Systematic Verification of the Modal Logic Cube in Isabelle/HOL
Freie Universität Berlin（柏林自由大学）；Cambridge University（剑桥大学）
我们提出了一个著名的模态逻辑立方体在Isabelle/HOL的自动验证，在其中我们证明了立方体的逻辑之间的包含关系，使用自动推理工具。先前的工作解决了这个问题，但不限于模态逻辑立方体，并使用一阶逻辑中的编码与一阶自动定理证明器相结合。相比之下，我们的解决方案更优雅，透明和有效。它采用了嵌入的量化模态逻辑在经典的高阶逻辑。自动推理工具，如大锤与LEO-II，Satallax和CVC 4，Metis和Nitpick，实现完全自动化。虽然成功，实验也激励一些技术改进的Isabelle/HOL工具。
2015-07-31 cs.AI cs.LO
On Quantifying Literals in Boolean Logic and Its Applications to Explainable AI
Computer Science Department, UCLA（加州大学洛杉矶分校计算机科学系）；Institut Universitaire de France（法国大学研究院）
量化布尔逻辑是在布尔逻辑中增加运算符以存在性地和普遍地量化变量的结果。这扩展了布尔逻辑的范围，使几十年来已经探索的各种应用成为可能。文字（变量状态）的存在量化及其应用也在文献中进行了研究。在本文中，我们通过研究泛字面量化及其应用，特别是可解释的AI来补充这一点。我们还提供了一个新的量化语义，讨论变量/文字和存在/泛量化之间的相互作用。我们进一步确定了一些类的布尔公式和电路上的量化可以有效地进行。文字量化比变量量化更细粒度，因为后者可以根据前者定义。这导致了一个细化量化布尔逻辑与文字量化作为其原语。
2021-10-12 cs.AI cs.DB cs.LG
Harnessing the Power of LLMs: Automating Unit Test Generation for High-Performance Computing
University Of Houston（休斯顿大学）；Kent State University（肯特州立大学）
针对高性能并行科学软件单元测试成本高、现有工具效果差的问题，本文利用 Davinci 与 ChatGPT 为 C++ 并行程序自动生成单元测试，验证了 LLM 的有效性及局限。
2024-07-06 cs.AI cs.SE
Extensional Higher-Order Paramodulation in Leo-III
University of Luxembourg（卢森堡大学）
Leo-III是一个自动化的定理证明器，用于扩展类型论，具有Henkin语义和选择。通过将基于调节的证明搜索适应于高阶逻辑来启用具有原始等式的推理。证明器可以与多个外部专家推理系统（诸如一阶证明器和SMT求解器）协作。Leo-III与TPTP/TSTP框架兼容，用于输入格式，报告结果和证明，以及推理系统之间的标准化通信，例如，从证明助手（如Isabelle/HOL）内部进行证明重建。Leo-III支持多态一阶和高阶逻辑，所有正常的量化模态逻辑以及不同的道义逻辑中的推理。它的发展开始了TPTP基础设施的不断扩展，以在非经典逻辑中进行推理。
2021-02-28 cs.AI cs.LO cs.SC
Advancing Natural Language Formalization to First Order Logic with Fine-tuned LLMs
Osnabrück University（奥斯纳布鲁克大学）；University of Zurich（苏黎世大学）
本文通过微调LLMs提升自然语言到一阶逻辑的转换性能，实验显示谓词可用性显著提升模型表现，T5模型优于大解码器-only模型，并能泛化至未见逻辑论证。
2025-11-30 cs.AI cs.CL
