COMPUTER SCIENCE QATAR TECHNICAL REPORT ABSTRACTS

Source: http://reports-archive.adm.cs.cmu.edu/anon/qatar/abstracts/12-113.html Parent: http://reports-archive.adm.cs.cmu.edu/qatar.html


	CMU-CS-QTR-113 Computer Science Qatar School of Computer Science, Carnegie Mellon University --- CMU-CS-QTR-113 Modeling Datalog Assertion and Retraction in Linear Logic Edmund S. L. Lam, Iliano Cervesato June 2012 CMU-CS-QTR-113.pdf Also appears as Computer Science Department Technical Report CMU-CS-12-126 Keywords: Datalog, Linear Logic, Retraction, Assertion, Dynamic updates 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. 29 pages *Carnegie Mellon University, Qatar Campus
--- Return to: SCS Technical Report Collection School of Computer Science This page maintained by reports@cs.cmu.edu

CMU-CS-QTR-113 Computer Science Qatar School of Computer Science, Carnegie Mellon University --- CMU-CS-QTR-113 Modeling Datalog Assertion and Retraction in Linear Logic Edmund S. L. Lam*, Iliano Cervesato* June 2012 CMU-CS-QTR-113.pdf Also appears as Computer Science Department Technical Report CMU-CS-12-126 Keywords: Datalog, Linear Logic, Retraction, Assertion, Dynamic updates 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. 29 pages *Carnegie Mellon University, Qatar Campus

--- Return to: SCS Technical Report Collection School of Computer Science This page maintained by reports@cs.cmu.edu