Maintaining State Constraints in Relational Databases: A Proof Theoretic Basis

William W. McCune, Lawrence Joseph Henschen

Research output: Contribution to journalArticle

43 Scopus citations

Abstract

If a relational database is required to satisfy a set of integrity constraints, then when the database is updated, one must ensure that it continues to satisfy the constraints. It is desirable not to have to evaluate each constraint after each update. A method is described that takes a constraint C and a class of updates, and either proves that an update in the class cannot violate C, or produces a formula C' 1989 that is satisfied before the update if and only if C would continue to be satisfied were the update to occur. C' is frequently much easier to evaluate than C. In addition, a formula D (a sufficient test) is sometimes produced such that if D is satisfied before the update, then C would continue to be satisfied were the update to occur. The method is proved correct. The method is substantially more general than other reported techniques for this problem. The method has been implemented, and a number of experiments with the implementation are presented.

Original languageEnglish (US)
Pages (from-to)46-68
Number of pages23
JournalJournal of the ACM (JACM)
Volume36
Issue number1
DOIs
StatePublished - Jan 1 1989

ASJC Scopus subject areas

  • Software
  • Control and Systems Engineering
  • Information Systems
  • Hardware and Architecture
  • Artificial Intelligence

Fingerprint Dive into the research topics of 'Maintaining State Constraints in Relational Databases: A Proof Theoretic Basis'. Together they form a unique fingerprint.

  • Cite this