We address the problem of formalizing the evolution of a database under the effect of an
arbitrary sequence of update transactions. We do so by appealing to a first order representation
language called the situation calculus, which is a standard approach in artificial intelligence to
the formalization of planning problems. We formalize database transactions in exactly the same
way as actions in the artificial intelligence planning domain. This leads to a database version
of the frame problem in artificial intelligence. We provide a solution to the frame problem
for a special, but substantial, class of update transactions. Using the axioms corresponding
to this solution, we provide procedures for determining whether a given sequence of update
transactions is legal, and for query evaluation in an updated database. These procedures have
the nice property that they appeal to theorem-proving only with respect to the initial database state.
We next address the problem of proving properties true in ali states of the database. It
turns out that mathematical induction is required for this task, and we formulate a number of
suitable induction principies. Among those properties of database states that we wish to prove
are the standard database -notions of static and dynamic integrity constraints. In our setting,
these emerge as inductive entailments of the database.
Finally, we discuss various possible extensions of the approach of this paper, including transaction
logs and historical queries, the complexity of query evaluation, actualized transactions,
logic programming approaches to updates, database views and state constraints.
