In the field of structural operational semantics (SOS), there have been several proposals both for syntactic rule formats guaranteeing the validity of algebraic laws, and for algorithms for automatically generating ground-complete axiomatizations. However, there has been no synergy between these two types of results. This paper takes the first steps in marrying these two areas of research in the meta-theory of SOS and shows that taking algebraic laws into account in the mechanical generation of axiomatizations results in simpler axiomatizations. The proposed theory is applied to a paradigmatic example from the literature, showing that, in this case, the generated axiomatization coincides with a classic hand-crafted one.
|Name||Lecture Notes in Computer Science|
|Conference||conference; 5th International Conference on Algebra and Coalgebra in Computer Science; 2013-09-03; 2013-09-06|
|Period||3/09/13 → 6/09/13|
|Other||5th International Conference on Algebra and Coalgebra in Computer Science|