Results on reasoning about updates in Transaction Logic

  • Anthony J. Bonner
  • Michael Kifer
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1472)


Transaction Logic was designed as a general logic of state change for deductive databases and logic programs. It has a model theory, a proof theory, and its Horn subset can be given a procedural interpretation. Previous work has demonstrated that the combination of declarative semantics and procedural interpretation turns the Horn subset of Transaction Logic into a powerful language for logic programming with updates [BK98,BK94,BK93,BK95]. In this paper, we focus not on the Horn subset, but on the full logic, and we explore its potential as a formalism for reasoning about logic programs with updates. We first develop a methodology for specifying properties of such programs, and then provide a sound inference system for reasoning about them, and conjecture a completeness result. Finally, we illustrate the power of the inference system through a series of examples of increasing difficulty.


Logic Program Minimal Model Inference Rule Logic Programming Classical Logic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [BK93]
    A.J. Bonner and M. Kifer. Transaction logic programming. In Intl. Conference on Logic Programming, pages 257–282, Budapest, Hungary, June 1993. MIT Press.Google Scholar
  2. [BK94]
    A.J. Bonner and M. Kifer. An overview of transaction logic. Theoretical Computer Science, 133:205–265, October 1994.zbMATHMathSciNetCrossRefGoogle Scholar
  3. [BK95]
    A.J. Bonner and M. Kifer. Transaction logic programming (or a logic of declarative and procedural knowledge). Technical Report CSRI-323, University of Toronto, November 1995. Scholar
  4. [BK96]
    A.J. Bonner and M. Kifer. Concurrency and communication in transaction logic. In Joint Intl. Conference and Symposium on Logic Programming, pages 142–156, Bonn, Germany, September 1996. MIT Press.Google Scholar
  5. [BK98]
    A.J. Bonner and M. Kifer. A logic for programming database transactions. In J. Chomicki and G. Saake, editors, Logics for Databases and Information Systems, chapter 5, pages 117–166. Kluwer Academic Publishers, March 1998.Google Scholar
  6. [Bon97a]
    A.J. Bonner. The power of cooperating transactions. Manuscript, 1997.Google Scholar
  7. [Bon97b]
    A.J. Bonner. Transaction Datalog: a compositional language for transaction programming. In Proceedings of the International Workshop on Database Programming Languages, Estes Park, Colorado, August 1997. Springer Verlag.Google Scholar
  8. [Cla78]
    K.L. Clark. Negation as failure. In H. Gallaire and J. Minker, editors, Logic and Data Bases, pages 292–322. Plenum Press, 1978.Google Scholar
  9. [DKRR98]
    H. Davulcu, M. Kifer, C.R. Ramakrishnan, and I.V. Ramakrishnan. Logic based modeling and analysis of workflows. In ACM Symposium on Principles of Database Systems, June 1998.Google Scholar
  10. [Har79]
    D. Harel. First-Order Dynamic Logic, volume 68 of Lecture Notes in Computer Science. Springer-Verlag, 1979.Google Scholar
  11. [Hun96]
    Samuel Y.K. Hung. Implementation and Performance of Transaction Logic in Prolog. Master's thesis, Department of Computer Science, University of Toronto, 1996. Scholar
  12. [Kif95]
    M. Kifer. Deductive and object-oriented data languages: A quest for integration. In Intl. Conference on Deductive and Object-Oriented Databases, volume 1013 of Lecture Notes in Computer Science, pages 187–212, Singapore, December 1995. Springer-Verlag. Keynote address at the 3d Intl. Conference on Deductive and Object-Oriented databases.Google Scholar
  13. [KLW95]
    M. Kifer, G. Lausen, and J. Wu. Logical foundations of object-oriented and frame-based languages. Journal of ACM, pages 741–843, July 1995.Google Scholar
  14. [McC63]
    J. McCarthy. Situations, actions, and clausal laws, memo 2. Stanford Artificial Intelligence Project, 1963.Google Scholar
  15. [MH69]
    J.M. McCarthy and P.J. Hayes. Some philosophical problems from the standpoint of artificial intelligence. In B. Meltzer and D. Michie, editors, Machine Intelligence, volume 4, pages 463–502. Edinburgh University Press, 1969. Reprinted in Readings in Artificial Intelligence, 1981, Tioga Publ. Co.Google Scholar
  16. [Pnu77]
    A. Pnueli. A temporal logic of programs. In Intl. Conference on Foundations of Computer Science, pages 46–57, October 1977.Google Scholar
  17. [Rei91]
    R. Reiter. The frame problem in the situation calculus: A simple solution (sometimes) and a completeness result for goal regression. In V. Lifschitz, editor, Aritifial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarty, pages 359–380. Academic Press, 1991.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Anthony J. Bonner
    • 1
  • Michael Kifer
    • 2
  1. 1.Department of Computer ScienceUniversity of TorontoTorontoCanada
  2. 2.Department of Computer ScienceSUNY at Stony BrookStony BrookUSA

Personalised recommendations