zbMATH — the first resource for mathematics

Rewriting logic as a logic of special relations. (English) Zbl 0917.68109
Kirchner, Claude (ed.) et al., International workshop on Rewriting logic and its applications. Abbaye des Prèmontrès at Pont-á-Mousson, France, September 1998. Amsterdam: Elsevier, Electronic Notes in Theoretical Computer Science. 15, electronic paper No. 12 (1998).
Summary: I formally define a logic of special relations with the purpose of capturing those logics that, by using several binary relations besides equality in their logical sentences, enhance the expressiveness of order-sorted equational logic. I believe that a general notion of rewriting along binary relations – that I briefly introduce in this paper – may constitute a kernel upon which particular rewriting based proof calculi for these logics can be constructed. As an example, I show how rewriting logic is captured in this logic of special relations by means of a map of logics as defined in Meseguer’s framework of general logics. This map highlights the expressive gain of this framework – since the properties of the rewrite relation are stated explicitly – while keeping a rewrite-based proof calculus. I also discuss, on the example of membership equational logic, how the general perspective of term rewriting presented in this paper unifies, under a unique notion of local confluence, several up to now distinct decidability conditions for logical theories.
For the entire collection see [Zbl 0903.00070].

68Q42 Grammars and rewriting systems
rewriting logic
Full Text: Link