Regular database update logics


Spruit, Paul and Wieringa, Roel and Meyer, John-Jules (2001) Regular database update logics. Theoretical Computer Science, 254 (1-2). pp. 591-661. ISSN 0304-3975

[img] PDF
Restricted to UT campus only
: Request a copy
Abstract:We study regular first-order update logic (FUL), which is a variant of regular dynamic logic in which updates to function symbols as well as to predicate symbols are possible. We fi1rst study FUL without making assumptions about atomic updates. Second, we look at relational algebra update logic (RAUL), which can be viewed as an extension of relational algebra with assignment. RAUL is an instantiation of FUL. Third, we study dynamic database logic (DDL), which is another version of FUL, in which the atomic updates can be "bulk updates" of predicates and updates of updateable functions. In all three cases, we define syntax, declarative semantics, axiomatizations, and operational semantics of the logic. All axiom systems are shown to be sound. Assuming the domain closure and unique naming assumptions, we also give a proof sketch of completeness of the axiomatization of DDL. The operational semantics presented in the paper are shown to be equivalent to the declarative semantics for certain classes of databases. We give examples of correctness proofs in RAUL and in DDL. Finally, we compare our approach to that of others and show how DDL can be used as a logic in which to specify and reason about updates to an object-oriented database system.
Item Type:Article
Copyright:© 2001 Elsevier Science B.V.
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:
Official URL:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page

Metis ID: 204982