Sound and Complete Equational Reasoning over Comodels
| Autor: | Dirk Pattinson, Lutz Schröder |
|---|---|
| Jazyk: | angličtina |
| Předmět: |
Bisimulation
Completeness Comodels General Computer Science Modulo Coinduction Mathematical proof Theoretical Computer Science Algebra Completeness (order theory) Computer Science::Logic in Computer Science Computer Science::Programming Languages State (computer science) Algebraic number Equational logic Equational Logic Mathematics Computer Science(all) |
| Zdroj: | MFPS |
| ISSN: | 1571-0661 |
| DOI: | 10.1016/j.entcs.2015.12.019 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|