发表机构
University of Southern Denmark; University of Amsterdam（南丹麦大学; 阿姆斯特丹大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文在Lean中构建库级模态逻辑形式化，通过垂直与水平复用提供通用框架，派生多种逻辑并减少67%代码，应用于数学、编程语言和并发推理。
AI 中文摘要
模态逻辑包含一族广泛的逻辑，用于对关系结构进行推理。文献中呈现了许多这样的逻辑，展示了多样的算子、语义和应用。这种多样性反映在机械化模态逻辑的动物园中，这些逻辑常常重复语法、语义、元理论和推理基础设施。我们在Lean中提出了一个库级（library-grade）的模态逻辑形式化，作为CSLib（Lean计算机科学库）的一部分开发，并围绕两种互补的复用形式设计：垂直复用，即专门逻辑从公共抽象中继承；水平复用，即模态逻辑成为独立形式化领域的推理工具。我们的开发为多元模态语言提供了一个通用框架，可复用的元理论和证明自动化，以及为专门模态逻辑派生的接口。我们通过派生基本模态逻辑、基本时态逻辑和Hennessy-Milner逻辑来示例我们的基础设施；后者包含并扩展了CSLib之前的实现，同时将其逻辑特定代码减少了67%。我们进一步将相同的模态基础设施应用于数学推理（理想的根）、编程语言理论（简单类型λ演算的类型安全策略）以及并发理论（通信系统演算中关于进程的推理）。我们的经验表明，在形式化共享库的理论时，复用、自动化以及与强大Lean生态系统的集成应被视为一等设计关注点。
英文摘要
Modal logic comprises a broad family of logics to reason about relational structures. The literature presents many such logics, displaying diverse operators, semantics, and applications. This plurality is reflected in a zoo of mechanised modal logics, which often duplicate syntax, semantics, metatheory, and reasoning infrastructure. We present a library-grade formalisation of modal logic in Lean, developed as part of CSLib (the Lean Computer Science Library) and designed around two complementary forms of reuse: vertical reuse, whereby specialised logics inherit from common abstractions, and horizontal reuse, whereby modal logic becomes a reasoning tool for independently formalised domains. Our development provides a generic framework for polyadic modal languages, reusable metatheory and proof automation, and derived interfaces for specialised modal logics. We exemplify our infrastructure by deriving basic modal logic, basic temporal logic, and Hennessy-Milner Logic; the latter subsumes and extends CSLib's previous implementation while reducing its logic-specific code by 67%. We further apply the same modal infrastructure to reasoning about mathematics (radicals of ideals), theory of programming languages (the type safety strategy for the simply typed $λ$-calculus), and concurrency theory (reasoning about processes in the Calculus of Communicating Systems). Our experience suggests that reuse, automation, and integration with the strong Lean ecosystem should be treated as first-class design concerns when formalising theories for shared libraries.
