A syntactic commutativity format for SOS
Mousavi, M.R., Reniers, Jan Friso Groote · TU/e Research Portal · 2004
Considering operators defined using Structural Operational Semantics (SOS), commuta-tivity axioms are intuitive properties that hold for many of them. Proving this intuition is usually a laborious task, requiring several pages of boring and standard proof. To save this effort, we propose a syntactic SOS format which guarantees commutativity for a set of com-position operators.