Files in this item

FilesDescriptionFormat

application/pdf

rodrigues-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
﻿