Rewriting Logic as a Logic of Special Relations

AbstractI 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