Stable Normative Explanations: From Argumentation to Deontic Logic
ALMA AI（ALMA人工智能研究院）；University of Bologna（博洛尼亚大学）；EUI（欧洲大学学院）
本文将可废止逻辑中的稳定解释概念引入形式论证框架，探讨其道义含义，并基于论证邻域结构构建可刻画该概念的道义逻辑，同时给出复杂性结果。
2023-07-11 cs.AI cs.LO
Modeling Deontic Modal Logic in ASP
The University of Texas at Dallas（德克萨斯大学达拉斯分校）；CETINIA, Universidad Rey Juan Carlos（CETINIA，雷耶·胡安·卡洛斯大学）
本文利用回答集编程中的默认否定和强否定直接表达道义模态算子，并通过全局约束表示义务、禁止和许可，解决了道义模态逻辑的经典悖论，并支持条件义务和条件禁止的知识表示。
2026-07-23 cs.AI cs.LO
Faithful Semantical Embedding of a Dyadic Deontic Logic in HOL
University of Luxembourg（卢森堡大学）；Freie Universität Berlin（柏林自由大学）
给出了Carmo和Jones提出的并元道义逻辑在经典高阶逻辑中的一个浅语义嵌入。这种嵌入被证明是健全和完整的，也就是说，忠实。这里提出的工作提供了理论基础，并在现成的高阶定理证明和证明助手的二元道义逻辑的实施和自动化。
2018-03-05 cs.AI cs.LO math.LO
Sound Conflict Analysis for Timed Contract Automata
针对连续时间下道义规范分析技术的缺失，提出一种可靠但不完备的算法用于检测时间契约自动机中的冲突，证明了其正确性并通过案例研究进行了验证。
2024-10-16 cs.LO
Avoiding Pragmatic Oddity: A Bottom-up Defeasible Deontic Logic
本文提出了一种扩展的可废止道义逻辑来处理语用奇性问题。该逻辑应用三个一般原则：（1）语用奇性问题必须在CTD推理的一般逻辑处理中解决;（2）必须采用非单调方法来处理CTD推理;（3）CTD推理的逻辑模型必须在计算上可行，并且如果可能的话，是有效的。可废止道义逻辑的拟议扩展阐述了Governatori和Rotolo（2019）提出的模型的初步版本。以前的解决方案是基于逻辑的（构造性的，自上而下的）证明理论的特定特征。然而，这种方法引入了一定程度的非确定性。为了避免这个问题，我们提供了一个自自底向上的【形】的逻辑特征。新的表征提供了见解的逻辑的有效实施，并允许我们建立的计算复杂性的问题。
2022-09-09 cs.AI cs.LO
Deontic Meta-Rules
Griffith University（格里菲斯大学）；Singapore Management University（新加坡管理大学）；University of Verona（维罗纳大学）；University of Bologna（博洛尼亚大学）
在逻辑中使用元规则，即，规则，其内容包括其他规则，最近在非单调推理的设置中获得了关注：Olivieri等人（2021）提出了第一个逻辑形式化和有效算法来计算这些理论的（Meta）扩展。由此产生的逻辑将不仅能够为政策建模，而且还能够处理许多法律制度中出现的众所周知的问题。在我们刚刚提到的应用领域中，使用可废止逻辑（DL）对元规则进行建模已经进行了研究。在这条研究路线中，上面提到的研究并没有关注元规则的一般计算属性。这项研究填补了这一空白，有两个主要贡献。首先，我们引入并形式化了两个变体的可废止道义逻辑与元规则来表示（1）可废止元理论与道义模态，（2）两种不同类型的规则之间的冲突：简单冲突可废止道义逻辑，谨慎冲突可废止道义逻辑。其次，我们提出了有效的算法来计算这两种变体的扩展。
2022-09-23 cs.AI cs.LO
Explicit non-normal modal logic
针对道义模态的超内涵性问题，本文提出作为非正规模态逻辑超内涵对应物的新型证成逻辑，证明其可靠性与完全性，并研究实现问题。
2023-08-11 cs.LO
A temporal logic of epistemic and normative justifications, with an application to the Protagoras paradox
本研究结合带过去与未来模态的线性时态逻辑与道义辩护逻辑，构建含两类辩护断言的推理框架，给出两种语义并证明公理系统的可靠性与完备性，还形式化分析了普罗泰戈拉悖论。
2021-09-21 cs.LO
A Neutral Temporal Deontic STIT Logic
在这项工作中，我们回答了一个长期存在的要求，通过引入多代理STIT逻辑TDS的道义STIT逻辑的时间嵌入。该逻辑是基于非时间功利STIT逻辑。然而，这里提出的逻辑将是中性的：而不是致力于功利主义理论，我们证明了逻辑TDS的声音和完整的关系框架，不采用任何功利功能。我们演示了如何将这些中性框架转化为实用的时间框架，同时保持有效性。最后，我们讨论了在时间设置中采用二元效用函数所产生的问题。
2019-11-18 cs.LO math.LO
A logic for default deontic reasoning
本文提出了一种基于默认逻辑的非模态证明论框架，用于解决规范冲突和动态规范问题。
2025-12-21 cs.LO math.LO
A Simple Doxastic Deontic Logic for Norm-Guided Decision Making
TU Wien（维也纳工业大学）
本文提出一种简单的信念道义逻辑，用于在冲突规范和不完整信息下进行决策，并定义了信念规范合规优化问题，区分主观与客观优化，并给出可归约为加权部分MaxSAT的条件。
2026-10-02 cs.AI cs.LO
Is Free Choice Permission Admissible in Classical Deontic Logic?
Data61, CSIRO（联邦科学与工业研究组织Data61研究所）；University of Bologna（博洛尼亚大学）
在本文中，我们将探讨如何，如果，自由选择许可（FCP）可以被接受，当我们考虑某些类型的许可和义务之间的道义冲突。众所周知，FCP可以在某些最小条件下许可不确定数量的许可的派生。我们讨论了这一点和其他缺点，并提出了六个希尔伯特式的经典道义系统承认一个守卫版本的FCP。就许可而言，我们所呈现的系统从推理的观点来看并不太弱，并且不致力于削弱任何特定的义务逻辑。
2019-06-10 cs.AI cs.LO cs.MA
A Note on Nesting in Dyadic Deontic Logic
University of Liverpool（利物浦大学）
本文报道了关于阿奎斯特的二元逻辑（称为系统G）的一些结果，这是最有影响力的二元义务推理逻辑之一（“应该是这样的情况......如果... ").虽然这种逻辑在文献中已经有一段时间了，但它的许多属性仍然有待深入考虑。在这篇简短的论文中，我们表明：系统G中的任何公式，包括嵌套的模态算子是等价于一些公式没有嵌套; Aqvist在第一次介绍该系统的通用模态是可定义的道义模态。
2017-10-10 cs.AI cs.LO cs.MA
A Deontic Stit Logic Based on Beliefs and Expected Utility
使用逻辑语言对行为和义务进行形式化是人工智能伦理学领域越来越重要的主题。具有表达性的句法和语义框架来推理代理人在道德情境中的决定，允许在将结果的责备（或赞扬）分配给所述代理人时相关的行为成分的明确表示。在这方面，行为的两个非常重要的组成部分是信念和基于信念的行动。在这项工作中，我们提出了一个逻辑的doxastic应该扩展认识论道义stit理论与信念。一方面，涉及信念算子的公式的语义是基于概率测度的。另一方面，doxastic oughts的语义依赖于最优性的概念，而潜在的选择规则是期望效用的最大化。我们引入一个公理系统的结果逻辑，我们解决其可靠性，完整性和可判定性的结果。这些结果在研究中具有重要意义，这些研究旨在使用认知、doxastic和道义逻辑的证明系统，通过定理证明和模型检查来帮助测试人工智能的道德行为。
2021-06-22 cs.LO cs.MA
Impossible and Conflicting Obligations in Justification Logic
该研究针对标准道义逻辑中义务一致性概念等价的问题，在证立逻辑框架下提出多种一致性原则并比较其逻辑强度，构建了使带jd公理的证立逻辑对任意常项规范完全的新语义，还探讨了相关道义悖论的哲学意义。
2023-10-06 cs.LO
Proof Theory and Decision Procedures for Deontic STIT Logics
本文首次为道义多智能体 STIT 逻辑提出无切割完备序列演算及带循环检查的证明搜索判定算法，并展示其在义务检查、合规性检查和联合履行检查等规范推理任务中的自动化应用。
2024-10-04 cs.LO math.LO
A tableau methodology for deontic conditional logics
在本文中，我们提出了一个定理证明方法的限制，但重要的片段的条件语言（布尔组合）条件语句与非嵌套的前件。该方法基于条件逻辑的可能世界语义。KEM标签形式主义，旨在说明正常模态逻辑的语义，很容易适应条件逻辑的语义，通过简单的索引标签与公式。推理规则由命题系统KE+提供-一个类似表格的分析证明系统，设计用于反驳和直接证明方法-扩大了条件连接词的适当消除规则。我们将要提出的定理证明方法可以被看作是为（可废止的）条件义务的几个条件逻辑开发适当的算法框架的第一步。
2000-03-10 cs.AI cs.LO
A Deontic Logic Analysis of Autonomous Systems' Safety
我们考虑了如何建模、验证和确保自主系统满足某些\textit{obligations}（如遵守交通法规的义务），并避免不允许的行为（如鲁莽地改变车道）的紧迫问题。时态逻辑在自治系统设计中被大量使用;然而，正如我们在这里所说明的，时态（alethic）逻辑单独用于自治系统的义务推理是不合适的。本文提出了使用支配行为功利主义（DAU），代理的道义逻辑，编码和自治系统的义务的原因。我们使用DAU来分析英特尔的责任敏感安全（RSS）提案，并将其作为真实案例研究。我们证明了DAU可以表达良构的RSS规则，正式派生这些规则的不良后果，说明如何DAU可以帮助设计系统，有特定的义务，以及如何模型检查DAU义务。
2020-09-01 cs.LO cs.SY eess.SY
Deontic Temporal Logic for Formal Verification of AI Ethics
International Institute of Information Technology - Bangalore（国际信息技术研究所-班加罗尔）
本文提出基于规范逻辑的AI伦理形式化方法，用于验证AI系统在公平性和可解释性方面的伦理行为，通过自动定理证明器验证实际系统是否满足伦理要求。
2026-03-27 cs.AI cs.LO
Swap Kripke models for deontic LFIs
本文首次将交换结构与克里普克模型结合，为基于LFIs的道义逻辑构造非确定性语义，并首次给出$C^{D}_n$层级的完整公理化与语义。
2025-06-06 cs.LO math.LO
Hypersequent calculi for non-normal modal and deontic logics: Countermodels and optimal complexity
我们提出了一些超代数演算的所有系统的经典立方体和它们的公理$T$，$P$，$D$的扩展，并为每个$n\geq 1$，规则$RD^+_n$。演算是内部的，因为它们只使用逻辑语言，加上额外的结构连接词。我们表明，结石是完整的，相对于相应的axiomatisation的句法证明削减消除。然后，我们定义了一个终止根优先证明搜索策略的基础上的超演算，并证明它是最佳的coNP完全逻辑。此外，我们得到，从每一个饱和的叶失败的证明，有可能定义一个反模型的根hyperprandem的双邻域语义，并定期逻辑也在关系语义。最后，我们给出了一个翻译之间的hyperprinciple的应用程序和推导的标记系统的经典立方体。
2020-06-09 cs.LO math.LO
An Algebraic Approach for Action Based Default Reasoning
通常，我们假设一个行为被允许仅仅是因为它没有被明确禁止;或者，类似地，一个行为被禁止仅仅是因为它没有被明确允许。这种假设出现，例如，在自治计算系统中，必须在存在管理特定场景的不完整规范集的情况下做出决策。结合对行为的默认推理和道义推理，我们可以对这些假设进行形式化的推理。考虑到这一点，我们提出了一个合乎逻辑的形式主义的默认推理的道义行动逻辑。我们方法的新颖性是双重的。首先，我们的形式主义默认推理处理行动和行动运营商，它是基于道义的行动逻辑最初提出的Segerberg。其次，受Segerberg方法的启发，我们使用来自布尔代数理论的工具。这些工具使我们能够将Segerberg的代数完备性结果扩展到缺省逻辑的设置。
2019-07-22 cs.LO
Automated Reasoning for Robot Ethics
Universität Koblenz-Landau（科布伦茨-兰道大学）；Harz University of Applied Sciences（哈尔茨应用科学大学）
道义逻辑是数理逻辑和哲学的一个分支。各种道义逻辑被认为是不同的应用领域，如论证理论，法律推理，多智能体系统中的行为。在本文中，我们将展示如何标准道义逻辑可以用来模拟多智能体系统的道德准则。此外，我们展示了如何超，高性能的定理证明，可以用来证明这些道德守则的属性。
2015-02-20 cs.AI cs.LO
Toward Robust Legal Text Formalization into Defeasible Deontic Logic using LLMs
TU Wien（维也纳技术大学）；AIT Austrian Institute of Technology（奥地利技术研究所）；School of Engineering and Technology（工程与技术学院）；Artificial Intelligence and Cyber Futures Institute（人工智能与未来网络研究院）
本文提出利用LLMs将法律文本形式化为可撤销规范逻辑，通过结构化管道和改进的评估方法，提升形式化的一致性和完整性。
2025-12-31 cs.AI cs.CL cs.CY
A Reduction of Input/Output Logics to SAT
uni-greifswald（格赖夫斯瓦尔德大学）
本文提出了一种将输入/输出逻辑归约到SAT问题的自动化方法，并展示了其原型实现。
2026-02-27 cs.AI cs.LO
Modeling Contrary-to-Duty with CP-nets
University of Bologna（博洛尼亚大学）；European University Institute（欧洲大学学院）；IRIT（图卢兹计算机科学研究所）；IBM Research（IBM研究院）
在道义逻辑的其他条件相同语义中，一个更大的规定集得到尊重的事态比一个其中一些规定被违反的事态更可取。条件偏好网（CP-nets）是一种表达和分析条件不变偏好的紧凑形式，具有良好的计算特性。本文展示了如何道义概念可以通过条件偏好模型捕获。定义了一个约束道义逻辑，并将其映射为条件偏好网。我们还将展示如何在CP网中建立与责任义务相反的模型，以及如何在这种形式主义中捕捉强许可和弱许可之间的区别。
2020-03-23 cs.AI cs.LO
An Update Semantics for Defeasible Obligations
Erasmus University Rotterdam（鹿特丹伊拉斯姆斯大学）
道义逻辑DUS是基于Veltman更新语义的规定性义务的道义更新语义。在DUS中，义务的逻辑有效性的定义不是基于静态的真值，而是基于动态的动作转换。本文用更新语义形式化了规定可废止义务，并讨论了可废止道义逻辑的诊断问题。假定一个可撤销的义务“通常A应该（做）”，连同“A没有（做）”这一事实。这是正常性主张的例外，还是违反了义务？在本文中，我们正式的启发式原则，这是一个违反，除非有一个更具体的压倒一切的义务。法律推理的潜在动机是，罪犯应该尽可能少地有机会通过声称他们的行为是例外而不是犯罪来为自己开脱。
2013-01-23 cs.AI cs.LO
On Three-Valued Modal Logics: from a Four-Valued Perspective
本文旨在以生动的直观形象、令人信服的哲学论证和广泛的实际应用，全面解决三值模态逻辑的语义定义这一古老的开放性问题。本文在已有的从创新的角度研究三值逻辑的基础上，采用迂回的方法从四值的角度解释三值逻辑，从而为三值模态逻辑的开发、解释和应用提供了一个通用的、系统的方法论。我们通过两个具体的例子来说明我们的方法，一个是道义的，另一个是认识的，对于这两个声音和强完整的自然演绎证明系统也详细介绍。我们认为，我们的三值模态逻辑作为一个轻量级的候选人合并道义或认知的概念到时态逻辑，没有更重的负担，多模态。
2022-09-27 cs.LO math.LO
Explainability by design: an experimental analysis of the legal coding process
University of Verona（威尼斯大学）；Central Queensland University（中央昆士兰大学）；University of Bologna（博洛尼亚大学）
本文提出一种从文本片段生成道义可废止逻辑规则的法律编码方法，通过人类实验测量编码努力，并利用Houdini技术给出基于领域知识、文本长度和引用深度等因素的编码时间预测方法。
2025-05-03 cs.AI cs.CL cs.LO
Mathematical Proof Assistants for Teaching Logic: The LogiKEy Methodology
Otto-Friedrich-Universität Bamberg（奥托-弗里德里希-班贝格大学）；Freie Universität Berlin（柏林自由大学）；University of Luxembourg（卢森堡大学）
本文介绍基于LogiKEy方法，利用经典高阶逻辑和证明助手Isabelle/HOL教授多元逻辑，通过系列谜题展示从命题到道义逻辑的教学路径，并反驳单一主义质疑，强调其可移植性。
2026-10-07 cs.AI cs.LO
Dyadic obligations: proofs and countermodels via hypersequents
本文为二元道义逻辑系统 E 提出具有切割消除和子公式性质的超矢列演算，并据此给出判定程序、反模型构造及 Co-NP 复杂度上界。
2024-06-13 cs.LO
Refining Labelled Systems for Modal and Constructive Logics with Applications
Australian National University（澳大利亚国立大学）；Laboratoire d’informatique de l’École polytechnique（巴黎综合理工学院计算机实验室）
本文介绍了“结构精化方法”，它作为一种手段转换的模态和/或建设性逻辑的关系语义到一个“经济”的证明系统，通过连接两个证明理论的范式：标记和嵌套演算。标记序列的形式主义已经成功地在拥有理想的证明理论的性质，可以自动生成大型类的逻辑切割免费演算。尽管有这些品质，标记系统使用了复杂的语法，明确地结合了相关逻辑的语义，这样的系统通常违反了子公式属性的高度。相比之下，嵌套微积分使用更简单的语法，并坚持严格阅读子公式属性，使这样的系统在自动推理算法的设计中非常有用。然而，嵌套演算范式的缺点是，关于这种演算的自动构造（如在标记设置中）的一般理论基本上是不存在的，这意味着嵌套系统的构造和它们的属性的确认通常是在个案的基础上完成的。细化方法连接这两种范式在一个富有成效的方式，通过转换成嵌套的（或，精制标记）系统与前保持整个转换过程中的属性标记系统。为了证明精化的方法和它的一些应用，我们考虑文法逻辑，一阶直觉逻辑和道义STIT逻辑。介绍了细化标记演算将被用来提供第一个证明搜索算法的道义STIT逻辑。此外，我们使用我们的精炼标记演算的语法逻辑，以表明在类中的每一个逻辑具有有效的林登插值属性。
2021-07-30 cs.AI cs.DM cs.FL
On Quantified Modal Theorem Proving for Modeling Ethics
Rensselaer Polytechnic Institute（伦斯勒理工学院）
在过去的十年中，形式逻辑已被用来模拟广泛的伦理理论和原则，目标是在自治系统中使用这些模型。用于建模伦理理论的逻辑及其自动推理机的要求与用于其他目的的模态逻辑不同，例如用于时间推理。为了满足这些要求，需要研究新的自动化检验方法。特别是，一个量化的模态逻辑，道义认知事件演算（DCEC），已被用来模拟各种版本的学说的双重效果，akrasia和美德伦理。使用一个片段的DCEC，我们概述了这些不同的特点，并提出了一个草图的算法，可以帮助某些方面证明自动化DCEC。
2019-12-30 cs.AI cs.LO
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
ProofCloud: A Proof Retrieval Engine for Verified Proofs in Higher Order Logic
本文提出证明检索引擎ProofCloud，为高阶逻辑中的已验证证明提供快速搜索与复用服务，并首次给出OpenTheory仓库的完整证明检查结果和基准。
2024-12-30 cs.LO
Surface Proofs for Nonsymmetric Linear Logic (Extended Abstract)
证明了乘性线性逻辑中的一个证明可以表示为一个修饰曲面，使得两个证明仅当它们的曲面在几何上等价时，它们在逻辑上等价。这是arXiv的扩展摘要：1601.05372。
2017-01-18 cs.LO
Automated proof search system for logic of correlated knowledge
本文提出了相关知识逻辑的自动证据检索系统和可判定性。证明系统的核心是具有可靠性、完备性、截集规则和结构规则的可容许性以及所有规则的可逆性等性质的逻辑演算。证明搜索过程的基础上的微积分执行自动终止证明搜索，并允许我们实现相关知识的逻辑决策结果。
2019-02-23 cs.LO
Intuitionistic modal logics: new and simpler decidability proofs for FIK and LIK
本研究整合模态逻辑终止表方法与直觉主义模态逻辑IK的有穷框架性质，为FIK和LIK给出更简洁的全新可判定性证明。
2025-03-24 cs.LO
FMP for QD logics. A wrong proof
本文旨在证明准密集逻辑具有FMP，但证明中存在无法修复的重大错误。
2026-03-16 cs.LO
Focusing and Polarization in Intuitionistic Logic
聚焦证明系统提供了一个范式，以结构化的可逆和不可逆推理规则的应用程序的切割自由证明。Andreoli的线性逻辑的聚焦证明系统已经被应用于证明搜索和证明归一化方法。文献中的各种证明系统都表现出某种程度上的聚焦特性。我们提出了一个新的，集中的证明系统的直觉逻辑，称为LJF，并显示如何其他证明系统可以映射到新的系统，通过插入逻辑连接，过早地停止聚焦。我们还使用LJF设计了一个经典逻辑的集中证明系统。我们的方法来设计和分析这些系统的基础上的完整性集中在线性逻辑和极性的概念，出现在吉拉德的LC和LU证明系统。
2007-08-16 cs.LO
A survey of proof nets and matrices for substructural logics
本文是一个调查的两种“压缩”证明计划，\emph{matrix method}和\emph{proof nets}，适用于各种逻辑沿着子结构层次从经典的所有方式到非关联的Lambek系统。为后者提供了一种新的处理证明网。证明网和矩阵的描述给出了一个统一的符号序列的基础上，使各种逻辑的计划的属性可以很容易地进行比较。
2012-03-22 cs.LO
Complexity of correctness for pomset logic proof nets
我们表明，它是coNP-完全的，以决定是否一个给定的证明结构的pomset逻辑是一个正确的证明网，使用图论在我们以前的文件（arXiv：1901.10247）。
2023-01-23 cs.LO
Syntactic cut-elimination and backward proof-search for tense logic via linear nested sequents (Extended version)
本文给出了基本正规时态逻辑Kt的一个线性嵌套演算。我们表明，演算，使向后证明搜索，反模型建设和句法切割消除。因此，线性嵌套序列提供了为包含逆的模态逻辑提供足够的证明理论所需的最小嵌套量。作为奖励，这产生了对称模态逻辑KB的无切演算。
2019-07-02 cs.LO
A logic of interactive proofs
本文提出概率双主体证成逻辑 IPJ，以支持对执行交互式证明的主体进行推理，并通过可忽略函数参数化分析概率增长，进而给出零知识证明的新概念。
2023-09-26 cs.LO
An introduction to Differential Linear Logic: proof-nets, models and antiderivatives
微分线性逻辑丰富了线性逻辑与额外的逻辑规则的指数连接，对偶的通常规则的遗弃，削弱和收缩。本文提出了微分线性逻辑的证明网语法及其指称模型的范畴公理化。我们还介绍了一个简单的分类条件下，这些模型的一般反导数操作变得可用。最后，我们简要地描述了集合和关系的模型，并给出了有限性空间和线性和连续函数的模型更详细的说明。
2016-06-06 cs.LO
A journey in modal proof theory: From minimal normal modal logic to discrete linear temporal logic
扩展和推广了Masini（1992）的2-序列方法，我们给出了经典模态逻辑在K，D，T，S4谱上的计算方法.系统以统一的方式呈现-通过调整单个参数，即对规则的适用性的约束，获得不同的逻辑。割消法只被证明一次，因为证明过程独立于产生不同系统的约束。给出了离散线性时态逻辑ltl的一个代数演算，并证明了其完备性。本文的主旨是模态和一阶量化之间的形式类比。
2020-01-07 cs.LO
A syntactic proof of decidability for the logic of bunched implication BI
本文通过证明论方法，给出了bunched implication逻辑BI可判定性的语法证明，提供了可实现的决策程序并界定了逻辑复杂性。
2026-01-03 cs.LO
Proof Normalisation in a Logic Identifying Isomorphic Propositions
我们定义了一个片段的命题逻辑同构命题，如$A\land B$和$B\land A$，或$A\Rightarrow (B\land C)$和$(A\Rightarrow B)\land(A\Rightarrow C)$被识别。我们定义了系统I，这个逻辑的证明语言，并证明其规范化和一致性。
2019-04-22 cs.LO
Proof-graphs for Minimal Implicational Logic
众所周知，命题经典证明的规模可能是巨大的。证明理论研究发现正常或切割自由证明和他们各自的非正常证明之间的指数差距。本文的目的是研究如何降低命题推理的权重。我们提出了形式主义的证明图的纯蕴涵逻辑，这是一个特定的形状，旨在捕捉演绎的逻辑结构的图形。这种形式主义的优点是公式可以在简化证明中共享。本文给出了最小蕴涵逻辑证明图的精确定义，并给出了证明图的规范化过程。与标准的树状形式主义相比，我们的规范化并没有增加节点的数量，当应用到相应的最小证明图表示。
2014-04-01 cs.LO
A Proof Tree Builder for Sequent Calculus and Hoare Logic
我们已经开发了一个基于Web的教学证明助手，证明树生成器，它可以让你从最初的目标向上应用规则在微积分和霍尔逻辑的一个简单的命令式语言。我们配备了一个基本的证明自动化功能和Z3集成我们的工具。普林斯顿大学自动推理课程的学生使用了我们的工具，并发现它很直观。证明树生成器可在https://proof-tree-builder.github.io上在线获得。
2023-03-10 cs.LO
Focused Proof-search in the Logic of Bunched Implications
集束蕴涵（BI）逻辑自由地组合了加法和乘法连接词，包括蕴涵;然而，尽管其证明理论得到了充分的研究，但BI中的证明搜索一直是一个难题。聚焦原则是对证明-搜索空间的一种限制，它可以捕获各种目标导向的证明-搜索过程。在本文中，我们表明，集中的证明搜索是完整的BI首先重新制定传统的束的嵌套序列，使用更简单的数据结构，然后与极化和集中的变体，我们显示是健全的和完整的，通过削减消除参数。这建立了一个操作语义集中证明搜索的逻辑集束的影响。
2021-01-26 cs.LO
A Vernacular for Coherent Logic
我们提出了一个简单的，但表现力的证明表示，从不同的证明助手证明可以很容易地生成。该表示法只使用了少量的推理规则，并且基于一阶逻辑的一个片段，称为相干逻辑。融贯逻辑已经被许多研究者认为是一种适用于许多日常数学发展的逻辑。建议的证明表示是伴随着相应的XML格式和一套XSL转换生成正式的证明Isabelle/Isar和Coq，以及证明表示在一个自然语言的形式（在LATEX或HTML格式）。此外，我们的自动定理证明器的连贯逻辑出口证明建议的XML格式。所有的工具都是公开的，还有一组样本定理。
2014-05-14 cs.LO
Infinitary and Cyclic Proof Systems for Transitive Closure Logic
传递闭包逻辑是通过引入传递闭包算子而获得的一阶逻辑的已知扩展。虽然其他具有归纳定义的一阶逻辑的扩展是由一组归纳定义先验参数化的，但传递闭包算子的添加一致地捕获了所有有限归纳定义。在本文中，我们提出了一个无穷证明系统的传递闭包逻辑，这是一个无限下降式对应的现有（显式归纳）证明系统的逻辑。我们表明，作为一阶逻辑与归纳定义的类似系统，我们的无穷系统是完整的标准语义和包含显式系统。此外，传递闭包算子的一致性允许使用简单的语法标准来定义语义上有意义的完整限制。因此，对规则无穷（即循环）证明的限制为自动化归纳推理的有效系统提供了基础。
2018-06-28 cs.LO
Birkhoff style proof systems for hybrid-dynamic quantum logic
本研究基于混合与动态模态逻辑构建量子逻辑框架，提出量子子句概念及对应推理证明规则，验证了其可靠性与紧致性，并证明了该逻辑片段的Birkhoff完备性，为量子逻辑编程与形式规约提供理论支撑。
2024-06-19 cs.LO
