Rewriting Logic as a Logic of Special Relations
Marco Schorlemmer · Electronic Notes in Theoretical Computer Science · 1998
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. I am very grateful to Jaume Agustí Jordi Levy, and José Meseguer for fruitful discussions and inspiring suggestions concerning the research issues presented in this paper.