Matching logic
Matching logic is a formal logic mainly used to reason about the correctness of computer programs. Its operators use pattern matching to operate on the power set of states, rather than the set of states. It was created by Grigore Roșu and is used in the K Framework. Overview 

Matching logic operates on patterns. Statements evaluate to the set of values that "match" them, not to true or false. Given a set of signatures , a pattern can be:

 A variable: 
 A structure following signature  using other patterns: 
 The complement of another pattern: 
 The intersection of two patterns: 
 A binding:   with 

A matching logic may also have a set  of sorts. In that case, each pattern belongs to a particular sort. Structures can be used to combine patterns of different sorts together. Some example of sorts used when working with program semantics might be "32-bit integer values", "stack frames", or "heap memory". Some derived concepts are defined as:

 
 
 
 
 
 

 is matched by all elements. is matched by none. "One should be careful when reasoning with such non-classic logics, as basic intuitions may deceive." When interpreting matching logic (that is, defining its semantic meaning), a pattern is modeled with a power set. The statement's interpretation is the set of values that match the pattern. Matching μ-Logic

Matching -logic adds a fixed-point operator . Applications 

Matching logic is used with reachability logic by the K Framework to specify an operational semantics and, from them, to create a Hoare logic. Matching logic can be converted to first-order logic with equality, which allows the K Framework to use existing SMT-solvers to find proofs for theorems. See also 

 Separation logic
 Hoare logic
 Regular expression, which matches sets of strings

References

Logic