Interpretability of First-Order Dynamic Logic in an Extension of Fork Algebras
by
Marcelo Frias
Department of Computer Science, University of Buenos Aires
Coauthors: Gabriel A. Baum (LIFIA, School of Informatics, Universidad Nacional de La Plata, Argentina), Thomas S.E.Maibaum (Department of Computer Science, King's College, London, UK)

Dynamic Logic has become a very useful tool in Computer Science, specially in system specification. Relational methods have also become of interest in the same field. Here we show how to extend a relational framework (fork algebras), in order to (a) be able to adopt the dynamic features of Dynamic Logic in a relational framework, and, (b) provide an equational (although infinitary) calculus for reasoning in First-Order Dynamic Logic.

We will present the calculus and an interpretability theorem stating that reasoning in Dynamic Logic theories can be carried on in an equational calculus that extends the relational calculus and also the fork algebra calculus.

The techniques used in proofs come from previous results reported in [FM01] [FO97] [FO98].

[FM01] Frias M.F. and Maddux R.D., Completeness of a Relational Calculus for Program Schemes, Theoretical Computer Science, Elsevier, to appear.

[FO97] Frias, M.F. and Orlowska E., A Proof System for Fork Algebras and its Applications to Reasoning in Logics Based on Intuitionism, Logique et Analyse vol.150-151-152 (1997), pp.239-284.

[FO98] Frias M.F. and Orlowska E., Equational Reasoning in Non Classical Logics, Journal of Applied Non Classical Logics, Vol.8, No.1-2, pp.27-66, 1998.

Date received: January 2, 2001

Copyright © 2001 by the author(s). The author(s) of this document and the organizers of the conference have granted their consent to include this abstract in Atlas Conferences Inc. Document # cafo-48.