Transaction logic
Transaction Logic is an extension of predicate logic that accounts in a clean and declarative way for the phenomenon of state changes in logic programs and databases. This extension adds connectives specifically designed for combining simple actions into complex transactions and for providing control over their execution. The logic has a natural model theory and a sound and complete proof theory. Transaction Logic has a Horn clause subset, which has a procedural as well as a declarative semantics. The important features of the logic include hypothetical and committed updates, dynamic constraints on transaction execution, non-determinism, and bulk updates. In this way, Transaction Logic is able to declaratively capture a number of non-logical phenomena, including procedural knowledge in artificial intelligence, active databases, and methods with side effects in object databases. Transaction Logic was originally proposed in  by Anthony Bonner and Michael Kifer and later described in more detail in  and. The most comprehensive description appears in. In later years, Transaction Logic was extended in various ways, including concurrency, defeasible reasoning, partially defined actions, and other features. In 2013, the original paper on Transaction Logic  has won the 20-year Test of Time Award of the Association for Logic Programming as the most influential paper from the proceedings of ICLP 1993 conference in the preceding 20 years. Examples

Graph coloring 
Here  denotes the elementary update operation of transactional insert. The connective  is called serial conjunction. colorNode <-  // color one node correctly
    node(N) ⊗ ¬ colored(N,_) ⊗ color(C)
    ⊗ ¬(adjacent(N,N2) ∧ colored(N2,C))
    ⊗ tinsert(colored(N,C)). colorGraph <- ¬uncoloredNodesLeft. colorGraph <- colorNode ⊗ colorGraph. Pyramid stacking 
The elementary update  represents the transactional delete operation. stack(N,X) <- N>0 ⊗ move(Y,X) ⊗ stack(N-1,Y). stack(0,X). move(X,Y) <- pickup(X) ⊗ putdown(X,Y). pickup(X) <- clear(X) ⊗ on(X,Y) ⊗
             ⊗ tdelete(on(X,Y)) ⊗ tinsert(clear(Y)). putdown(X,Y) <-  wider(Y,X) ⊗ clear(Y) 
                 ⊗ tinsert(on(X,Y)) ⊗ tdelete(clear(Y)). Hypothetical execution 
Here  is the modal operator of possibility: If both  and  are possible, execute . Otherwise, if only  is possible, then execute it. execute <- <>action1 ⊗ <>action2 ⊗ action1. execute <- ¬<>action1 ⊗ <>action2 ⊗ action2. Dining philosophers 
Here  is the logical connective of parallel conjunction of Concurrent Transaction Logic. diningPhilosophers <- phil(1) | phil(2) | phil(3) | phil(4). Implementations 
A number of implementations of Transaction Logic exist:
 The original implementation. An implementation of Concurrent Transaction Logic. Transaction Logic enhanced with tabling. An implementation of Transaction Logic has also been incorporated as part of the Flora-2 knowledge representation and reasoning system. All these implementations are open source. References

External links 
 Flora-2 Web site, containing additional papers on Transaction Logic

Logic programming languages
Declarative programming languages
Knowledge representation