Matching Logic: A Logic for Structural Reasoning

Permalink

https://hdl.handle.net/2142/47004

Title: Matching Logic: A Logic for Structural Reasoning
Author(s): Rosu, Grigore
Issue Date: 2014-01-20
Keyword(s): first-order logic, separation logic, matching logic
Abstract: Matching logic is a first-order logic (FOL) variant to reason about structure. Its sentences, called patterns, are constructed using variables, symbols, connectives and quantifiers, but no dif ference is made between function and predicate symbols. In models, a pattern evaluates into a power-set domain (the set of values that match it), in contrast to FOL where functions, predicates and connectives map into a domain. Matching logic generalizes several logical frameworks important for program analysis, such as: propositional logic, algebraic specification, FOL with equality, and separation logic. Patterns allow for specifying separation requirements at any level in any program configuration, not only in the heaps or stores, without any special logical constructs for that: the very nature of pattern matching is that if two structures are matched as part of a pattern, then they can only be spatially separated. Like FOL, matching logic can also be translated into pure predicate logic with equality, but it also admits its own sound and complete proof system.
Type of Resource: text
Language: en
Permalink: http://hdl.handle.net/2142/47004