Declarative expression of deductive database updates
Saurav Manchanda · 1989
An update can be specified as a single database state transition, or as a sequence of queries and database state transitions. We give an extension of Datalog for expressing both types of update specifications on a logic database. The extension supports the simple and intuitive expression of basic update operations, hypothetical reasoning and update procedures. The extension possesses a possible-world semantics, and a sound and complete proof theory. Soundness and completeness is proved by showing that an update procedure can be mapped into a semantically equivalent Pure Prolog program. This means that the semantic and proof-theoretic results of Pure Prolog can be mapped into similar results for the Datalog extension.