Files in this item

FilesDescriptionFormat

application/pdf

application/pdfrodrigues-chen-rosu-2021-tr.pdf (721kB)
(no description provided)PDF

Description

Title:Technical Report: Decidable Fragments of Matching Logic
Author(s):Rodrigues, Nishant; Chen, Xiaohong; Rosu, Grigore
Subject(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.
Issue Date:2021-02-02
Citation Info:@techreport{chen-rosu-2020-tr, author = {Nishant Rodrigues, Xiaohong Chen and Grigore Ro\c{s}u}, title = {Technical Report: Decidable Fragments of Matching Logic}, author_id = {Nishant Rodrigues and Xiaohong Chen and Grigore Rosu}, category = {fsl,matching_logic,program_verification}, project_url = {http://www.matching-logic.org}, project_name = {Matching Logic}, institution = {University of Illinois at Urbana-Champaign}, month = {February}, year = {2021}, number = {http://hdl.handle.net/2142/106608}, 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. }, }
Genre:Technical Report
Type:Text
Language:English
URI:http://hdl.handle.net/2142/109255
Date Available in IDEALS:2021-02-02


This item appears in the following Collection(s)

Item Statistics