一句话：为匹配逻辑给出可靠完备证明系统，并扩展出匹配 μ-逻辑，统一刻画多种不动点、模态与时序逻辑。
匹配逻辑通过模式与模式匹配来规约和推理结构。此前，可靠且完备的演绎系统仅对提供相等和成员关系的特定理论已知。本文首先在全一般性下为匹配逻辑提出一个可靠且完备的证明系统；其次引入匹配 μ-逻辑，即带最小不动点 μ 绑定子的匹配逻辑扩展。作者证明匹配 μ-逻辑可把许多数学与计算机科学中的重要逻辑作为特例纳入，包括带最小不动点的一阶逻辑、模态 μ-逻辑、动态逻辑、无穷/有限迹线性时序逻辑与计算树逻辑等时序逻辑，尤其是 K 框架所依赖的 reachability logic。该工作为不动点与归纳、编程语言语义及程序规约与验证提供了统一基础。
Matching logic is a logic for specifying and reasoning about structure by means of patterns and pattern matching. This paper makes two contributions. First, it proposes a sound and complete proof system for matching logic in its full generality. Previously, sound and complete deduction for matching logic was known only for particular theories providing equality and membership. Second, it proposes matching μ -Iogic, an extension of matching logic with a least fixpoint μ -binder, It is shown that matching μ -Iogic captures as special instances many important logics in mathematics and computer science, including first-order logic with least fixpoints, modal μ -Iogic as well as dynamic logic and various temporal logics such as infinite/finite-trace linear temporal logic and computation tree logic, and notably reachability logic, the underlying logic of the \mathbbk framework for programming language semantics and formal analysis. Matching μ -logic therefore serves as a unifying foundation for specifying and reasoning about fixpoints and induction, programming languages and program specification and verification.
DOI 原文 ·
@inproceedings{paperbot4984,
title = {Matching μ-Logic},
author = {Xiaohong Chen and Grigore Rosu},
booktitle = {LICS},
year = {2019},
doi = {10.1109/lics.2019.8785675}
}