3 papers
cs.LO2022
Embedding Kozen-Tiuryn Logic into Residuated One-Sorted Kleene Algebra with Tests
Igor Sedlár, Johann J. Wannenburg
Kozen and Tiuryn have introduced the substructural logic for reasoning about correctness of while programs (ACM TOCL, 2003). The logic distinguishes betwe…
math.LO2022
Semilinear De Morgan monoids and epimorphisms
Johann J. Wannenburg, James G. Raftery
A representation theorem is proved for De Morgan monoids that are (i) semilinear, i.e., subdirect products of totally ordered algebras, and (ii) negatively generated, i.e., generat…
cs.LO2022
One-sorted Program Algebras
Igor Sedlár, Johann J. Wannenburg
Kleene algebra with tests, KAT, provides a simple two-sorted algebraic framework for verifying properties of propositional while programs. Kleene algebra with domain, KAD, is a one…