Rewriting logic appears to have good properties as logical framework, and can be useful for the development of programming languages which attempt to integrate various paradigms of declarative programming. In this paper I propose to tend towards the operational semantics for such languages by basing it on bi-rewrite systems and ordered chaining calculi which apply rewrite techniques to first-order theories with arbitrary possibly non-symmetric transitive relations, because this was an important breakthrough for the automation of deduction in these kind of theories. I show that a proof calculus based on the bi-rewriting technique may serve as framework of different proof calculi, by analizing those of equational logic and Horn logic, and presenting them as specific cases of bi-rewrite systems. Deduction is then essentially bi-rewriting a theory of rewriting logic. Since recently the interest in specifications based on theories with transitive relations has arisen, the result of this research towards a general framework for bi-rewriting based operational semantics of several programming paradigms will also be very useful for the development of rapid prototyping tools for these kind of specifications. © 2000.

Supported by project DISCOR (TIC 94-0847-C02-01) funded by the CICYT

Peer Reviewed