Exploiting Algebraic Laws to Improve Mechanized Axiomatizations
2013 (English)In: Algebra and Coalgebra in Computer Science: 5th International Conference, Calco 2013, Warsaw, Poland, September 2013, Proceedings, Berlin: Springer Berlin/Heidelberg, 2013, 36-50 p.Conference paper (Refereed)
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. © 2013 Springer-Verlag Berlin Heidelberg.
Place, publisher, year, edition, pages
Berlin: Springer Berlin/Heidelberg, 2013. 36-50 p.
, Lecture Notes in Computer Science, ISSN 0302-9743 ; 8089
Process Algebra, Structural Operational Semantics, Bisimulation, Ground Complete Axiomatization, Algebraic Properties, Rule Formats
Computer and Information Science
IdentifiersURN: urn:nbn:se:hh:diva-22060DOI: 10.1007/978-3-642-40206-7_5ScopusID: 2-s2.0-84885981989ISBN: 9783642402067ISBN: 9783642402050OAI: oai:DiVA.org:hh-22060DiVA: diva2:619611
CALCO 2013, The 5th Conference on Algebra and Coalgebra in Computer Science, Warsaw, Poland, September 3-6, 2013
ProjectsMeta-theory of Algebraic Process TheoriesExtending and Axiomatizing Structural Operational Semantics: Theory and Tools
FundereLLIIT - The Linköping‐Lund Initiative on IT and Mobile Communications