Theorem Proving Techniques for View Deletion in Databases

In this paper, we show how techniques from first-order theorem proving can be used for efficient deductive database updates. The key idea is to transform the given database, together with the update request, into a (disjunctive) logic program and to apply the hyper-tableau calculus (Baumgartner et al. 1996) to solve the original update problem. The resulting algorithm has the following properties: it works goal-directed (i.e. the search is driven by the update request), it is rational in the sense that it satisfies certain rationality postulates stemming from philosophical works on belief dynamics, and, unlike comparable approaches, it is of polynomial space complexity. To obtain soundness and completeness results, the hyper-tableau calculus is slightly modified for minimal model reasoning. Besides a direct proof we give an alternate proof which gives insights into the relation to previous approaches. As a by-product we thereby derive a soundness and completeness result of hyper-tableaux for computing minimal abductive explanations.