Abstract
Database Abstract State Machines (DB-ASMs) provide a universal computation model for database transformations that encompass queries and updates. In this paper we present a proof system for DB-ASMs. It is shown that the proof system for DB-ASMs is sound. As DB-ASMs are restricted by allowing quantifiers over only the database part of a state which is a finite structure, we can formalise non-determinism of DB-ASMs by utilising a modal operator [] for an update set or multiset generated by a DB-ASM rule. In doing so, we lay down a solid foundation for the completeness proof of the proof system proposed for DB-ASMs in this paper.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Börger, E., Stärk, R.F.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003)
Grädel, E., Gurevich, Y.: Metafinite model theory. Information and Computation 140(1), 26–81 (1998)
Groenboom, R., de Renardel Lavalette, G.: Reasoning about dynamic features in specification languages - a modal view on creation and modification. In: Proceedings of the International Workshop on Semantics of Specification Languages (SoSL), pp. 340–355. Springer, Heidelberg (1994)
Groenboom, R., de Renardel Lavalette, G.: A formalization of evolving algebras. In: Proceedings of Accolade 1995 (1995); Dutch Research School in Logic
Gurevich, Y.: Sequential abstract state machines capture sequential algorithms. ACM Transactions on Computational Logic 1(1), 77–111 (2000)
Hughes, G., Cresswell, M.: A new introduction to modal logic. Burns & Oates (1996)
de Renardel Lavalette, G.: A logic of modification and creation. In: Logical Perspectives on Language and Information. CSLI publications, Stanford (2001)
Schewe, K.-D., Wang, Q.: A customised ASM thesis for database transformations. Acta Cybernetica 19(4), 765–805 (2010)
Schönegge, A.: Extending Dynamic Logic for Reasoning about Evolving Algebras. Technical Report 49/95, Universität Karlsruhe, Fakultät für Informatik (1995)
Stärk, R., Nanchen, S.: A logic for abstract state machine. Journal of Universal Computer Science 7(11) (2001)
Van den Bussche, J.: Formal Aspects of Object Identity in Database Manipulation. PhD thesis, University of Antwerp (1993)
Van den Bussche, J., Van Gucht, D.: Semi-determinism (extended abstract). In: Proceedings of the Eleventh ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, pp. 191–201. ACM Press, New York (1992)
Wang, Q.: Logical Foundations of Database Transformations for Complex-Value Databases. Logos Verlag, Berlin (2010)
Wang, Q., Schewe, K.-D.: Axiomatization of database transformations. In: Proceedings of the 14th International ASM Workshop (2007)
Wang, Q., Schewe, K.-D.: Towards a Logic for Abstract MetaFinite State Machines. In: Hartmann, S., Kern-Isberner, G. (eds.) FoIKS 2008. LNCS, vol. 4932, pp. 365–380. Springer, Heidelberg (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wang, Q. (2011). A Proof System with Bounded Non-determinism in Database Transformations. In: Schewe, KD., Thalheim, B. (eds) Semantics in Data and Knowledge Bases. SDKB 2010. Lecture Notes in Computer Science, vol 6834. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-23441-5_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-23441-5_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-23440-8
Online ISBN: 978-3-642-23441-5
eBook Packages: Computer ScienceComputer Science (R0)