© 1996 by Oxford University Press
Original Articles |
A Linear Logic Approach to Consistency Preserving Updates
1LIPN, URA 1507 CNRS, Université de Paris-Nord Villetaneuse, F-93430, France. E-mail: bidoit{at}ural507.univ-parisl3.fr
2LRI, URA 410 CNRS, Bat. 490, Université de Paris-Sud Orsay, F-91405, France. E-mail: serenachris{at}lri.fr
The aim of this paper is to propose linear logic as a proof system allowing one to perform updates of databases containing incomplete information. In our approach, a database is specified by facts, deduction rules (among which default rules) and update constraints. Updates will always preserve consistency, i.e. any update of a consistent database will produce a new base which is consistent. The computation of the static semantics of a database DB corresponds to the construction of a proof in a logical theory associated to the database; the non logical axioms of such a theory are linear sequents formalising the deduction rules and the update constraints of DB. Similarly, the calculus of the update semantics of a database DB w.r.t. the insertion of a literal L, is the construction of a proof in the very same linear theory.
Keywords: Deductive databases; incomplete information; linear logic; updates