Transaction logic

<h2 id="examples">Examples</h2>
<h3>Graph coloring</h3>
<p>Here tinsert denotes the elementary update operation of <i>transactional insert</i>. The connective ⊗ is called <i>serial conjunction</i>.
</p>
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.

<h3>Pyramid stacking</h3>
<p>The elementary update tdelete represents the <i>transactional delete</i> operation.
</p>
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)).

<h3>Hypothetical execution</h3>
<p>Here <> is the modal operator of possibility: If both action1 and action2 are possible, execute action1. Otherwise, if only action2 is possible, then execute it.
</p>
execute <- <>action1 ⊗ <>action2 ⊗ action1.
execute <- ¬<>action1 ⊗ <>action2 ⊗ action2.

<h3>Dining philosophers</h3>
<p>Here | is the logical connective of parallel conjunction of Concurrent Transaction Logic.<a class="footnote-ref" id="fnref:10" href="#fn:10"><sup>10</sup></a>
</p>
diningPhilosophers <- phil(1) | phil(2) | phil(3) | phil(4).

<h2 id="implementations">Implementations</h2>
<p>A number of implementations of Transaction Logic exist:
</p>
<ul><li>The original implementation.<a class="footnote-ref" id="fnref:11" href="#fn:11"><sup>11</sup></a></li>
<li>An implementation of Concurrent Transaction Logic.<a class="footnote-ref" id="fnref:12" href="#fn:12"><sup>12</sup></a></li>
<li>Transaction Logic enhanced with <a href="/facts/Tabling/u08VhUKm">tabling</a>. An implementation of Transaction Logic has also been incorporated as part of the <a href="/facts/Flora-2/Snejq0mx">Flora-2</a> knowledge representation and reasoning system.<a class="footnote-ref" id="fnref:13" href="#fn:13"><sup>13</sup></a></li></ul>
<p>All these implementations are <a href="/facts/Open_source/7X9rCdz4">open source</a>.
</p>

<h2 id="external-links">External links</h2>
<ul><li><a href="http://flora.sourceforge.net">Flora-2 Web site</a>, containing additional papers on Transaction Logic</li></ul>

<h2 id="references">References</h2>

<ol>
<li id="fn:1"><p>A.J. Bonner and M. Kifer (1993), Transaction Logic Programming, International Conference on Logic Programming (ICLP), 1993. <a href="#fnref:1" class="footnote-back-ref">↩</a></p></li>
<li id="fn:2"><p>A.J. Bonner and M. Kifer (1994), An Overview of Transaction Logic, Theoretical Computer Science, 133:2, 1994. <a href="#fnref:2" class="footnote-back-ref">↩</a></p></li>
<li id="fn:3"><p>A.J. Bonner and M. Kifer (1998), Logic Programming for Database Transactions in Logics for Databases and Information Systems, J. Chomicki and G. Saake (eds.), Kluwer Academic Publ., 1998. <a href="http://www.cs.sunysb.edu/~kifer/TechReports/tr-chomicki.pdf" target="_blank">http://www.cs.sunysb.edu/~kifer/TechReports/tr-chomicki.pdf</a> <a href="#fnref:3" class="footnote-back-ref">↩</a></p></li>
<li id="fn:4"><p>A.J. Bonner and M. Kifer (1995), Transaction Logic Programming (or A Logic of Declarative and Procedural Knowledge). Technical Report CSRI-323, November 1995, Computer Science Research Institute, University of Toronto. <a href="http://www.cs.sunysb.edu/~kifer/TechReports/transaction-logic.pdf" target="_blank">http://www.cs.sunysb.edu/~kifer/TechReports/transaction-logic.pdf</a> <a href="#fnref:4" class="footnote-back-ref">↩</a></p></li>
<li id="fn:5"><p>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 <a href="http://www.cs.sunysb.edu/~kifer/TechReports/concurrent-trans-logic.pdf" target="_blank">http://www.cs.sunysb.edu/~kifer/TechReports/concurrent-trans-logic.pdf</a> <a href="#fnref:5" class="footnote-back-ref">↩</a></p></li>
<li id="fn:6"><p>P. Fodor and M. Kifer (2011), Transaction Logic with Defaults and Argumentation Theories. In Technical communications of the 27th International Conference on Logic Programming (ICLP), July 2011. <a href="http://drops.dagstuhl.de/opus/volltexte/2011/3159/" target="_blank">http://drops.dagstuhl.de/opus/volltexte/2011/3159/</a> <a href="#fnref:6" class="footnote-back-ref">↩</a></p></li>
<li id="fn:7"><p>M. Rezk and M. Kifer (2012), Transaction Logic with Partially Defined Actions. Journal on Data Semantics, August 2012, vol. 1, no. 2, Springer. <a href="https://link.springer.com/article/10.1007%2Fs13740-012-0007-8" target="_blank">https://link.springer.com/article/10.1007%2Fs13740-012-0007-8</a> <a href="#fnref:7" class="footnote-back-ref">↩</a></p></li>
<li id="fn:8"><p>H. Davulcu, M. Kifer and I.V. Ramakrishnan (2004), CTR-S: A Logic for Specifying Contracts in Semantic Web Services. Proceedings of the 13-th World Wide Web Conference (WWW2004), May 2004. <a href="http://www.www2004.org/proceedings/docs/2p144.pdf" target="_blank">http://www.www2004.org/proceedings/docs/2p144.pdf</a> <a href="#fnref:8" class="footnote-back-ref">↩</a></p></li>
<li id="fn:9"><p>P. Fodor and M. Kifer (2010), Tabling for Transaction Logic. In Proceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming (PPDP), July 2010. <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.184.6968" target="_blank">http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.184.6968</a> <a href="#fnref:9" class="footnote-back-ref">↩</a></p></li>
<li id="fn:10"><p>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 <a href="http://www.cs.sunysb.edu/~kifer/TechReports/concurrent-trans-logic.pdf" target="_blank">http://www.cs.sunysb.edu/~kifer/TechReports/concurrent-trans-logic.pdf</a> <a href="#fnref:10" class="footnote-back-ref">↩</a></p></li>
<li id="fn:11"><p>Hung, Samuel (1996). "Transaction Logic Prototype". University of Toronto, Department of Computer Science. Retrieved 2021-05-10. <a href="http://www.cs.toronto.edu/~bonner/transaction-logic.html" target="_blank">http://www.cs.toronto.edu/~bonner/transaction-logic.html</a> <a href="#fnref:11" class="footnote-back-ref">↩</a></p></li>
<li id="fn:12"><p>Sleghel, Amalia F. (2000). "Concurrent Transaction Logic Prototype". University of Toronto, Department of Computer Science. Retrieved 2021-05-10. <a href="http://www.cs.toronto.edu/~bonner/ctr/index.html" target="_blank">http://www.cs.toronto.edu/~bonner/ctr/index.html</a> <a href="#fnref:12" class="footnote-back-ref">↩</a></p></li>
<li id="fn:13"><p>"Knowledge Representation & Reasoning with Flora-2". Sourceforge.net. Retrieved 2021-05-10. <a href="http://flora.sourceforge.net" target="_blank">http://flora.sourceforge.net</a> <a href="#fnref:13" class="footnote-back-ref">↩</a></p></li>
</ol>

Transaction logic open-in-new

Transaction logic