oa Modeling datalog fact assertion and retraction in linear logic

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 traditional 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 work 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 do this specifically by explicitly representing the removal of facts and enriching our linear logic interpretation of Datalog inference rules with embedded retraction rules. These retraction rules are essentially linear implications designed to exercise the retraction of consequences when base facts are targeted for retraction. As such, we can map Datalog assertion and retraction onto the forward-chaining fragment of linear logic proof search. We formally prove the correctness of this interpretation with respect to its traditional counterpart. In the future, we intend to exploit our work here to develop a rich logic programming language that integrates Datalog style assertion and retraction with higher-order multiset rewritings.