@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}
}
