Title
Maintaining state constraints in relational databases: a proof theoretic basis
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' (a complete test) 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.
Year
DOI
Venue
1989
10.1145/58562.59302
J. ACM
Keywords
DocType
Volume
additional key words and phrases: automated theorem proving,relational database,integrity constraints,formula D,proof theoretic basis,formula C,sufficient test,constraint C,relational databases,relational databases.,dependency statement,Maintaining state constraint,complete test,integrity constraint,first-order logic
Journal
36
Issue
ISSN
Citations 
1
0004-5411
41
PageRank 
References 
Authors
19.30
16
2
Name
Order
Citations
PageRank
William McCune115045.05
Lawrence J. Henschen2478280.94