Technical Report: Decidable Fragments of Matching Logic

Rodrigues, Nishant; Chen, Xiaohong; Rosu, Grigore

Permalink

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

Description

Title

Technical Report: Decidable Fragments of Matching Logic

Author(s)

• Rodrigues, Nishant
• Chen, Xiaohong
• Rosu, Grigore

Issue Date

2021-02-02

Keyword(s)

• matching logic
• modal logic
• temporal logic
• decidability

Abstract

Matching logic is a unifying logic aimed at defining programming language semantics, and reasoning about various program and language properties. It is a general logic designed with minimalism in mind. With only eight syntactic constructs, matching logic can define many important logical frameworks and languages as its theories. Yet, to our knowledge, no research has been conducted into the decidabiltiy of matching logic. In this paper, we begin such an initiative with respect to decidable fragments of matching logic and identify the first non-trivial decidable fragment for the empty theory. Our decision procedure extends a tableau system for modal \(\mu\)-calculus. We also give an implementation of the proposed decision procedure and show that with modifications, it can be extended to support theories with certain axioms.

Type of Resource

text

Language

en

Permalink

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

Owning Collections