Exploiting algebraic laws to improve mechanized axiomatizations

L. Aceto, E.I. Goriac, A. Ingólfsdóttir, M.R. Mousavi, M.A. Reniers

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    2 Citations (Scopus)

    Abstract

    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.
    Original languageEnglish
    Title of host publicationAlgebra and Coalgebra in Computer Science (5th International Conference, CALCO 2013, Warsaw, Poland, September 3-6, 2013, Proceedings)
    EditorsR. Heckel, S. Milius
    Place of PublicationBerlin
    PublisherSpringer
    Pages36-50
    ISBN (Print)978-3-642-40205-0
    DOIs
    Publication statusPublished - 2013
    Eventconference; 5th International Conference on Algebra and Coalgebra in Computer Science; 2013-09-03; 2013-09-06 -
    Duration: 3 Sep 20136 Sep 2013

    Publication series

    NameLecture Notes in Computer Science
    Volume8089
    ISSN (Print)0302-9743

    Conference

    Conferenceconference; 5th International Conference on Algebra and Coalgebra in Computer Science; 2013-09-03; 2013-09-06
    Period3/09/136/09/13
    Other5th International Conference on Algebra and Coalgebra in Computer Science

    Fingerprint

    Dive into the research topics of 'Exploiting algebraic laws to improve mechanized axiomatizations'. Together they form a unique fingerprint.

    Cite this