TY - GEN
T1 - A proof system with bounded non-determinism in database transformations
AU - Wang, Qing
PY - 2011
Y1 - 2011
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=80052208625&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-23441-5_7
DO - 10.1007/978-3-642-23441-5_7
M3 - Conference contribution
AN - SCOPUS:80052208625
SN - 9783642234408
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 114
EP - 133
BT - Semantics in Data and Knowledge Bases - 4th International Workshop, SDKB 2010, Revised Selected Papers
T2 - 4th International Workshop on Semantics in Data and Knowledge Bases, SDKB 2010, Co-located with ICALP 2010
Y2 - 5 July 2010 through 5 July 2010
ER -