Sound and Complete Equational Reasoning over Comodels - Schröder, Lutz; Pattinson, Dirk (Proc. Mathematical Foundations of Programming Semantics XXXI, MFPS 2015, 2015)
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.
UnivIS-Import:2016-02-10:Pub.2015.tech.IMMD.profes_1.sounda
Keywords: Equational Logic; Comodels; Completeness; Bisimulation