Sound and Complete Equational Reasoning over Comodels

Dirk Pattinson; Lutz Schröder

doi:10.1016/j.entcs.2015.12.019

Sound and Complete Equational Reasoning over Comodels

Dirk Pattinson, Lutz Schröder

Research output: Contribution to journal › Article › peer-review

5 Citations (Scopus)

Abstract

Comodels of Lawvere theories, i.e. models in Set^op, 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.

Original language	English
Pages (from-to)	315-331
Number of pages	17
Journal	Electronic Notes in Theoretical Computer Science
Volume	319
DOIs	https://doi.org/10.1016/j.entcs.2015.12.019
Publication status	Published - 21 Dec 2015

Access to Document

10.1016/j.entcs.2015.12.019

Cite this

@article{fec9d1171a284cdf9d948e726df01412,

title = "Sound and Complete Equational Reasoning over Comodels",

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.",

keywords = "Bisimulation, Comodels, Completeness, Equational Logic",

author = "Dirk Pattinson and Lutz Schr{\"o}der",

note = "Publisher Copyright: {\textcopyright} 2015 Published by Elsevier B.V.",

year = "2015",

month = dec,

day = "21",

doi = "10.1016/j.entcs.2015.12.019",

language = "English",

volume = "319",

pages = "315--331",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier B.V.",

}

TY - JOUR

T1 - Sound and Complete Equational Reasoning over Comodels

AU - Pattinson, Dirk

AU - Schröder, Lutz

PY - 2015/12/21

Y1 - 2015/12/21

N2 - 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.

AB - 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.

KW - Bisimulation

KW - Comodels

KW - Completeness

KW - Equational Logic

UR - http://www.scopus.com/inward/record.url?scp=84951781973&partnerID=8YFLogxK

U2 - 10.1016/j.entcs.2015.12.019

DO - 10.1016/j.entcs.2015.12.019

M3 - Article

SN - 1571-0661

VL - 319

SP - 315

EP - 331

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

ER -

Sound and Complete Equational Reasoning over Comodels

Abstract

Access to Document

Other files and links

Fingerprint

Cite this