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 which go beyond pure equational Horn logic: either the rules are impure by involving nonequational side-conditions, or they 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. This paper presents a positive and a negative result regarding axiomatisability of observational congruence in equational Horn logic. Firstly, we show how Milner's impure rule system can be reworked into a pure Horn axiomatisation that is complete for guarded processes. Secondly, we prove that for unguarded processes, both Milner's and Bloom/Ésik's axiomatisations are incomplete without the congruence rule, and neither system has a complete extension in rank 1 equational axioms. It remains open whether there are higher-rank equational axioms or Horn rules which would render Milner's or Bloom/Ésik's axiomatisations complete for unguarded processes. |
Year | DOI | Venue |
---|---|---|
2007 | 10.1007/978-3-540-74407-8_14 | CONCUR |
Keywords | Field | DocType |
equational horn logic,unguarded process,pure horn axiomatisation,equational axiom,pure equational,observational congruence axiomatisable,equational logic,higher-rank equational axiom,congruence rule,horn logic,horn rule | Discrete mathematics,Axiom,Horn logic,Bisimulation,Equational logic,Process calculus,Congruence (geometry),Mathematics | Conference |
Volume | ISSN | ISBN |
4703 | 0302-9743 | 3-540-74406-1 |
Citations | PageRank | References |
1 | 0.34 | 22 |
Authors | ||
2 |
Name | Order | Citations | PageRank |
---|---|---|---|
Michael Mendler | 1 | 314 | 34.60 |
Gerald Lüttgen | 2 | 600 | 40.71 |