We provide a complete formalization of External Transaction Logic (or ET R), an extension of Transaction Logic to reason and execute external actions, i.e. actions performed on an external domain of which one has limited or no control; while interacting with an internal knowledge base compliant with ACID transactions. In such complex environment, if a failure occurs, it is no longer possible to simply rollback to the initial state prior to the execution of the transaction. Since rollbacking of external actions is unfeasible, as in databases, a relaxed transaction model can still be achieved by defining compensating operations that revert each of the external actions performed. To reason about external actions, we augment Transaction Logic’s theory with the ability to consult an external oracle, thereby allowing the abstraction from the theory and semantics of the external domain. In this paper we define the semantics of ET R, prove the equivalence to Transaction Logic when no external actions are defined, and construct a sound and complete SLD-style proof theory for a Horn-like subset of the logic. The solution obtained extends the semantics and proof theory of traditional Logic Programming both with the ability to perform ACID updates and to interact with an external domain.
|Journal||Theory And Practice Of Logic Programming|
|Publication status||Published - 1 Jan 2013|