Sound and Complete Equational Reasoning over Comodels
Schröder L, Pattinson D (2015)
Publication Type: Conference contribution, Original article
Publication year: 2015
Journal
Publisher: Elsevier BV
Edited Volumes: Electronic Notes in Theoretical Computer Science
Series: Electronic Notes in Theoretical Computer Science
Book Volume: 319
Pages Range: 315-331
Conference Proceedings Title: Proc. Mathematical Foundations of Programming Semantics XXXI, MFPS 2015
Event location: Nijmegen
URI: http://www8.cs.fau.de/_media/research:papers:comodels-compl.pdf
DOI: 10.1016/j.entcs.2015.12.019
Abstract
Comodels of Lawvere theories, i.e. models in Setop, model state spaces with algebraic access operations. Standard equational reasoning is known to be sound but incomplete for comodels. We give two sound and complete calculi for equational reasoning over comodels: an inductive calculus for equality-on-the-nose, and a coinductive/inductive calculus for equality modulo bisimulation which captures bisimulations syntactically through non-wellfounded proofs.
Authors with CRIS profile
Related research project(s)
Coinduction Meets Algebra For the Axiomatization of System Equivalence (COAX)
Oct. 1, 2014 - July 31, 2018
Probabilistische Beschreibungslogik als Fragment der Probabilistischen Logik Erster Stufe (ProbDL)
April 1, 2011 - April 1, 2014
Involved external institutions
Australia (AU)How to cite
APA:
Schröder, L., & Pattinson, D. (2015). Sound and Complete Equational Reasoning over Comodels. In Proc. Mathematical Foundations of Programming Semantics XXXI, MFPS 2015 (pp. 315-331). Nijmegen: Elsevier BV.
MLA:
Schröder, Lutz, and Dirk Pattinson. "Sound and Complete Equational Reasoning over Comodels." Proceedings of the Mathematical Foundations of Programming Semantics XXXI, Nijmegen Elsevier BV, 2015. 315-331.
BibTeX: Download