Efficient Tabling Mechanisms for Transaction Logic Programs
Paul Fodor

TL;DR
This paper introduces two optimized evaluation algorithms for Horn Transaction Logic, combining tabling and incremental evaluation techniques to improve performance in state-updating logic programs.
Contribution
It presents novel, complementary methods for efficient Transaction Logic evaluation, integrating tabling with state signatures and incremental updates based on inertia heuristics.
Findings
Tabling with state signatures improves repeated call efficiency.
Incremental evaluation reduces recomputation in state changes.
Combined methods enhance overall Transaction Logic performance.
Abstract
In this paper we present efficient evaluation algorithms for the Horn Transaction Logic (a generalization of the regular Horn logic programs with state updates). We present two complementary methods for optimizing the implementation of Transaction Logic. The first method is based on tabling and we modified the proof theory to table calls and answers on states (practically, equivalent to dynamic programming). The call-answer table is indexed on the call and a signature of the state in which the call was made. The answer columns contain the answer unification and a signature of the state after the call was executed. The states are signed efficiently using a technique based on tries and counting. The second method is based on incremental evaluation and it applies when the data oracle contains derived relations. The deletions and insertions (executed in the transaction oracle) change the…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, programming, and type systems · Advanced Software Engineering Methodologies
