Interpretability of First-Order Dynamic Logic in a Relational Calculus

FRIAS, MARCELO FABIAN; BAUM, GABRIEL; MAIBAUM, THOMAS STEPHEN EDWARD

LECTURE NOTES IN COMPUTER SCIENCE

Springer

Año: 2002 vol. 2561 p. 66 - 80

0302-9743

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.