Regular database update logics

AbstractWe 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 first 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