{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,12]],"date-time":"2026-02-12T08:45:55Z","timestamp":1770885955558,"version":"3.50.1"},"reference-count":28,"publisher":"Elsevier","isbn-type":[{"value":"9780934613408","type":"print"}],"license":[{"start":{"date-parts":[[1988,1,1]],"date-time":"1988-01-01T00:00:00Z","timestamp":567993600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1988]]},"DOI":"10.1016\/b978-0-934613-40-8.50013-0","type":"book-chapter","created":{"date-parts":[[2014,7,1]],"date-time":"2014-07-01T16:04:11Z","timestamp":1404230651000},"page":"313-362","source":"Crossref","is-referenced-by-count":55,"title":["A Theorem-Proving Approach to Database Integrity"],"prefix":"10.1016","author":[{"given":"Fariba","family":"Sadri","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert","family":"Kowalski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/B978-0-934613-40-8.50013-0_bib1","unstructured":"Steps (1) and (2) above are extensions of steps (1) and (2) respectively in the description of SLDNF-derivation"},{"key":"10.1016\/B978-0-934613-40-8.50013-0_bib2","unstructured":"A selected condition \u201cNOT A\u201d can only be eliminated through the negation as failure rule. A selected conclusion \u201cNOT A,\u201d however, can only be eliminated through (extended) resolution with an input clause. In this simplified version of the proof procedure, only the top clause can have such a conclusion. Therefore, an extended resolution step can only be applied to obtain the second clause in a derivation from the top clause"},{"key":"10.1016\/B978-0-934613-40-8.50013-0_bib3","unstructured":"These metarules do not treat unification explicitly. The required unification steps would automatically be performed if the rules were executed by a Prolog-like system. Although this is common Prolog practice its logical status is problematic. These problems can be avoided by defining unification explicitly and by adding extra conditions to the metarules to compute the required mgu's and the resulting instantiated formulae, as is the case in the standard definition of provability (see Kowalski [1979], for example)"},{"key":"10.1016\/B978-0-934613-40-8.50013-0_bib4","unstructured":"The \u201cDemo\u201d and \u201cNOT Demo\u201d conditions in the metarules can be solved either by running metalevel definitions of \u201cDemo\u201d and \u201cNOT Demo\u201d or by using reflection as in FOL (Weyhrauch [1980]) or in amalgamation logic (Bowen and Kowalski [1982]). To solve \u201cDemo(D0 f)\u201d by reflection, we show that the goal named f can be solved by SLDNF in the database named D0. To solve \u201cNOT Demo(D f)\u201d by reflection we show that the goal named f fails finitely by SLDNF in the database named D"},{"key":"10.1016\/B978-0-934613-40-8.50013-0_bib5","unstructured":"The variables p in (MR1) and (MR2) and f in (MR4) are supposed to range over object level facts. These variables, however, do not always occur as arguments of metalevel predicates or functions in these rules. Thus, our metarules (MR1), (MR2), and (MR4) are not strictly well-formed (although, in practice, they work when using a Prolog-like execution mechanism). This problem can be avoided by replacing the occurrences of p in the first conditions of (MR1) and (MR2) and the occurrence of f in the conclusion of (MR4) by well-formed atoms Demo(D p) and Demo(D f). This, however, introduces other complications because it requires additional reflection rules and modifications to the extended resolution step"},{"key":"10.1016\/B978-0-934613-40-8.50013-0_bib6","unstructured":"Note that (MR1)\u2013(MR4), together with the standard and the extended resolution rules, cater for the propagation of the effects of initial additions and deletions through chains of database rules"},{"key":"10.1016\/B978-0-934613-40-8.50013-0_bib7","series-title":"Foundations of Deductive Databases and Logic Programming","first-page":"89","article-title":"Towards a Theory of Declarative Knowledge","author":"Apt","year":"1988"},{"key":"10.1016\/B978-0-934613-40-8.50013-0_bib8","series-title":"Logic Programming","first-page":"153","article-title":"Amalgamating Language and Metalanguage in Logic Programming","author":"Bowen","year":"1982"},{"key":"10.1016\/B978-0-934613-40-8.50013-0_bib9","series-title":"Symbolic Logic and Mechanical Theorem Proving","author":"Chang","year":"1973"},{"key":"10.1016\/B978-0-934613-40-8.50013-0_bib10","series-title":"Logic and Data Bases","first-page":"293","article-title":"Negation as Failure","author":"Clark","year":"1978"},{"key":"10.1016\/B978-0-934613-40-8.50013-0_bib11","unstructured":"Decker, H. [1986] Integrity Enforcement on Deductive Databases, Proc. EDS 86, Charleston, SC, 271\u2013285"},{"key":"10.1016\/B978-0-934613-40-8.50013-0_bib12","series-title":"The Range Form or How to Avoid Floundering","author":"Decker","year":"1987"},{"key":"10.1016\/B978-0-934613-40-8.50013-0_bib13","series-title":"USH-Resolution and Its Completeness","author":"Hill","year":"1974"},{"key":"10.1016\/B978-0-934613-40-8.50013-0_bib14","unstructured":"Jaffar, J., Lassez, J-L., and Lloyd, J. W. [1983] Completeness of the Negation as Failure Rule, IJCAI-83, Karlsruhe, 500\u2013506"},{"issue":"4","key":"10.1016\/B978-0-934613-40-8.50013-0_bib15","doi-asserted-by":"crossref","first-page":"572","DOI":"10.1145\/321906.321919","article-title":"A Proof Procedure Using Connection Graphs","volume":"22","author":"Kowalski","year":"1975","journal-title":"JACM"},{"key":"10.1016\/B978-0-934613-40-8.50013-0_bib16","series-title":"Logic for Problem Solving","author":"Kowalski","year":"1979"},{"key":"10.1016\/B978-0-934613-40-8.50013-0_bib17","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/0004-3702(71)90012-9","article-title":"Linear Resolution with Selection Function","volume":"2","author":"Kowalski","year":"1971","journal-title":"Artificial Intelligence"},{"key":"10.1016\/B978-0-934613-40-8.50013-0_bib18","unstructured":"Kowalski, R., Sadri, F., and Soper P. [1987] Integrity Checking in Deductive Databases, in Proc. 13th VLDB, Brighton, England, 61\u201369"},{"key":"10.1016\/B978-0-934613-40-8.50013-0_bib19","series-title":"Foundations of Logic Programming","author":"Lloyd","year":"1984"},{"key":"10.1016\/B978-0-934613-40-8.50013-0_bib20","series-title":"Integrity Constraint Checking in Stratified Databases","author":"Lloyd","year":"1986"},{"issue":"3","key":"10.1016\/B978-0-934613-40-8.50013-0_bib21","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1016\/0743-1066(84)90011-6","article-title":"Making Prolog More Expressive","volume":"1","author":"Lloyd","year":"1984","journal-title":"J. Logic Programming"},{"issue":"2","key":"10.1016\/B978-0-934613-40-8.50013-0_bib22","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1016\/0743-1066(85)90013-5","article-title":"A Basis for Deductive Database Systems","volume":"2","author":"Lloyd","year":"1985","journal-title":"J. Logic Programming"},{"issue":"1","key":"10.1016\/B978-0-934613-40-8.50013-0_bib23","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1016\/0743-1066(86)90004-X","article-title":"A Basis for Deductive Database Systems II","volume":"3","author":"Lloyd","year":"1986","journal-title":"J. Logic Programming"},{"issue":"3","key":"10.1016\/B978-0-934613-40-8.50013-0_bib24","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1007\/BF00263192","article-title":"Logic for Improving Integrity Checking in Relational Data Bases","volume":"18","author":"Nicolas","year":"1982","journal-title":"Acta Informatica"},{"key":"10.1016\/B978-0-934613-40-8.50013-0_bib25","unstructured":"Soper, P. J. R. [1986] Integrity Checking in Deductive Databases, M. Sc. thesis, Department of Computing, Imperial College, University of London"},{"key":"10.1016\/B978-0-934613-40-8.50013-0_bib26","series-title":"Deductive Database Tools","first-page":"3052","author":"Topor","year":"1985"},{"key":"10.1016\/B978-0-934613-40-8.50013-0_bib27","series-title":"Foundations of Deductive Databases and Logic Programming","first-page":"217","article-title":"On Domain Independent Databases","author":"Topor","year":"1988"},{"key":"10.1016\/B978-0-934613-40-8.50013-0_bib28","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/0004-3702(80)90015-6","article-title":"Prolegomena to a Theory of Mechanized Formal Reasoning","volume":"13","author":"Weyhrauch","year":"1980","journal-title":"Artificial Intelligence"}],"container-title":["Foundations of Deductive Databases and Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780934613408500130?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:B9780934613408500130?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2018,10,2]],"date-time":"2018-10-02T02:22:52Z","timestamp":1538446972000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/B9780934613408500130"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1988]]},"ISBN":["9780934613408"],"references-count":28,"URL":"https:\/\/doi.org\/10.1016\/b978-0-934613-40-8.50013-0","relation":{},"subject":[],"published":{"date-parts":[[1988]]}}}