TY - GEN
T1 - Automating proofs of integrity constraints in situation calculus
AU - Bertossi, Leopoldo
AU - Pinto, Javier
AU - Saez, Pablo
AU - Kapur, Deepak
AU - Subramaniam, Mahadevan
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 1996.
PY - 1996
Y1 - 1996
N2 - Automated support for proving integrity constraints (ICs) on deductive database update specifications is developed using an induction theorem prover, Rewrite Rule Laboratory (RRL) [6]. The approach proposed by Reiter [9, 11,-10] for solving the frame problem for such applications in a language of the situation calculus is used as a basic framework. Integrity constraints are propositions that are expected to be true in every accessible state of a database, and they should be provable from the specification of the evolution of the database. Accessible states are defined by induction [12] as those reachable from the initial state by update actions whose execution is possible. Induction theorem provers can only reason about quantifier-free formulas (i.e., universally quantified formulas) whereas in order to express integrity constraints, quantifiers may be used. It is shown that by making use of the fact that in relational data base.applications, domain of objects under consideration is finite, such ICs expressed using quantifiers can be mechanically translated into quantifier-free formulas by introducing new predicates and by explicitly building domains of objects involved in updates. Bridge lemmas connecting the semantics of the new predicates to the fluents used to express integrity constraints can be mechanically generated and automatically proved in RRL. An interesting feature of the proposed approach is that mechanically generated proofs of integrity constraints have a structure similar to manually-generated proofs.
AB - Automated support for proving integrity constraints (ICs) on deductive database update specifications is developed using an induction theorem prover, Rewrite Rule Laboratory (RRL) [6]. The approach proposed by Reiter [9, 11,-10] for solving the frame problem for such applications in a language of the situation calculus is used as a basic framework. Integrity constraints are propositions that are expected to be true in every accessible state of a database, and they should be provable from the specification of the evolution of the database. Accessible states are defined by induction [12] as those reachable from the initial state by update actions whose execution is possible. Induction theorem provers can only reason about quantifier-free formulas (i.e., universally quantified formulas) whereas in order to express integrity constraints, quantifiers may be used. It is shown that by making use of the fact that in relational data base.applications, domain of objects under consideration is finite, such ICs expressed using quantifiers can be mechanically translated into quantifier-free formulas by introducing new predicates and by explicitly building domains of objects involved in updates. Bridge lemmas connecting the semantics of the new predicates to the fluents used to express integrity constraints can be mechanically generated and automatically proved in RRL. An interesting feature of the proposed approach is that mechanically generated proofs of integrity constraints have a structure similar to manually-generated proofs.
UR - http://www.scopus.com/inward/record.url?scp=84949806797&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84949806797&partnerID=8YFLogxK
U2 - 10.1007/3-540-61286-6_146
DO - 10.1007/3-540-61286-6_146
M3 - Conference contribution
AN - SCOPUS:84949806797
SN - 9783540612865
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 212
EP - 222
BT - Foundations of Intelligent Systems - 9th International Symposium, ISMIS 1996, Proceedings
A2 - Ras, Zbigniew W.
A2 - Michalewicz, Maciek
PB - Springer Verlag
T2 - 9th International Symposium on Methodologies for Intelligent Systems, ISMIS 1996
Y2 - 9 June 1996 through 13 June 1996
ER -