Transaction Logic is an extension of
predicate logic
First-order logic, also called predicate logic, predicate calculus, or quantificational logic, is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables ove ...
that accounts in a clean and declarative way for the phenomenon of state changes in
logic programs and
database
In computing, a database is an organized collection of data or a type of data store based on the use of a database management system (DBMS), the software that interacts with end users, applications, and the database itself to capture and a ...
s. 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
In mathematical logic, model theory is the study of the relationship between theory (mathematical logic), formal theories (a collection of Sentence (mathematical logic), sentences in a formal language expressing statements about a Structure (mat ...
and a sound and complete
proof theory
Proof theory is a major branchAccording to , proof theory is one of four domains mathematical logic, together with model theory, axiomatic set theory, and recursion theory. consists of four corresponding parts, with part D being about "Proof The ...
. Transaction Logic has a
Horn clause
In mathematical logic and logic programming, a Horn clause is a logical formula of a particular rule-like form that gives it useful properties for use in logic programming, formal specification, universal algebra and model theory. Horn clauses are ...
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
Procedural knowledge (also known as know-how, knowing-how, and sometimes referred to as practical knowledge, imperative knowledge, or performative knowledge) is the knowledge exercised in the performance of some task. Unlike descriptive knowledge ...
in
artificial intelligence
Artificial intelligence (AI) is the capability of computer, computational systems to perform tasks typically associated with human intelligence, such as learning, reasoning, problem-solving, perception, and decision-making. It is a field of re ...
,
active databases, and methods with side effects in
object database
An object database or object-oriented database is a database management system in which information is represented in the form of objects as used in object-oriented programming. Object databases are different from relational databases which are ...
s.
Transaction Logic was originally proposed in 1993 b
Anthony Bonneran
Michael Kiferref name="tr-iclp1993">A.J. Bonner and M. Kifer (1993), ''Transaction Logic Programming'', International Conference on Logic Programming (ICLP), 1993. and later described in more detail in ''An Overview of Transaction Logic'' and ''Logic Programming for Database Transactions''. The most comprehensive description appears in Bonner & Kifer's technical report from 1995.
In later years, Transaction Logic was extended in various ways, including
concurrency,
[A.J. Bonner and M. Kifer (1996)]
''Concurrency and communication in Transaction Logic''
Joint Intl. Conference and Symposium on Logic Programming, Bonn, Germany, September 1996 defeasible reasoning
In philosophy of logic, defeasible reasoning is a kind of provisional reasoning that is rationally compelling, though not deductively valid. It usually occurs when a rule is given, but there may be specific exceptions to the rule, or subclasse ...
, partially defined actions, and other features.
In 2013, the original paper on Transaction Logic ha
wonth
20-year Test of Time Awardof the
Association for Logic Programming as the most influential paper from the proceedings o
ICLP 1993 conferencein 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 Flora-2 is an open source semantic rule-based system for knowledge representation and reasoning.
The language of the system is derived from F-logic, HiLog,
W. Chen, M. Kifer and D.S. Warren (1993)''HiLog: A Foundation for Higher-Order Logic Program ...
knowledge representation and reasoning system.
All these implementations are
open source
Open source is source code that is made freely available for possible modification and redistribution. Products include permission to use and view the source code, design documents, or content of the product. The open source model is a decentrali ...
.
References
{{Reflist
External links
Flora-2 Web site containing additional papers on Transaction Logic
Logic programming languages
Declarative programming languages
Knowledge representation