Transaction Logic: An Introduction

A tutorial presented at ILPS'97

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.

This tutorial is intended as an introduction to Transaction Logic, which will provide a glimpse into the model theory, the proof theory, and some of the applications of the logic.

Relevant links

Some relevant papers

More papers can be found at Transaction Logic homepage.

Tutorial slides

The PDF version of the slides is available here
Michael Kifer's homepage

visits since March 14, 1997.



Last modified: Sat Oct 18 15:53:48 EDT 1997