Axiomatization, Declarative Semantics and Operational Semantics of Passive and Active Updates in Logic Databases

摘要

The use of logic in database theory is commonly restricted to the specification of database states. Reasoning about state changes (the database updates) must then be done outside the logic. In this report, we consider a logic that also takes the updates into account. Taking propostional dynamic logic as a starting point, we define PDDL: prepositional dynamic database logic. The main features of PDDL are:•There are two kinds of atomic updates in PDDL, passive and active updates. Passive updates just change the truth value of an atom to true/false and active updates set one atom to true/false and then compute derived updates using a logic program. Just like the atomic actions of dynamic logic, the atomic updates can be combined into update programs with the operators sequential composition, choice and iteration. We have one more update action (also present in dynamic logic): the test of a formula.•The declarative semantics for formulas and updates, is based on Kripke structures. Because of the specific language of updates, we have many properties of the semantics that are not present in propositional dynamic logic (PDL). One of these properties is that we can identify worlds with the same valuation in a structure, the resulting structure is called normalized, and it is equivalent to the original structure.•We have a proof system for PDDL which is soundand complete for the class of‘full’structures. For non-full structures, the main problem is the axiomatization of successor worlds. For the most interesting class of (non-full) structures given some set of constraints, we give a reduction of the non-full case to the full case.•We have a Plotkin-style operational semantics for update programs. The operational semantics allows us to compute the result of executing an update in some database state. A database state is a set of (propositional) formulas and specifies some subset of the worlds in a structure (the worlds in whichs the database state is true). The operational and declarative semantics are shown to be