Quelle  root.bib

@inproceedings{DesharnaisJipsenStruth,
  author    = {Desharnais, J. and Jipsen, P. and Struth, G.},
  title     = {Domain and Antidomain Semigroups},
  booktitle = {Relations and {Kleene} Algebra in Computer Science},
  editor    = {Berghammer, R. and Jaoua, A. and M{\"{o}}ller, B.},
  series    = {Lecture Notes in Computer Science},
  volume    = {5827},
  publisher = {Springer},
  year      = {2009},
  pages     = {73--87},
  year      = {2009}
}

@article{DesharnaisMoellerStruthLMCS,
  author    = {Desharnais, J. and M{\"{o}}ller, B. and Struth, G.},
  title     = {Algebraic Notions of Termination},
  journal   = {Logical Methods in Computer Science},
  volume    = {7},
  number    = {1},
  year      = {2011}
}

@inproceedings{DesharnaisStruthAMAST,
  author    = {Desharnais, J. and Struth, G.},
  title     = {Domain Axioms for a Family of Near-Semirings},
  booktitle = {{AMAST} 2008},
  pages     = {330--345},
  year      = {2008},
  editor    = {Meseguer, J. and Rosu, G.},
  series    = {Lecture Notes in Computer Science},
  volume    = {5140},
  publisher = {Springer},
  year      = {2008}
}

@article{DesharnaisStruthSCP,
  author    = {Desharnais, J. and Struth, G.},
  title     = {Internal axioms for domain semirings},
  journal   = {Science of Computer Programming},
  volume    = {76},
  number    = {3},
  pages     = {181--203},
  year      = {2011}
}

@article{FurusawaStruth,
  author    = {Furusawa, H. and Struth, G.},
  title     = {Concurrent Dynamic Algebra},
  journal   = {{ACM} {TOCL}},
  volume    = {16},
  number    = {4},
  pages     = {30},
  year      = {2015}
}

@article{MoellerStruth,
  author    = {M{\"{o}}ller, B. and Struth, G.},
  title     = {Algebras of modal operators and partial correctness},
  journal   = {Theoretical Computer Science},
  volume    = {351},
  number    = {2},
  pages     = {221--239},
  year      = {2006}
}


@article{Solin11,
  author    = {Solin, K.},
  title     = {Normal forms in total correctness for while programs
                  and action systems},
  journal   = {J.\ Logic and Algebraic Programming},
  volume    = {80},
  number    = {6},
  year      = {2011},
  pages     = {362--375}
}

@inproceedings{armstrongstruth12hoka,
  author    = {Alasdair Armstrong and Georg Struth},
  title     = {Automated Reasoning in Higher-Order Regular Algebra},
  booktitle = {{RAMICS} 2012},
  year      = {2012},
  pages     = {66-81},
  ee        = {https://doi.org/10.1007/978-3-642-33314-9_5},
  editor    = {Wolfram Kahl and Timothy G. Griffin},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {7560}
}

@inproceedings{bachmair86commutation,
  author    = {Leo Bachmair and Nachum Dershowitz},
  title     = {Commutation, Transformation, and Termination},
  editor    = {J{\"o}rg H. Siekmann},
  booktitle = {Conference on Automated Deduction},
  volume    = {230},
  series    = {Lecture Notes in Computer Science},
  pages     = {5--20},
  publisher = {Springer},
  year      = {1986},
  ee        = {https://doi.org/10.1007/3-540-16780-3_76}
}

@book{birkhoff67lattices,
  author    = {Garrett Birkhoff},
  title     = {Lattice Theory},
  publisher = {American Mathematical Society Colloquium Publications},
  year      = {1967}
}

@article{boffa90remarque,
  author  = {Maurice Boffa},
  title   = {Une remarque sur les syst\`emes complets d'identit\'es
                  rationnelles},
  journal = {Informatique The\'eorique et Applications},
  year    = {1990},
  volume  = {24},
  number  = {4},
  pages   = {419--423}
}

@inproceedings{cohen00omega,
  author    = {Ernie Cohen},
  title     = {Separation and Reduction},
  booktitle = {MPC},
  year      = {2000},
  pages     = {45--59},
  ee        = {https://doi.org/10.1007/10722010_4},
  editor    = {Roland Carl Backhouse and Jos{\'e} Nuno Oliveira},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {1837}
}

@book{conway71regular,
  author    = {Conway, John Horton},
  title     = {Regular Algebra and Finite Machines},
  publisher = {Chapman and Hall},
  year      = {1971}
}

@inproceedings{dershowitz09lazy,
  author    = {Nachum Dershowitz},
  title     = {On Lazy Commutation},
  editor    = {Orna Grumberg and Michael Kaminski and Shmuel Katz and
                  Shuly Wintner},
  booktitle = {Languages: From Formal to Natural},
  volume    = {5533},
  series    = {Lecture Notes in Computer Science},
  pages     = {59--82},
  publisher = {Springer},
  year      = {2009},
  ee        = {https://doi.org/10.1007/978-3-642-01748-3_5}
}

@article{desharnaismoellerstruth06kad,
  author    = {Jules Desharnais and Bernhard M{\"o}ller and Georg
                  Struth},
  title     = {{Kleene} Algebra with Domain},
  journal   = {ACM {TOCL}},
  volume    = {7},
  number    = {4},
  year      = {2006},
  pages     = {798-833},
  ee        = {http://doi.acm.org/10.1145/1183278.1183285}
}

@article{doornbos97calculational,
  author    = {Henk Doornbos and Roland Carl Backhouse and Jaap van
                  der Woude},
  title     = {A Calculational Approach to Mathematical Induction},
  journal   = {Theoretical Computer Science},
  volume    = {179},
  number    = {1--2},
  year      = {1997},
  pages     = {103--135},
  ee        = {https://doi.org/10.1016/S0304-3975(96)00154-5}
}

@inproceedings{fosterstruth12regalg,
  author    = {Simon Foster and Georg Struth},
  title     = {Automated Analysis of Regular Algebra},
  booktitle = {{IJCAR} 2012},
  year      = {2012},
  pages     = {271--285},
  ee        = {https://doi.org/10.1007/978-3-642-31365-3_22},
  editor    = {Bernhard Gramlich and Dale Miller and Uli Sattler},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {7364}
}

@inproceedings{fosterstruthweber11tutorial,
  author    = {Simon Foster and Georg Struth and Tjark Weber},
  title     = {Automated Engineering of Relational and Algebraic
                  Methods in {Isabelle}/{HOL} -- (Invited Tutorial)},
  booktitle = {{RAMICS}},
  year      = {2011},
  editor    = {Harrie C. M. de Swart},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6663},
  pages     = {52--67},
  ee        = {https://doi.org/10.1007/978-3-642-21070-9_5}
}

@book{galatosjipsenkowalskiono07residuated,
  author    = {Nikolaos Galatos and Peter Jipsen and Tomasz Kowalski
                  and Hiroakira Ono},
  title     = {Resituated Lattices: An Algebraic Glimpse at
                  Substructural Logics},
  publisher = {Elsevier},
  year      = {2007}
}

@book{gondran10graphs,
  author    = {Michel Gondran and Michel Minoux},
  title     = {Graphs, Dioids and Semirings: New Models and Algorithms},
  volume    = {41},
  series    = {Operations Research/Computer Science Interfaces},
  publisher = {Springer},
  year      = {2010}
}

@inproceedings{guttmannstruthweber11algmeth,
  author    = {Walter Guttmann and Georg Struth and Tjark Weber},
  title     = {Automating Algebraic Methods in {Isabelle}},
  booktitle = {{ICFEM} 2011},
  year      = {2011},
  pages     = {617-632},
  ee        = {https://doi.org/10.1007/978-3-642-24559-6_41},
  editor    = {Shengchao Qin and Zongyan Qiu},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6991}
 }

@inproceedings{guttmannstruthweber11tarskikleene,
  author    = {Walter Guttmann and Georg Struth and Tjark Weber},
  title     = {A Repository for {Tarski}-{Kleene} Algebras},
  booktitle = {{ATE} 2011},
  year      = {2011},
  pages     = {30--39},
  ee        = {http://ceur-ws.org/Vol-760/paper5.pdf},
  editor    = {Peter H{\"o}fner and Annabelle McIver and Georg Struth},
  publisher = {CEUR-WS.org},
  series    = {CEUR Workshop Proceedings},
  volume    = {760}
}

@book{harelkozentiuryn00dynamic,
  author    = {David Haren and Dexter Kozen and Jerzy Tiuryn},
  title     = {Dynamic Logic},
  publisher = {MIT Press},
  year      = {2000}
}

@article{hofnerstruth10nontermination,
  author    = {Peter H{\"o}fner and Georg Struth},
  title     = {Algebraic notions of nontermination: Omega and
                  divergence in idempotent semirings},
  journal   = {J.\ Log.\ Algebr.\ Program.},
  volume    = {79},
  number    = {8},
  year      = {2010},
  pages     = {794-811},
  ee        = {https://doi.org/10.1016/j.jlap.2010.07.016}
}

@article{ka,
  author  = {Armstrong, A. and Gomes, Victor B. F. and Struth, G. and
                  Weber, T.},
  title   = {{Kleene} Algebra},
  journal = {Archive of Formal Proofs},
  year    = {2013}
}

@article{kat,
  author  = {Armstrong, A. and Gomes, Victor B. F. and Struth, G.},
  title   = {Kleene Algebra with Tests},
  journal = {Archive of Formal Proofs},
  year    = {2014}
}

@article{kad,
  author  = {Gomes, Victor B. F. and Guttmann, W. and H{\"o}fner,
                  P. and Struth, G. and Weber, T.},
  title   = {Kleene Algebra with Domain},
  journal = {Archive of Formal Proofs},
  year    = {2016}
}

@article{kozen00hoare,
  author    = {Dexter Kozen},
  title     = {On {Hoare} logic and {Kleene} algebra with tests},
  journal   = {ACM Trans.\ Comput.\ Log.},
  volume    = {1},
  number    = {1},
  year      = {2000},
  pages     = {60--76},
  ee        = {https://doi.org/10.1145/343369.343378}
}

@inproceedings{kozen90kleene,
  author    = {Dexter Kozen},
  title     = {On {Kleene} Algebras and Closed Semirings},
  editor    = {Branislav Rovan},
  booktitle = {Mathematical Foundations of Computer Science},
  volume    = {452},
  series    = {Lecture Notes in Computer Science},
  pages     = {26--47},
  publisher = {Springer},
  year      = {1990},
  ee        = {https://doi.org/10.1007/BFb0029594}
}

@article{kozen94complete,
  author    = {Dexter Kozen},
  title     = {A Completeness Theorem for {Kleene} Algebras and the
                  Algebra of Regular Events},
  journal   = {Inf.\ Comput.},
  volume    = {110},
  number    = {2},
  year      = {1994},
  pages     = {366-390},
  ee        = {https://doi.org/10.1006/inco.1994.1037}
}

@article{krauss12regular,
  author    = {Alexander Krauss and Tobias Nipkow},
  title     = {Proof Pearl: Regular Expression Equivalence and
                  Relation Algebra},
  journal   = {J.\ Autom.\ Reasoning},
  volume    = {49},
  number    = {1},
  year      = {2012},
  pages     = {95--106},
  ee        = {https://doi.org/10.1007/s10817-011-9223-4}
}

@inproceedings{mciverweber05pka,
  author    = {Annabelle McIver and Tjark Weber},
  title     = {Towards Automated Proof Support for Probabilistic
                  Distributed Systems},
  booktitle = {LPAR},
  series    = {Lecture Notes in Computer Science},
  volume    = {3835},
  year      = {2005},
  editor    = {Geoff Sutcliffe and Andrei Voronkov},
  pages     = {534--548}
}

@article{multirelations,
  author    = {Furusawa, H. and Struth, G.},
  title     = {Binary Multirelations},
  journal   = {Archive of Formal Proofs},
  year      = {2015}
}

@book{pilz83nearrings,
  author    = {G{\"u}nter Pilz},
  title     = {Near-rings},
  publisher = {North-Holland},
  address   = {Amsterdam},
  edition   = {Second},
  year      = {1983}
}

@inproceedings{pratt90action,
  author    = {Vaughan R. Pratt},
  title     = {Action Logic and Pure Induction},
  editor    = {Jan van Eijck},
  booktitle = {Logics in AI, European Workshop, JELIA '90},
  volume    = {478},
  series    = {Lecture Notes in Computer Science},
  pages     = {97--120},
  publisher = {Springer},
  year      = {1991},
  ee        = {https://doi.org/10.1007/BFb0018436}
}

@article{regalg,
  author  = {Foster, S. and Struth, G.},
  title   = {Regular Algebras},
  journal = {Archive of Formal Proofs},
  year    = {2014}
}

@article{rel,
  author  = {Armstrong, A. and Foster, S. and Guttmann, W. and Struth,
                  G. and Weber, T.},
  title   = {Relation Algebra},
  journal = {Archive of Formal Proofs},
  year    = {2014}
}

@article{struth06churchrosser,
  author    = {Georg Struth},
  title     = {Abstract abstract reduction},
  journal   = {J.\ Log.\ Algebr.\ Program.},
  volume    = {66},
  number    = {2},
  year      = {2006},
  pages     = {239-270},
  ee        = {https://doi.org/10.1016/j.jlap.2005.04.001}
}

@article{struth12regeq,
  author    = {Georg Struth},
  title     = {Left omega algebras and regular equations},
  journal   = {J.\ Log.\ Algebr.\ Program.},
  volume    = {81},
  number    = {6},
  year      = {2012},
  pages     = {705-717},
  ee        = {https://doi.org/10.1016/j.jlap.2012.05.004}
}

@article{venema03gamealgebra,
  author    = {Yde Venema},
  title     = {Representation of Game Algebras},
  journal   = {Studia Logica},
  volume    = {75},
  number    = {2},
  year      = {2003},
  pages     = {239-256},
  ee        = {https://doi.org/10.1023/A:1027363028181}
}

@article{vonwright04refinement,
  author    = {Joakim von Wright},
  title     = {Towards a refinement algebra},
  journal   = {Sci.\ Comput.\ Program.},
  volume    = {51},
  number    = {1-2},
  year      = {2004},
  pages     = {23-45},
  ee        = {https://doi.org/10.1016/j.scico.2003.09.002}
}

@article{wagner77omega,
  author    = {Klaus W. Wagner},
  title     = {Eine topologische {C}harakterisierung einiger {K}lassen
                  regul{\"a}rer {F}olgenmengen},
  journal   = {Elektronische Informationsverarbeitung und Kybernetik},
  volume    = {13},
  number    = {9},
  year      = {1977},
  pages     = {473-487}
}

@book{weightedautomata09,
  editor    = {Manfred Droste and Werner Kuich and Heiko Vogler},
  title     = {Handbook of Weighted Automata},
  publisher = {Springer},
  year      = {2009}
}

@book{maddux,
  author    = {Maddux, R. D.},
  title     = {Relation Algebras},
  publisher = {Elsevier},
  year      = {2006}
}