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
Modulo quantifiers over functional vocabularies extending addition
本文证明满足位置范式的扩展加法的纯函数词汇表上的FO和FOMOD逻辑具有CBP，并指出证明FOMOD[<,+,2^x]无法定义所有正则语言等价于分离电路复杂性类ACC0和NC1。
2025-02-01 cs.LO
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
Harnessing Higher-Order (Meta-)Logic to Represent and Reason with Complex Ethical Theories
计算机机械化的一个雄心勃勃的明确的道德理论，Geetheth的通用一致性原则，是用来展示一种方法，表现出复杂的逻辑功能，如道德和道义模态，索引，高阶量化等的道德理论的代表和推理。利用教会的类型论作为一个元逻辑的高表达能力，语义嵌入量化的非经典逻辑的组合，我们的工作推动现有的边界在知识表示和推理。我们证明了复杂的伦理理论的直观编码和它们在计算机上的自动化不再是对立面。
2019-06-15 cs.LO
Reasoning in Non-normal Modal Description Logics
非正规模态逻辑，解释的邻域模型，概括了通常的关系语义，已发现应用在几个领域，如认识论，道义，和联盟推理。在这里，我们提出了初步的结果推理的模态描述逻辑的一个家庭，通过结合ALC与非正规模态算子。首先，我们提供了一个框架的终止，正确的，和完整的Tableau算法来检查满足性的公式在这样的逻辑与语义的基础上变化的域。然后，我们调查的可满足性问题，这些语言的片段，通过限制应用程序的模态算子的公式，并解释模型与常数域，提供紧密的复杂性结果。
2022-06-30 cs.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
Continuous Modal Logical Neural Networks: Modal Reasoning via Stochastic Accessibility
Lawrence Berkeley National Laboratory（伯克利劳伦斯国家实验室）
本文提出连续模态逻辑神经网络，通过随机可及性实现模态推理，结合逻辑公式指导神经网络生成符合逻辑属性的解决方案。
2026-03-04 cs.LG cs.LO
Dyadic obligations: proofs and countermodels via hypersequents
本文为二元道义逻辑系统 E 提出具有切割消除和子公式性质的超矢列演算，并据此给出判定程序、反模型构造及 Co-NP 复杂度上界。
2024-06-13 cs.LO
Monadic second order finite satisfiability and unbounded tree-width
Seese（1991）的经典结果证明了一元二阶逻辑的有限可满足性问题只能在有界树宽的结构类上判定。本文证明了以下问题是可判定的：输入：（i）一元二阶逻辑语句$α$，（ii）一个语句$β$，该语句在一阶逻辑的两变量片段中扩展为计数量词. $α$和$β$的词汇表可以相交。输出量：是否存在满足$α\landβ$的有限结构，使得该结构对$α$的词汇表的限制具有有界树宽？(The所需结构的树宽度不受限制）。因此，我们证明了可满足性问题的可判定性的有限结构的有界树宽度的逻辑扩展一元二阶逻辑的线性基数约束的形式$|X_{1}|+\cdots+|X_{r}|<|Y_{1}|+\cdots+|Y_{s}|$，其中$X_{i}$和$Y_{j}$是一元二阶变量。我们证明了WS1S的一个类似的扩展的可判定性。
2016-04-16 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
Logic-Parametric Neuro-Symbolic NLI: Controlling Logical Formalisms for Verifiable LLM Reasoning
University of Luxemburg（卢森堡大学）；University of Sheffield（谢菲尔德大学）
本文提出逻辑参数化框架，通过可控逻辑形式提升神经符号推理的鲁棒性与适应性，实验表明内部逻辑策略在不同领域具有更优表现。
2026-01-09 cs.AI cs.CL cs.LO
Defeasible Conditional Obligation in a Two-tiered Preference-based Semantics (Extended Version)
Technische Universität Wien (TU Wien)（维也纳技术大学）
本文提出一种双层偏好语义框架，通过结合非单调推理机制和双序关系（理想性与正常性），解决可废止条件义务的逻辑建模问题，并与约束输入/输出逻辑建立联系。
2026-06-28 cs.AI cs.LO
Relating description complexity to entropy
我们展示了熵和描述复杂性之间的一些新的联系，这是一个指指定给定属性的最小公式长度的概念。设MLU是用泛模态扩充命题逻辑得到的逻辑，GMLU是相应的具有计数能力的扩充。在有限的情况下，MLU对于指定变量赋值的集合是表达完备的，而GMLU对于多集合是表达完备的。我们表明，对于MLU，具有最大玻尔兹曼熵的模型类是具有最大描述复杂度的模型类。关于GMLU，我们表明，预期玻尔兹曼熵是渐近等价于预期的描述复杂性乘以所考虑的命题符号的数量。为了对比这些结果，我们表明，这种联系打破时，我们移动到考虑一阶逻辑FO的词汇表具有较高的arity关系。为了建立上述结果，我们证明了几乎所有的有限模型都需要相对较大的FO公式来定义它们。我们的研究结果涉及柯尔莫哥洛夫复杂性和熵之间的联系，展示了一种方法来构思这样的结果在逻辑为基础的方案，关系结构的不同大小的公式进行分类。
2022-09-26 cs.LO math.LO
Complexity and Expressivity of Uniform One-Dimensional Fragment with Equality
均匀一维片段UF 1 ^=是从一阶逻辑中获得的一种形式，通过将量化限制在存在（全称）量词块的应用中，使得在量化公式中最多有一个变量保持自由。片段在布尔运算下是闭合的，但附加的限制（称为一致性条件）适用于具有两个或多个变量的原子公式的组合。这个片段可以被看作是二元逻辑的规范化推广，定义它是为了能够处理任意的关系。最近引入了分片的概念，并证明了UF 1 ^=的无等式分片的可满足性问题是可判定的.本文证明了UF 1 ^=的可满足性和有限可满足性问题是NEXPTIME-完全的。我们还证明了具有计数量词的扩展UF ^=的相应问题是不可判定的。除了可判定性问题，我们还比较了UF ^=和二元逻辑与计数量词FOC^2的表达性。我们表明，虽然逻辑一般来说是不可比较的，但当注意力仅限于元数界为二的词汇时，UF 1 ^=严格包含在FOC^2中。
2014-09-02 cs.LO math.LO
Normative Conditional Reasoning as a Fragment of HOL
本文通过Isabelle/HOL浅层语义嵌入机械化Aqvist条件义务系统E，既用于自动验证道义对应关系，也用于编码Parfit令人反感的结论，提出弱化传递性而非完全放弃的替代方案。
2024-07-07 cs.AI cs.LO cs.SC
