Optimizations and Extensions for the Horn Transaction Logic Programs

Abstract

My thesis describes optimization techniques and extensions for the Horn Transaction Logic. The Horn Transaction Logic is an extension of the classical logic programming with state updates and it has a SLD-style evaluation algorithm. This SLD-style algorithm enters into infinite loops when computing answers to many recursive programs when they change the underlying state of the knowledge base. We solve this problem by tabling the calls, states and answers in a searchable structure, so that the same call is not re-executed ad infinitum. With these techniques, we can efficiently compute queries to transaction logic programs, and when the underlying programs have the bounded term-depth property, these techniques are guaranteed to terminate. I also present extensions to Transaction Logic, for instance a definite semantics for the existentially quantified values that occur in facts, queries and updates of facts. The applications of these techniques promise great improvements in the uses of transaction logic: state-changing systems, artificial intelligence planning, dynamic constraints on transaction execution, workflow modeling and verification, and systems involving financial transactions.