Automating proofs of integrity constraints in situation calculus

Leopoldo Bertossi, Javier Pinto, Pablo Saez, Deepak Kapur, Mahadevan Subramaniam

Research output: Chapter in Book/Report/Conference proceedingConference contribution

11 Citations (Scopus)

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.

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer Verlag
Pages212-222
Number of pages11
Volume1079
ISBN (Print)9783540612865
StatePublished - 1996
Externally publishedYes
Event9th International Symposium on Methodologies for Intelligent Systems, ISMIS 1996 - Zakopane, Poland
Duration: Jun 9 1996Jun 13 1996

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1079
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other9th International Symposium on Methodologies for Intelligent Systems, ISMIS 1996
CountryPoland
CityZakopane
Period6/9/966/13/96

Fingerprint

Integrity Constraints
Calculus
Quantifiers
Specifications
Proof by induction
Update
Semantics
Predicate
Express
Specification
Deductive Databases
Theorem
Proposition
Lemma
Intelligent databases

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Bertossi, L., Pinto, J., Saez, P., Kapur, D., & Subramaniam, M. (1996). Automating proofs of integrity constraints in situation calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1079, pp. 212-222). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1079). Springer Verlag.

Automating proofs of integrity constraints in situation calculus. / Bertossi, Leopoldo; Pinto, Javier; Saez, Pablo; Kapur, Deepak; Subramaniam, Mahadevan.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 1079 Springer Verlag, 1996. p. 212-222 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1079).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Bertossi, L, Pinto, J, Saez, P, Kapur, D & Subramaniam, M 1996, Automating proofs of integrity constraints in situation calculus. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 1079, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1079, Springer Verlag, pp. 212-222, 9th International Symposium on Methodologies for Intelligent Systems, ISMIS 1996, Zakopane, Poland, 6/9/96.
Bertossi L, Pinto J, Saez P, Kapur D, Subramaniam M. Automating proofs of integrity constraints in situation calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 1079. Springer Verlag. 1996. p. 212-222. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Bertossi, Leopoldo ; Pinto, Javier ; Saez, Pablo ; Kapur, Deepak ; Subramaniam, Mahadevan. / Automating proofs of integrity constraints in situation calculus. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 1079 Springer Verlag, 1996. pp. 212-222 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{5683dcb3b01b4b64920ceb75cca0dc24,
title = "Automating proofs of integrity constraints in situation calculus",
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.",
author = "Leopoldo Bertossi and Javier Pinto and Pablo Saez and Deepak Kapur and Mahadevan Subramaniam",
year = "1996",
language = "English (US)",
isbn = "9783540612865",
volume = "1079",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "212--222",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

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

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

M3 - Conference contribution

SN - 9783540612865

VL - 1079

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 212

EP - 222

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

PB - Springer Verlag

ER -