A proof system with bounded non-determinism in database transformations

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. Show more