Matching μ-Logic

Chen, Xiaohong; Roşu, Grigore

Permalink

https://hdl.handle.net/2142/102281 Copy

Description

Title

Matching μ-Logic

Author(s)

• Chen, Xiaohong
• Roşu, Grigore

Issue Date

2019-01-19

Keyword(s)

Logic, Verification, Rewriting, K

Abstract

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 μ-logic, an extension of matching logic with a least fixpoint μ-binder. It is shown that matching μ-logic captures as special instances many important logics in mathematics and computer science, including first-order logic with least fixpoints, modal μ-logic 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 K 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.

Type of Resource

text

Permalink

http://hdl.handle.net/2142/102281

Owning Collections