Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
L. Bertossi and J. Ferretti. SCDBR: A Reasoner for Specifications in the Situation Calculus of Database Updates. In Temporal Logic. Proc. First Intl. Conf. ICTL '94, Bonn, Germany, July 1994, LNAI 827, 543–545, Springer.
L. Bertossi, J. Pinto, P. Saez, D. Kapur, and M. Subramaniam. Automated Proofs of Integrity Constraints in Situation Calculus. Technical Report, Computer Science Dept., SUNY, Albany, Nov. 1995.
R.S. Boyer and J S. Moore. A Computational Logic Handbook. AP, 1988.
R.S. Boyer and J. S. Moore. The Addition of Bounded Quantification and Partial Functions to A Computational Logic and Its Theorem Prover. Journal of Automated Reasoning, 4:117–172, 1988.
D. Kapur. Constructors can be Partial too. Dept. of Computer Science, State University of New York at Albany, 1994.
D. Kapur and H. Zhang. An Overview of Rewrite Rule Laboratory (RRL). J. of Computer and Mathematics with Applications, 1995.
J. McCarthy and P. Hayes. Some Philosophical Problems from the Standpoint of Artificial Intelligence. In B. Meltzer and D. Michie, eds, Machine Intelligence, vol. 4, 463–502, Edinburgh, Scotland, 1969. Edinburgh University Press.
R. Reiter. Towards a Logical Reconstruction of Relational Databases Theory. In J. Mylopoulos and J. Schmidt, eds, On Conceptual Modeling: Perspectives from AI, Databases and Programming Languages, 191–233. Springer-Verlag, 1984.
R. Reiter. The Frame Problem in the Situation Calculus: a Simple Solution (sometimes) and a Completeness Result for Goal Regression. In V. Lifschitz, ed, Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, 359–380. Academic Press, 1991.
R. Reiter. Formalizing Database Evolution in the Situation Calculus. In Proceedings of the Fifth Generation Computer Systems, Tokyo, Japan, June 1992.
R. Reiter. On Specifying Database Updates. Technical Report KRR-TR-92-3, University of Toronto, Department of Computer Science, Toronto, Canada, 1992.
R. Reiter. Proving Properties of States in the Situation Calculus. Artificial Intelligence, 64(2):337–351, 1993.
T. Sheard and D. Stemple. Automatic Verification of Database Transaction Safety. TR 88-29, Dept. Computer and Information Science, U. Mass., Amherst, MA, 1988.
H. Zhang and D. Kapur. First-Order Theorem Proving using Conditional Rewrite Rules. In Lusk and Overbeek, eds., Proc. 9th Intl. Conf. on Automated Deduction (CADE-9), LNCS 310, 1–20. Springer, 1988.
H. Zhang, D. Kapur, and M.S. Krishnamoorthy. A Mechanizable Induction Principle for Equational Specifications. In Lusk and Overbeek, eds, Proc. 9th Intl. Conf. on Automated Deduction (CADE-9), LNCS 310, 162–181. Springer, 1988.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bertossi, L., Pinto, J., Saez, P., Kapur, D., Subramaniam, M. (1996). Automating proofs of integrity constraints in situation calculus. In: Raś, Z.W., Michalewicz, M. (eds) Foundations of Intelligent Systems. ISMIS 1996. Lecture Notes in Computer Science, vol 1079. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61286-6_146
Download citation
DOI: https://doi.org/10.1007/3-540-61286-6_146
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61286-5
Online ISBN: 978-3-540-68440-4
eBook Packages: Springer Book Archive