Name
Abstract | ||
|---|---|---|
It is well known that bisimulation on μ-expressions cannot be finitely axiomatised in equational logic. Complete axiomatisations such as those of Milner and Bloom/Ésik necessarily involve implicational rules. However, both systems rely on features beyond pure equational Horn logic: either rules that are impure by involving non-equational side-conditions, or rules that are schematically infinitary like the congruence rule which is not Horn. It is an open question whether these complications cannot be avoided in the proof-theoretically and computationally clean and powerful setting of second-order equational Horn logic. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1016/j.ic.2009.05.005 | Information and Computation |
Keywords | DocType | Volume |
Process algebra,μ-Expressions,Observational congruence,Finite axiomatisation,Horn logic | Journal | 208 |
Issue | ISSN | Citations |
6 | 0890-5401 | 1 |
PageRank | References | Authors |
0.34 | 0 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Michael Mendler | 1 | 314 | 34.60 |
| Gerald Lüttgen | 2 | 600 | 40.71 |