Interpretability of First—Order Dynamic Logic in a Relational Calculus

Dynamic logic has become a very useful tool in Computer Science, with direct applications in system specification. Here we show how to interpret first-order dynamic logic in an extension of the relational calculus of fork algebras. That is, reasoning in first-order dynamic logic can be replaced by equational reasoning in the extended relational calculus. This allows to: (a) incorporate the features of dynamic logic in a relational framework, and, (b) provide an equational calculus for reasoning in first-order dynamic logic.