Towards a Verification Logic for Rewriting Logic

This paper is an initial step in the development of a logic for verifying properties of programs in rewriting logic. Rewriting logic is primarily a logic of change, in which deduction corresponds directly to computation, and not a logic to talk about change in a more indirect and global manner, such as the different modal and temporal logics that can be found in the literature.We start by defining a modal action logic (VLRL) in which rewrite …