Transaction logic provides a logical foundation for state changes and side effects in a logic programming language. A significant portion of this theory is implemented in FLORA-2. Applications of Transaction Logic include modeling and reasoning about workflows, planning, robotics, view maintenance in databases, and more.
Transaction Logic extends classical logic with one main connective, "sequential conjunction", which captures the concept of doing one action right after another. Transaction logic has a model theory and a sound and complete proof theory.
There is also an extension called "Concurrent Transaction Logic". An implementation of Concurrent Transaction Logic, can be found in http://www.cs.toronto.edu/~bonner/ctr/Home.html
Transaction Logic provides a completely logical account for production rules and database-style triggers.
Impact on Design
The model theory of Transaction Logic and its realization in FLORA-2 can serve as a guide for designing a logically sound production rules language.
For More Information
More information on Transaction Logic and Concurrent Transaction Logic can be found in
RIFWG contact: MichaelKifer.