[1] Statements evaluate to the set of values that "match" them, not to true or false.
Some examples of sorts used when working with program semantics might be "32-bit integer values", "stack frames", or "heap memory".
"One should be careful when reasoning with such non-classic logics, as basic intuitions may deceive.
"[1] 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 can be converted to first-order logic with equality, which allows the K Framework to use existing SMT-solvers to find proofs for theorems.