Transaction Logic: An Introduction

The status of update operators in logic programming, such as assert and retract, has been a sore spot from the very inception of Prolog. Unlike much of the language, the update operators persistently defied the logical semantics, and their non-backtrackable nature was in stark contradiction with Prolog's operational semantics.

The result of this unsatisfactory state of affairs is that Prolog programs that rely on backtracking through assert and retract are notoriously hard to debug and maintain. This theoretical weakness becomes even more apparent when declarative programming tries to take a bite out of the object-oriented pie, where state-changing methods are commonplace.

Although it is not hard to hack up backtrackable updates in Prolog and the technique for doing so has been known for a long time, the logic behind this such updates remained unclear. Unclear, that is, until Transaction Logic came along.

Transaction Logic is a conservative extension of classical predicate calculus. It has a natural model theory, a sound and complete proof theory and, unlike many other logics, it allows users to program state-changing actions by combining simple actions into complex ones. The semantics of Transaction Logic leads naturally to features whose amalgamation in a single logic has proved elusive in the past. Apart from composable, "backtrackable updates," these features include non-deterministic actions, dynamic constraints on execution, tentative (non-committed) execution, concurrent and communicating processes, and more. Transaction Logic holds promise as a logical model of hitherto non-logical phenomena, including so-called procedural knowledge in AI, active databases, and the behavior of object-oriented databases, especially methods with side effects.

Some relevant papers

Tutorial slides