A New Approach to Inferences of Semantic Constraints.

Joachim Biskup, Andreas Kluck: A New Approach to Inferences of Semantic Constraints. ADBIS 1997: 72-79
  author    = {Joachim Biskup and
               Andreas Kluck},
  title     = {A New Approach to Inferences of Semantic Constraints},
  booktitle = {Proceedings of the First East-European Symposium on Advances
               in Databases and Information Systems (ADBIS'97), St.-Petersburg,
               September 2-5, 1997. Volume 1: Regular Papers},
  publisher = {Nevsky Dialect},
  year      = {1997},
  pages     = {72-79},
  ee        = {db/conf/adbis/BiskupK97.html},
  crossref  = {DBLP:conf/adbis/97},
  bibsource = {DBLP,}


Chase procedures are well-known decision and semi-decision procedures for the implication problem among dependencies, a specific type of first-order logic formulas, that are used for expressing database constraints. Of course, the implication problem can also be treated by general refutationally complete inference systems, like resolution with paramodulation. Recently the inference rule of basic paramodulation has been introduced and investigated as a strategy for exploring the search space for a refutation most efficiently. This paper demonstrates that chase procedures can be seen as special instances of basic paramodulation by defining the parameters of basic paramodulation, a reduction ordering and a term selection function, appropriately. The mutual simulation of chase procedures and basic paramodulation also extends to the completeness proofs.

Copyright © 1997 by the ACM, Inc., used by permission. Permission to make digital or hard copies is granted provided that copies are not made or distributed for profit or direct commercial advantage, and that copies show this notice on the first page or initial screen of a display along with the full citation.

ACM SIGMOD Anthology

CDROM Version: Load the CDROM "Volume 2 Issue 5, SSDBM, DBPL, KRDB, ADBIS, COOPIS, SIGBDP" and ... DVD Version: Load ACM SIGMOD Anthology DVD 1" and ... BibTeX


Serge Abiteboul, Richard Hull, Victor Vianu: Foundations of Databases. Addison-Wesley 1995, ISBN 0-201-53771-0
Contents BibTeX
Alfred V. Aho, Catriel Beeri, Jeffrey D. Ullman: The Theory of Joins in Relational Databases. ACM Trans. Database Syst. 4(3): 297-314(1979) BibTeX
Paolo Atzeni, Valeria De Antonellis: Relational Database Theory. Benjamin/Cummings 1993, ISBN 0-8053-0249-2
Leo Bachmair, Harald Ganzinger: Rewrite-Based Equational Theorem Proving with Selection and Simplification. J. Log. Comput. 4(3): 217-247(1994) BibTeX
Leo Bachmair, Harald Ganzinger, Christopher Lynch, Wayne Snyder: Basic Paramodulation and Superposition. CADE 1992: 462-476 BibTeX
Leo Bachmair, Harald Ganzinger, Christopher Lynch, Wayne Snyder: Basic Paramodulation. Inf. Comput. 121(2): 172-192(1995) BibTeX
Catriel Beeri, Moshe Y. Vardi: The Implication Problem for Data Dependencies. ICALP 1981: 73-85 BibTeX
Catriel Beeri, Moshe Y. Vardi: A Proof Procedure for Data Dependencies. J. ACM 31(4): 718-741(1984) BibTeX
Ronald Fagin: Horn clauses and database dependencies. J. ACM 29(4): 952-985(1982) BibTeX
John Grant, Barry E. Jacobs: On the family of generalized dependency constraints. J. ACM 29(4): 986-997(1982) BibTeX
Jean-Marie Hullot: Canonical Forms and Unification. CADE 1980: 318-334 BibTeX
Anthony C. Klug, Rod Price: Determining View Dependencies Using Tableaux. ACM Trans. Database Syst. 7(3): 361-380(1982) BibTeX
John W. Lloyd: Foundations of Logic Programming, 2nd Edition. Springer 1987, ISBN 3-540-18199-7
David Maier, Alberto O. Mendelzon, Yehoshua Sagiv: Testing Implications of Data Dependencies. ACM Trans. Database Syst. 4(4): 455-469(1979) BibTeX
Robert Nieuwenhuis, Albert Rubio: Theorem Proving with Ordering and Equality Constrained Clauses. J. Symb. Comput. 19(4): 321-351(1995) BibTeX
John Alan Robinson: A Machine-Oriented Logic Based on the Resolution Principle. J. ACM 12(1): 23-41(1965) BibTeX
Fereidoon Sadri, Jeffrey D. Ullman: The Theory of Functional and Template Dependencies. Theor. Comput. Sci. 17: 317-331(1982) BibTeX
Mihalis Yannakakis, Christos H. Papadimitriou: Algebraic Dependencies. J. Comput. Syst. Sci. 25(1): 2-41(1982) BibTeX
ACM SIGMOD Anthology - DBLP: [Home | Search: Author, Title | Conferences | Journals]
ACM SIGMOD Anthology: Copyright © by ACM (, Corrections:
DBLP: Copyright © by Michael Ley (, last change: Sat May 16 22:56:30 2009