Extending Concurrent Separation Logic to Enhance Modular Formalization
如今，许多基于大规模分布式系统的服务已经被开发出来，以提高人类生活的便利性。另一方面，由于这些系统的复杂性和嵌套性，确保其正确性和性能成为一个重大的挑战。虽然并发分离逻辑（CSL）通过指定系统并验证它们的正确性部分地解决了这个问题，但它面临着模块化问题。在本文中，我们提出了一个扩展的并发分离逻辑（ECSL），以解决CSL的模块化问题的时间扩展，通信扩展，环境扩展，嵌套扩展的支持。ECSL能够在从存储管理到体系结构和协议设计的不同抽象层次上对系统进行形式化，具有很强的模块性。在开发ECSL的过程中，坚持统一性和兼容性原则。
2020-07-27 cs.LO
Formalization of Transform Methods in Higher-order Logic: A Survey
大多数工程和物理系统通常分别由基于其连续时间和离散时间动力学的微分方程和差分方程来表征。此外，这些动态模型进行了分析，使用变换的方法来证明这些系统的各种性质，如，传递函数，频率响应和稳定性，并找出解决方案的微分/差分方程。用于执行基于变换方法的分析的常规技术已经不能提供这些系统的精确分析。因此，高阶逻辑定理证明，一种形式化的方法，已经被用于精确地分析基于变换方法的系统。在本文中，我们调查的发展转换方法为基础的分析，在各种高阶逻辑定理证明和概述相应的现实世界的案例研究，从航空电子，医学和运输领域，已分析了这些发展的基础上。
2021-11-19 cs.LO
Isabelle's Metalogic: Formalization and Proof Checker
Isabelle是一个通用的定理证明器，使用高阶逻辑的一个片段作为定义对象逻辑的元逻辑。伊莎贝尔还提供了证明条件。我们正式这个元逻辑和语言的证明条款在Isabelle/HOL，定义一个可执行的（但效率低下）证明条款检查器，并证明其正确性w.r.t.元逻辑我们将证明检查器与Isabelle集成，并在一系列逻辑和理论上运行它，以检查这些理论中所有证明的正确性。
2021-04-25 cs.LO
Isabelle/HOL as a Meta-Language for Teaching Logic
证明助手是逻辑教学的重要工具。我们支持这一主张，讨论三个形式化的Isabelle/HOL在最近的课程中使用的自动推理。第一个是系统W（一个只有两个原始符号的经典命题逻辑系统）的形式化，第二个是自然演绎助手（NaDeA），第三个是使用我们的序列演算验证器（SeCaV）的单边递归演算。我们依次描述每个形式化，集中在我们如何在教学中使用它们，并从逻辑教育的角度评论有趣或有用的功能。最后，我们反思了所吸取的经验教训，以及这些经验教训下一步可能引导我们走向何方。
2020-10-30 cs.LO
The Distributed Ontology Language (DOL): Ontology Integration and Interoperability Applied to Mathematical Formalization
分布式本体语言（DOL）目前正在ISO/TC 37/SC 3的OntoIOp（本体集成和互操作性）活动中进行标准化。它旨在为（1）异构逻辑形式化的本体，（2）模块化本体，（3）本体之间的链接，以及（4）本体的注释提供一个统一的框架。本文重点介绍了DOL的元理论功能在数学形式化中的应用：在COLORE（公共逻辑库）中验证数学概念的本体形式化之间的关系，这为形式化现实世界的概念，如空间和时间关系提供了基础。
2012-04-23 cs.LO
Formalization of Bond Graph using Higher-order-logic Theorem Proving
键合图是描述复杂工程和物理系统动力学的统一图形方法，广泛应用于电气、机械、医学、热力学和流体力学等领域。传统上，这些动态分析使用纸和笔的证明方法和基于计算机的技术。然而，这两种技术都有其固有的局限性，如人为错误倾向，结果的近似和巨大的计算需求。因此，这些技术不能被信任用于执行基于键合图的动态分析系统的安全关键领域，如机器人和医学。形式化方法，特别是高阶逻辑定理证明，可以克服这些传统方法的缺点，并提供这些系统的准确分析。它已被广泛应用于工程和物理系统的动力学分析。在本文中，我们提出使用高阶逻辑定理证明进行键合图的物理系统的分析。特别是，我们提供了键合图的形式化，其中主要包括功能，允许键合图转换到其相应的数学模型（状态空间模型）和验证其各种属性，如，稳定性。为了说明我们所提出的方法的实际有效性，我们提出了正式的稳定性分析的假肢机电一体化的手使用HOL光定理证明。此外，为了帮助HOL中的非专家，我们在MATLAB中编码我们正式验证的稳定性定理，以执行拟人假肢机电一体化手的稳定性分析。
2021-11-24 cs.LO
Integrating DFT and DRBD Formalizations in HOL4
动态故障树（DFT）和动态可靠性框图（DRBD）是描述工程系统动态失效行为的两种建模方法。最近，两个独立的高阶逻辑（HOL）形式化的DFT和DRBD代数已经在HOL4定理证明器。在这项工作中，我们建议整合这两种建模方法的有效形式的复杂系统的可靠性分析，利用每种方法的优点。通过DFT和DRBD代数之间的等价性的正式证明提供了这种集成的可靠性。作为一个案例研究，我们显示了建议的综合正式的可靠性分析的效率的线控系统。
2019-10-20 cs.LO
Formal Probabilistic Analysis of Dynamic Fault Trees in HOL4
动态故障树（DFT）是一种广泛使用的故障建模技术，可以以非常有效的方式捕获系统的动态故障特征。模拟和模型检验传统上用于DFT的概率分析。仿真通常基于采样，因此不能保证其结果是完整的，而模型检验使用计算机算术和数值算法来计算概率的精确值，其中包含许多舍入误差。利用高阶逻辑（HOL）定理证明的表达和声音的性质，我们提出了，在这项工作中，DFT门和它们的概率行为，以及它们的一些简化性质的形式化HOL。这种形式化将允许我们通过验证关于其在HOL中的行为的通用数学表达式来进行DFT的概率分析。特别是，我们形式化的AND，OR，优先级AND，功能DEPPER，热SPARE，冷SPARE和暖SPARE门，并验证其相应的概率表达式在HOL。此外，我们正式验证了一个重要的属性，Pr（X<Y），使用Lebesgue积分，因为这种关系允许我们推理优先级-“与”门和Before运算符的概率属性。我们还正式的概念，条件密度，以正式验证的概率表达式的冷SPare和暖SPare门。为了说明我们的形式化的有用性，我们用它来正式分析心脏辅助系统的DFT。
2018-07-24 cs.LO
Formalization of Transform Methods using HOL Light
变换方法，如拉普拉斯和傅立叶，经常用于分析工程和物理系统的动态行为，基于其传递函数和频率响应或其相应微分方程的解。在本文中，我们提出了一个正在进行的项目，重点是高阶逻辑形式化的转换方法使用HOL光定理证明。特别是，我们提出了形式化的动机，其次是相关的工作。接下来，我们介绍迄今为止完成的任务，同时强调在正式化过程中面临的一些挑战。最后，我们提出了一个路线图，以实现我们的目标，目前的状态和未来的目标，这个项目。
2017-05-29 cs.LO
Formalization of Metatheory of the Quipper Quantum Programming Language in a Linear Logic
我们开发了一个线性逻辑框架内的混合系统，并使用它来推理的类型系统的量子λ演算。特别是，我们认为一个实用的版本的演算称为原Quipper，其中包含的核心Quipper。Quipper是一种正在积极开发的新量子程序设计语言，最近在量子计算社区中获得了很大的普及。Hybrid是一个系统，旨在支持使用高阶抽象语法（HOAS）来表示和推理Coq证明助手中实现的正式系统。在这项工作中，我们扩展了系统的线性规格说明逻辑（SL），以理由Quipper的线性型系统。为此，我们形式化的原型Quipper的语义编码的SL中的类型和评价规则，并证明类型的可靠性。
2018-12-10 cs.LO cs.PL
Natural Deduction Assistant (NaDeA)
我们提出了自然演绎助手（NaDeA），并讨论了它的优点和缺点作为一种工具，用于教学逻辑。NaDeA可在线获得，基于Isabelle证明助手中的自然演绎的形式化。我们首先提供简洁的配方的主要形式化结果。然后，我们详细说明的先决条件NaDeA，特别是我们描述了一个形式化的伊莎贝尔的“希尔伯特公理”，我们使用作为一个起点，在我们的本科课程数理逻辑。我们讨论了最近的评估NaDeA，并给出了一个概述在NaDeA的练习。
2019-04-01 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
Teaching a Formalized Logical Calculus
经典一阶逻辑在许多方面都是数学、语言学、计算机科学和人工智能的核心，因此有必要详细定义它。我们提出了合理性和完整性证明的一阶逻辑，形式化的互动证明助手伊莎贝尔/HOL的一个微积分。我们的形式化是基于Stefan Berghmann的工作，我们已经更新为使用Isabelle的声明式证明风格Isar（正式证明档案，条目FOL-Fitting，2007年8月/2018年7月）。我们用de Bruijn指数表示变量;这使得在量词下的替换对人类读者来说不那么直观。然而，与使用字符串表示的变量的替换实现相比，自然数的性质产生了一个优雅的解决方案。所考虑的微积分具有一个总是空的前件和一个在后件中的公式列表的特殊性质。我们得到的可靠性和完整性的证明，作为其tableau对应的逆对偶的派生结果的微积分。我们努力不仅提出的结果的合理性和完整性的证明，但也提供了一个深入到一个类似编程的方法，一阶逻辑语法，语义和微积分的形式化。我们在一门计算机科学专业的逻辑本科课程中使用了这种形式化，并讨论了我们的经验。
2020-02-28 cs.LO
Theory-Scale Auto-Formalization of Logics for Computer Science
提出LCS-Bench基准，通过半自动化流水线构建包含327个教材条目、4076个Lean声明的理论级自动形式化数据集，评估14个模型，发现最先进模型仅达20.1%准确率。
2026-06-26 cs.LG cs.LO cs.PL
The Kleene-Rosser Paradox, The Liar's Paradox & A Fuzzy Logic Programming Paradox Imply SAT is (NOT) NP-complete
在针对$λ$ -演算[94]的Kleene-Rosser悖论检查{ \bf P}与{ \bf NP}问题之后，发现它代表NP-完全性的反例。我们证明它与库克定理的证明相矛盾。说谎者悖论的逻辑形式化导致了同样的结果。这种将说谎者悖论形式化为可计算形式的形式是在[90]的系统中发现的模糊逻辑编程悖论的2值实例。给出了证明{ \bf SAT}是（非）NP完全的三个证明. NP完全性的反例类也是Fagin定理[36]和Immermann-Vardi定理[89，110]的反例，它们是描述复杂性的基本结果。所有这些结果表明{ \bf ZF $\not$ C}是不一致的。
2009-07-10 cs.LO
A Monadic Formalization of ML5
ML 5是一种用于空间分布式计算的程序设计语言，基于与模态逻辑S5的Curry-Howard对应关系。尽管是通过与S5模态逻辑的对应关系来设计的，但ML 5程序设计语言在几个方面与该逻辑不同。在本文中，我们解释ML 5和S5之间的这些差异，通过将ML 5翻译成稍微不同的逻辑：直觉S5扩展了一个松散的模态，将有效的计算封装在一个单子中。这种翻译既解释了现有的ML 5设计，又提出了一些简化和概括。我们已经在Agda证明助手中正式确定了我们的翻译。我们没有将lax S5形式化为一个证明理论，而是将它作为依赖类型宿主语言中的一个论域（universe）来进行\emph{embed}，并通过实现模态逻辑的Kripke语义来消除论域。这种表示技术节省了我们为逻辑定义证明理论并证明其正确的工作，并且还允许我们继承元语言的等式理论，该理论可以用于证明语义验证ML 5的操作语义。
2010-09-14 cs.LO cs.PL
Teaching the Formalization of Mathematical Theories and Algorithms via the Automatic Checking of Finite Models
在逻辑和证明的实际应用中的教育，如计算机程序的形式规范和验证，受到了这样一个事实的严重阻碍，即投入在证明上的大多数时间和精力实际上是徒劳的：由于学生开发的规范和算法中的错误，他们的证明努力往往毫无意义（因为被证明的命题实际上是不感兴趣的）或先验注定要失败的（因为要证明的命题实际上并不成立），这是一个常见的挫折来源，并给形式方法带来了坏名声。RISCAL（RISC算法语言）是一种形式化的规约语言和相关的软件系统，它试图通过使逻辑形式化变得有趣而不是负担来克服这个问题。为此，RISCAL允许学生通过自动评估/执行和检查（小）有限模型来轻松验证命题实例的正确性。因此，许多/大多数错误可以被快速检测到，随后的证明尝试可以集中在更有意义和真实的命题上。
2018-03-05 cs.LO
Cubical Type Theoretic Navya-Nyāya
本文用立方体类型论形式化了印度晚期古典哲学中的海军-尼亚耶学派逻辑语言，解决了传统逻辑无法处理的依赖限定、类型缺失、非扩展性身份和无界关系深度等问题。
2026-05-10 cs.LO
Deontic Temporal Logic for Formal Verification of AI Ethics
International Institute of Information Technology - Bangalore（国际信息技术研究所-班加罗尔）
本文提出基于规范逻辑的AI伦理形式化方法，用于验证AI系统在公平性和可解释性方面的伦理行为，通过自动定理证明器验证实际系统是否满足伦理要求。
2026-03-27 cs.AI cs.LO
Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation
本文基于证明助手Isabelle/HOL，利用自由逻辑的浅层语义嵌入对范畴论进行元逻辑研究，形式化了初等拓扑斯与对称幺半闭范畴，并构建了易于使用的Isabelle范畴论库，为未来形式化研究奠定基础。
2023-06-16 cs.LO math.CT math.LO
Intuitionistic Propositional Logic in Lean
该研究在Lean证明助手中形式化直觉主义命题逻辑，验证其两份完备性证明，探究Kripke与代数两种语义范式的关系，还证明了大量定理及演绎规则。
2024-10-31 cs.LO
Formalization of Fragments of the Theory of Hereditarily Finite Sets
Institute of Computer Science of the Czech Academy of Sciences（捷克科学院计算机科学研究所）；Faculty of Mathematics and Physics, Charles University, Prague（布拉格查理大学数学与物理学院）
该研究在Isabelle/HOL中形式化遗传有穷集理论片段，采用locale层级结构对应不同公理片段，用一阶可定义谓词的归纳定义处理公理模式，分析等价的有穷性与正则性公理，并通过模型形式化公理独立性结论。
2026-09-28 cs.LO
nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models
CISPA Helmholtz Center for Information Security（CISPA亥姆霍兹信息安全中心）；Stanford University（斯坦福大学）
在执行任何验证任务时，所需系统需求的严格形式化是必不可少的。这通常限制了验证技术的应用，因为编写正式规范是一项容易出错且耗时的手动任务。为了促进这一点，我们提出了nl2spec，应用大语言模型（LLM）从非结构化自然语言中获得正式规范（在时序逻辑）的框架。特别是，我们引入了一种新的方法来检测和解决固有的模糊性的系统要求在自然语言：我们利用LLM映射子公式的形式化回相应的自然语言片段的输入。用户迭代地添加、删除和编辑这些子翻译以修改错误的形式化，这比手动重新起草整个形式化更容易。该框架对特定的应用领域是不可知的，并且可以扩展到类似的规约语言和新的神经模型。我们进行用户研究以获得具有挑战性的数据集，我们使用该数据集对翻译质量进行实验。我们提供了一个开源的实现，包括一个基于Web的前端。
2023-03-08 cs.AI cs.LG cs.LO
Teaching Intuitionistic and Classical Propositional Logic Using Isabelle
我们描述了一个自然演绎形式化的直觉和经典命题逻辑的伊莎贝尔/纯框架。与早期的工作相比，我们探索了使用深度嵌入方法进行逻辑建模的教学优势，在这里我们采用了逻辑框架建模。这产生了简单而自然的教学例子，我们报告了它在2020年和2021年教授我们的自动推理课程中所发挥的作用。
2022-02-08 cs.LO
The decision problem of modal product logics with a diagonal, and faulty counter machines
在二变量一阶逻辑的命题模态（和代数）处理中，等式由“对角”常数建模，在通用框架的平方积中解释为恒等（也称为“对角”）关系。在这里，我们研究的决定问题的产品的两个任意模态逻辑配备这样的对角线。由于二元一阶逻辑中等式的存在或不存在并不影响其可满足性问题的复杂性，因此人们可能会认为，在一般的乘积逻辑中添加对角线也是无害的。我们证明，情况远非如此，复杂性可能会有相当大的跳跃，甚至从可判定到高度不可判定。我们的不可判定逻辑也可以被看作是一阶逻辑的新片段，其中添加等式将可判定片段改变为不可判定。我们证明了我们的结果的一个新的应用计数器机的问题。虽然我们的形式主义显然不能直接强制可靠的计数器机器计算，但模型中唯一对角线的存在使得有可能对相同指令序列的有损和插入错误计算进行编码。我们表明，给定这样一对错误的计算，就有可能根据它们重建可靠的运行。
2015-09-07 cs.LO
Embedding Differential Dynamic Logic in PVS
本文提出将微分动态逻辑（dL）嵌入原型验证系统（PVS）中，形式化了混合程序语义与证明演算，构建了Plaidypvs以支持在PVS内部验证混合程序并推理整类程序。
2024-04-23 cs.LO
A simplified framework for first-order languages and its formalization in Mizar
本文给出了经典一阶逻辑的严格形式化的集合论处理。由于这是一个具体的Mizar形式化的基本结果（Lindenbaum引理; Henkin，可满足性，完备性和Lowenheim-Skolem定理）的目标，它变成了一个系统的追求简化：我们放弃了自由发生的概念，派生树，并研究严格需要什么推理规则来证明上述结果。之后，我们讨论实际的Mizar实现的细节，并给出其中开发的一般技术。
2012-05-19 cs.LO math.LO
Formal Analysis of Continuous-time Systems using Fourier Transform
为了研究工程和物理系统的动力学行为，我们经常需要捕捉它们的连续行为，这是使用微分方程建模，并执行这些系统的频域分析。传统上，使用基于纸笔的分析技术或计算机模拟，使用傅立叶变换方法来执行该频域分析。然而，这两种方法都容易出错，因此不适用于分析安全关键领域（如医学和运输）中使用的系统。为了提供一个准确的替代方案，我们建议使用高阶逻辑定理证明进行频域分析这些系统。为此，本文提出了一个高阶逻辑形式化的傅立叶变换使用HOL-Light定理证明。特别地，我们使用基于高阶逻辑的多变量微积分的微分、积分、超越和拓扑理论的形式化来形式化地定义傅立叶变换，并推理其经典性质的正确性，例如存在性、线性、时移、频移、调制、时间标度、时间反转和时域微分，以及其与傅立叶余弦的关系，傅立叶正弦和拉普拉斯变换。我们使用我们提出的形式化的形式化验证的频率响应的一般n阶线性系统，音频均衡器和MEMS加速度计，使用霍尔光定理证明。
2017-07-31 cs.LO
Formal Design of Asynchronous Fault Detection and Identification Components using Temporal Epistemic Logic
自主关键系统，如卫星和空间漫游者，必须能够检测故障的发生，以确保正确的操作。此任务由故障检测和识别（FDI）组件执行，这些组件嵌入在这些系统中，并负责通过从传感器读取数据并触发预定义的警报来自动及时地检测故障。设计有效的外国直接投资成分是一个极其困难的问题，也是由于缺乏完整的理论基础，以及精确的规范和验证技术。在本文中，我们提出了第一个正式的方法来设计的FDI组件的离散事件系统，无论是在同步和异步设置。我们提出了一个逻辑语言的规范的外国直接投资的要求，占了广泛的实际案例，并包括新的方面，如最大化和跟踪诊断。该语言配备了一个明确的语义的时间认知逻辑的基础上，并被证明享有适当的属性。我们将讨论如何验证需求，以及如何验证给定的FDI组件是否满足这些需求。我们提出了一种算法，正确的建设FDI组件的合成，并报告的适用性的设计方法的工业案例研究来自航空航天。
2016-02-10 cs.LO
PFL: a Probabilistic Logic for Fault Trees
针对故障树结构化查询分析研究不足的问题，本文提出概率故障树逻辑PFL及领域特定语言LangPFL，扩展布尔故障树推理逻辑BFL，支持含概率的故障树属性规范，并基于BDD给出相关理论与模型检测算法，通过COVID-19相关及油气管道故障树验证了有效性。
2025-08-04 cs.LO
Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic
我们提出了一个共归纳的框架，定义和推理的无穷类似物的方程逻辑和长期重写在一个统一的，共归纳的方式。该设置捕获任意序数长度的重写序列，但它既不需要序数也不需要度量收敛。这使得该框架特别适合于定理证明器中的形式化。
2018-01-09 cs.LO
Existentially Quantified Systems of Equations as an Implicit Representation of Answers in Logic Programming
在本文中，我们提出了另一种方法来形式化的逻辑编程理论。在这种形式化中，我们允许在查询中存在量化变量和方程。与标准方法相反，答案的作用将由存在量化的方程组发挥。这使得我们在处理替换时可以避免问题。特别地，当输入子句引入新变量时，我们不需要“全局”变量分隔条件。此外，这种形式化可以被视为并发逻辑语言理论的基础，因为它还包括广泛的并行计算方法。此外，答案的平行组合可以直接定义为答案的一致连接。
2022-07-19 cs.LO cs.PL
Formalized Lambek Calculus in Higher Order Logic (HOL4)
在这个项目中，一个相当完整的证明理论形式化的Lambek演算（非关联的任意扩展）已经从Coq证明辅助移植到HOL4定理证明器，并进行了一些改进和新的定理。定义了Lambek演算的三个演绎系统（句法演算、自然演绎和序列演算），并证明了许多相关定理。形式上证明了这些系统之间的等价性。最后，在HOL4中设计并实现了序列微积分证明的形式化（其中Coq具有内置支持）。一些基本结果，包括所谓的“割自由”证明的子公式的性质进行了形式证明。这项工作可以被认为是对语言解析器的基础上的类别语法，这是不是多模态的，但仍然有能力支持上下文敏感的语言，通过自定义的扩展的初步工作。
2017-05-20 cs.CL cs.LO
First Order Logic with Fuzzy Semantics for Describing and Recognizing Nerves in Medical Images
Sorbonne Université（索邦大学）；SCAI；Institut Polytechnique de Paris（巴黎高等理工学院）；Institut Imagine（Imagine研究所）；Ligue contre le Cancer（癌症防治联盟）；Télécom Paris（巴黎电信学院）；LTCI；Université Paris Cité（巴黎城市大学）；Hôpital Necker Enfants-Malades, APHP（Necker儿童医院，法国国家卫生研究院）
本文提出结合模糊语义与一阶逻辑对解剖知识进行形式化，定义空间实体、关系和量词的语言，并基于此提出空间推理算法，用于从磁共振图像中分割和识别神经以辅助外科手术规划。
2025-04-30 cs.AI cs.LO math.LO
NaDeA: A Natural Deduction Assistant with a Formalization in Isabelle
我们提出了一个新的软件工具，用于教学逻辑的基础上自然演绎。它的证明系统在证明助手Isabelle中得到了形式化的描述，使得它的定义非常精确。形式化的合理性已在Isabelle中得到证明。该工具是用TypeScript / JavaScript开发的开源软件，因此可以直接在浏览器中使用，无需进一步安装。虽然开发的本科计算机科学的学生谁是用来学习和编程具体的计算机代码在程序设计语言，我们认为相关的方法为更广泛的受众和其他证明系统。
2015-07-14 cs.CY cs.LO
A formalization of convex polyhedra based on the simplex method
在证明助手Coq中给出了凸多面体的形式化。我们的工作的基石是一个完整的实施单纯形法，连同证明其正确性和终止。这允许我们以有效的方式定义多面体上的基本谓词（即，作为程序），并将它们与相应的通常的逻辑对应物相关联。为此，我们广泛使用布尔反射方法。这种方法的好处是，我们可以很容易地推导出多面体上的几个基本结果的证明，如Farkas引理，线性规划的对偶定理和Minkowski定理。
2018-08-10 cs.LO math.CO math.OC
Monoid Theory in Alonzo: A Little Theories Formalization in Simple Type Theory
McMaster University（麦克马斯特大学）
本文以幺半群理论为例，展示了如何利用小理论方法在Alonzo逻辑系统中形式化数学知识，采用不完全形式化证明的替代方法以侧重于交流性和可访问性。
2025-10-31 cs.LO math.LO
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
Dynamic Logic of Legal Competences
Sun Yat-sen University（中山大学）；Universität Bayreuth（拜罗伊特大学）
我们提出了一个新的形式化的法律能力，特别是Hohfeldian类别的权力和豁免权，通过道义上的动态认知逻辑的重新解释。我们认为，这一逻辑明确地抓住了法律能力的规范变化的特点，同时提供了一个复杂的减少后者静态规范的立场。该逻辑是完全可公理化的，我们将其应用于德国合同法中的一个具体案例，以说明它可以捕捉法律能力和法律允许性之间的区别。
2021-10-09 cs.AI cs.LO
Formalizing a Many-Sorted Hybrid Polyadic Modal Logic in Lean
Faculty of Mathematics and Computer Science, University of Bucharest（布加勒斯特大学数学与计算机科学系）
本文在Lean中形式化了一个多类签名和多模态算子的混合模态逻辑，提供DSL用于定义语言和协议，并证明了其可靠性定理，展示了在代码验证、BAN逻辑和S5系统中的应用。
2026-06-26 cs.LO cs.PL
An Expressive Probabilistic Temporal Logic
本文认为，概率，时间和行动的综合治疗是必不可少的概率的概念的适当的逻辑帐户，并根据这种直觉，描述了一个表达概率的时间逻辑推理的行动与不确定的结果。该逻辑是模态的和高阶的：由动作注释的模态用于表达由动作产生的下一状态中的命题的可能性和必要性，并且需要高阶函数来表达概率算子。所提出的逻辑被证明是经典数学概率论的一个适当的扩展，并通过Monty Hall问题的形式化来说明其表达能力。
2017-10-08 cs.AI cs.LO
Inference rules for RDF(S) and OWL in N3Logic
University of Bialystok（比亚韦斯托克大学）
本文介绍了资源描述框架（RDF）、RDF模式（RDFS）和Web本体语言（OWL）的推理规则。我们的形式化是基于符号3逻辑，它扩展了RDF的逻辑符号，并创建演绎RDF图存储的语义Web逻辑。我们还提出了OWL-P，这是一个轻量级的OWL形式主义，并支持软推理，省略复杂的语言结构。
2016-01-11 cs.AI cs.DB cs.LO
Models of fault-tolerant distributed computation via dynamic epistemic logic
分布式计算模型的可计算能力由进程可用的通信介质、进程和通信的时序假设以及进程可能遭受的故障的性质决定。在一个配套文件中，我们展示了如何动态认知逻辑可以用来给一个正式的语义给定的分布式计算模型，精确地捕获所需的知识来解决分布式任务，如共识。此外，通过移动到由单纯复形定义的认知逻辑的对偶模型，拓扑不变量被暴露，这决定了任务的可解性。在本文中，我们将展示如何扩展上述设置，以包括在知识的过程中，知识的计算模型本身。该扩展描述了知识流程获得有关当前执行，在过程中没有输入值的问题。
2017-04-25 cs.DC cs.LO cs.MA
