Matching μ-Logic

Xiaohong Chen, Grigore Rosu

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 μ-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 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.

Original languageEnglish (US)
Title of host publication2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019
PublisherInstitute of Electrical and Electronics Engineers Inc.
ISBN (Electronic)9781728136080
DOIs
StatePublished - Jun 2019
Event34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019 - Vancouver, Canada
Duration: Jun 24 2019Jun 27 2019

Publication series

NameProceedings - Symposium on Logic in Computer Science
Volume2019-June
ISSN (Print)1043-6871

Conference

Conference34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019
CountryCanada
CityVancouver
Period6/24/196/27/19

Fingerprint

Temporal logic
Computer programming languages
Acoustic waves
Logic
Pattern matching
Computer science
Binders
Semantics
Fixpoint
Specifications
Programming Languages
Reasoning
Linear Temporal Logic
Semantic Analysis
Dynamic Logic
Proof System
Formal Analysis
Deduction
Pattern Matching
First-order Logic

ASJC Scopus subject areas

  • Software
  • Mathematics(all)

Cite this

Chen, X., & Rosu, G. (2019). Matching μ-Logic. In 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019 [8785675] (Proceedings - Symposium on Logic in Computer Science; Vol. 2019-June). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/LICS.2019.8785675

Matching μ-Logic. / Chen, Xiaohong; Rosu, Grigore.

2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019. Institute of Electrical and Electronics Engineers Inc., 2019. 8785675 (Proceedings - Symposium on Logic in Computer Science; Vol. 2019-June).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Chen, X & Rosu, G 2019, Matching μ-Logic. in 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019., 8785675, Proceedings - Symposium on Logic in Computer Science, vol. 2019-June, Institute of Electrical and Electronics Engineers Inc., 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, Canada, 6/24/19. https://doi.org/10.1109/LICS.2019.8785675
Chen X, Rosu G. Matching μ-Logic. In 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019. Institute of Electrical and Electronics Engineers Inc. 2019. 8785675. (Proceedings - Symposium on Logic in Computer Science). https://doi.org/10.1109/LICS.2019.8785675
Chen, Xiaohong ; Rosu, Grigore. / Matching μ-Logic. 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019. Institute of Electrical and Electronics Engineers Inc., 2019. (Proceedings - Symposium on Logic in Computer Science).
@inproceedings{abe7d934c4a34883bc8ca0d2f17aaccd,
title = "Matching μ-Logic",
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 μ-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 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.",
author = "Xiaohong Chen and Grigore Rosu",
year = "2019",
month = "6",
doi = "10.1109/LICS.2019.8785675",
language = "English (US)",
series = "Proceedings - Symposium on Logic in Computer Science",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
booktitle = "2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019",
address = "United States",

}

TY - GEN

T1 - Matching μ-Logic

AU - Chen, Xiaohong

AU - Rosu, Grigore

PY - 2019/6

Y1 - 2019/6

N2 - 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 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.

AB - 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 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.

UR - http://www.scopus.com/inward/record.url?scp=85070758315&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85070758315&partnerID=8YFLogxK

U2 - 10.1109/LICS.2019.8785675

DO - 10.1109/LICS.2019.8785675

M3 - Conference contribution

AN - SCOPUS:85070758315

T3 - Proceedings - Symposium on Logic in Computer Science

BT - 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019

PB - Institute of Electrical and Electronics Engineers Inc.

ER -