Is Observational Congruence Axiomatisable in Equational Horn Logic?

13 years 3 months ago
Is Observational Congruence Axiomatisable in Equational Horn Logic?
It is well known that bisimulation on µ-expressions cannot be finitely axiomatised in equational logic. Complete axiomatisations such as those of Milner and Bloom/´Esik necessarily involve implicational rules. However, both systems rely on features which go beyond pure equational Horn logic: either the rules are impure by involving non-equational 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/´Esik’s axiomati...
Michael Mendler, Gerald Lüttgen
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Authors Michael Mendler, Gerald Lüttgen
Comments (0)