Research Summary: Tabled Evaluation for Transaction Logic Programs

Abstract

In my thesis, I present problems and techniques in tabling Transaction Logic ($\mathcal{TR}$). $\mathcal{TR}$ is an extension of classical logic programming with backtrackable state updates and it has a top-down evaluation algorithm similar to Prolog’s SLD derivation extended with execution paths of states instead of a single global state. This backward chaining algorithm can be very inefficient by re-computing the same transactional queries more than once, or can enter into infinite loops by visiting the same paths of states an infinite number of times when computing answers to recursive programs. We solve these problems by memoizing (caching) the calls, call initial states, unifications (answers) and return states in a searchable structure for the Sequential Transaction Logic, respective building a graph for the query and tabling the nodes ready for current execution for the Concurrent Transaction Logic. Important problems of tabling $\mathcal{TR}$ are to store, index, update, query and resume states into memory. I implemented and measured the efficiency of multiple data structures used in tabling programs with backtrackable updates in XSB Prolog. My thesis studies the data structures and their performance for various applications of TR, such as, artificial intelligence planning, NP-complete graph algorithms (Hamiltonian cycle, clique, shortest consuming paths, connected components) and active databases. One of the most promising techniques was storing logs (i.e., inserts and deletes relative to a materialized state) into individual tries (optimized for querying), while keeping a global page trie as a common index for restarting.