Computer Science Qatar
School of Computer Science, Carnegie Mellon University
Modeling Datalog Assertion and Retraction
Edmund S. L. Lam*, Iliano Cervesato*
Also appears as Computer Science Department
Practical algorithms have been proposed to efficiently recompute the logical consequences of a Datalog program after a new fact has been asserted or retracted. This is essential in a dynamic setting where facts are frequently added and removed. Yet while assertion is logically well understood as incremental inference, the monotonic nature of first-order logic is ill-suited to model retraction. As such, the traditional logical interpretation of Datalog offers at most an abstract specification of Datalog systems, but has tenuous relations to the algorithms that perform efficient assertions and retractions in practical implementations. This report proposes a logical interpretation of Datalog based on linear logic. It not only captures the meaning of Datalog updates, but also provides an operational model that underlies the dynamic changes of the set of inferable facts, all within the confines of logic. We prove the correctness of this interpretation with respect to its traditional counterpart.