{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,15]],"date-time":"2026-01-15T02:08:54Z","timestamp":1768442934142,"version":"3.49.0"},"reference-count":57,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[1993,9,1]],"date-time":"1993-09-01T00:00:00Z","timestamp":746841600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":7259,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[1993,9]]},"DOI":"10.1016\/0304-3975(93)90107-5","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T23:47:37Z","timestamp":1027640857000},"page":"99-166","source":"Crossref","is-referenced-by-count":33,"title":["Proof methods of declarative properties of definite programs"],"prefix":"10.1016","volume":"118","author":[{"given":"Pierre","family":"Deransart","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/0304-3975(93)90107-5_BIB1","series-title":"Tech. Report 90-26-2","article-title":"Axiomatic verification of logic programs","author":"Antoy","year":"1991"},{"key":"10.1016\/0304-3975(93)90107-5_BIB2","series-title":"Tech. Report 87-35","article-title":"Introduction to logic programming","author":"Apt","year":"1987"},{"key":"10.1016\/0304-3975(93)90107-5_BIB3","series-title":"Proc. Compulog Meeting","first-page":"150","article-title":"Studies in pure prolog: termination in computational logic","year":"1990"},{"key":"10.1016\/0304-3975(93)90107-5_BIB4","doi-asserted-by":"crossref","first-page":"841","DOI":"10.1145\/322326.322339","article-title":"Contributions to the theory of logic programming","volume":"29","author":"Apt","year":"1982","journal-title":"J. ACM"},{"key":"10.1016\/0304-3975(93)90107-5_BIB5","article-title":"On an interactive program verifier of PROLOG programs","volume":"26","author":"Balogh","year":"1978"},{"key":"10.1016\/0304-3975(93)90107-5_BIB6","series-title":"Proc. PLILP '88","first-page":"58","article-title":"A tool to check the non-floundering of logic programs and goals","volume":"Vol. 348","author":"Barbutti","year":"1958"},{"key":"10.1016\/0304-3975(93)90107-5_BIB7","article-title":"Proving termination properties of PROLOG programs: a semantic approach","author":"Baudinet","year":"1988","journal-title":"Report STAN-CS 88-1202"},{"key":"10.1016\/0304-3975(93)90107-5_BIB8","series-title":"Ph.D. Dissertation","article-title":"A method of presentation of the abstract data types: applications","author":"Bidoit","year":"1981"},{"key":"10.1016\/0304-3975(93)90107-5_BIB9","series-title":"Proc. Tapsoft '89","first-page":"96","article-title":"Verifying correctness of logic programs","volume":"Vol. 352","author":"Bossi","year":"1989"},{"key":"10.1016\/0304-3975(93)90107-5_BIB10","first-page":"192","article-title":"Abstract interpretation: the global optimization of PROLOG programs","author":"Bruynooghe","year":"1987","journal-title":"Proc. SLP '87"},{"key":"10.1016\/0304-3975(93)90107-5_BIB11","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1145\/800027.808470","article-title":"Some transformations for developing recursive programs","author":"Burstall","year":"1975","journal-title":"Proc. Int. Conf. on Reliable Software"},{"key":"10.1016\/0304-3975(93)90107-5_BIB12","series-title":"Res. Mon. 79\/59 TOC","article-title":"Predicate logic as a computational formalism","author":"Clark","year":"1979"},{"key":"10.1016\/0304-3975(93)90107-5_BIB13","series-title":"Proc. IFIP '77","first-page":"939","article-title":"A first order theory on data and programs","author":"Clark","year":"1977"},{"key":"10.1016\/0304-3975(93)90107-5_BIB14","series-title":"Proc. ICLP '91","first-page":"629","article-title":"The axiomatic semantics of logic programs","author":"Colussi","year":"1991"},{"key":"10.1016\/0304-3975(93)90107-5_BIB15","article-title":"Equational problems and disunification","author":"Comon","year":"1988","journal-title":"INRIA RR 904"},{"key":"10.1016\/0304-3975(93)90107-5_BIB16","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1137\/0207005","article-title":"Soundness and completeness of an axiom system for programs verification","volume":"7","author":"Cook","year":"1978","journal-title":"SIAM J. Comput."},{"key":"10.1016\/0304-3975(93)90107-5_BIB17","series-title":"Methods and Tools for Compiler Construction, CEC-INRIA Course","article-title":"Attribute grammars: definitions, analysis of dependencies, proof methods","author":"Courcelle","year":"1984"},{"key":"10.1016\/0304-3975(93)90107-5_BIB18","doi-asserted-by":"crossref","DOI":"10.1016\/0890-5401(88)90002-8","article-title":"Proof of partial correctness for attribute grammars with application to recursive procedure and logic programming","volume":"78","author":"Courcelle","year":"1988","journal-title":"Informat. and Comput."},{"key":"10.1016\/0304-3975(93)90107-5_BIB19","first-page":"463","article-title":"Logical attribute grammars","volume":"Vol. 83","author":"Deransart","year":"1983"},{"key":"10.1016\/0304-3975(93)90107-5_BIB20","first-page":"207","article-title":"Proofs of declarative properties of logic programs","volume":"Vol. 352","author":"Deransart","year":"1989"},{"key":"10.1016\/0304-3975(93)90107-5_BIB21","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/BF03037477","article-title":"An operational formal description of PROLOG: a specification method and its application","volume":"10","author":"Deransart","year":"1992","journal-title":"New Generation Computing"},{"key":"10.1016\/0304-3975(93)90107-5_BIB22","series-title":"French\u2013Japan Symp.","first-page":"133","article-title":"Logic programming, methodology and teaching","author":"Deransart","year":"1988"},{"key":"10.1016\/0304-3975(93)90107-5_BIB23","article-title":"Methodological view of logic programming with negation","author":"Deransart","year":"1989","journal-title":"INRIA RR 1011"},{"key":"10.1016\/0304-3975(93)90107-5_BIB24","series-title":"Proc. Tutorial ICLP '89","article-title":"Proofs, methods and declarative diagnosis in logic programming","author":"Deransart","year":"1989"},{"key":"10.1016\/0304-3975(93)90107-5_BIB25","article-title":"Attributes grammars: definitions, systems and biblioraphy","volume":"Vol. 323","author":"Deransart","year":"1988"},{"key":"10.1016\/0304-3975(93)90107-5_BIB26","article-title":"Modelling data dependencies in logic programs by attribute schemata","author":"Deransart","year":"1984","journal-title":"INRIA RR 323"},{"key":"10.1016\/0304-3975(93)90107-5_BIB27","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1016\/0743-1066(85)90015-9","article-title":"Relating logic programs and attribute grammars","volume":"2","author":"Deransart","year":"1985","journal-title":"J. Logic Programming"},{"key":"10.1016\/0304-3975(93)90107-5_BIB28","series-title":"Proc. PLILP '88","first-page":"219","article-title":"A grammatical view of logic programming","volume":"Vol. 348","author":"Deransart","year":"1989"},{"key":"10.1016\/0304-3975(93)90107-5_BIB29","series-title":"A Grammatical View of Loggic Programming","author":"Deransart","year":"1993"},{"key":"10.1016\/0304-3975(93)90107-5_BIB30","series-title":"Ph.D. Thesis","article-title":"A methodology for logic program construction","author":"Deville","year":"1987"},{"key":"10.1016\/0304-3975(93)90107-5_BIB31","series-title":"RP 88\/8","article-title":"A correctness definition for logic programming","author":"Deville","year":"1988"},{"key":"10.1016\/0304-3975(93)90107-5_BIB32","series-title":"Proc. 4th IEEE Symp. on Logic Programming","first-page":"389","article-title":"Do logic programs resemble programs in conventional languages?","author":"Drabent","year":"1987"},{"key":"10.1016\/0304-3975(93)90107-5_BIB33","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(88)90099-0","article-title":"Inductive assertion method for logic programs","volume":"59","author":"Drabent","year":"1988","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0304-3975(93)90107-5_BIB34","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/0743-1066(87)90001-X","article-title":"Error diagnosis in logic programming, an adaptation of E.Y. Shapiro's methods","volume":"4","author":"Ferrand","year":"1987","journal-title":"J. Logic Programming"},{"key":"10.1016\/0304-3975(93)90107-5_BIB35","series-title":"Logics of Programs","first-page":"89","article-title":"Proving termination of Prolog programs","volume":"Vol. 193","author":"Francez","year":"1985"},{"key":"10.1016\/0304-3975(93)90107-5_BIB36","series-title":"Proc. ICLP '88","first-page":"893","article-title":"Equivalence-preserving transformations of inductive properties of Prolog programs","author":"Fribourg","year":"1988"},{"key":"10.1016\/0304-3975(93)90107-5_BIB37","article-title":"Formulation induction formulas in verification of Prolog programs","author":"Fujita","year":"1984","journal-title":"Tech. Report 097"},{"key":"10.1016\/0304-3975(93)90107-5_BIB38","doi-asserted-by":"crossref","first-page":"372","DOI":"10.1145\/322248.322258","article-title":"Derivation of logic programs","volume":"28","author":"Hogger","year":"1981","journal-title":"J. ACM"},{"key":"10.1016\/0304-3975(93)90107-5_BIB39","series-title":"APIC Studies in Data Processing No 21","article-title":"Introduction to logic programming","author":"Hogger","year":"1984"},{"key":"10.1016\/0304-3975(93)90107-5_BIB40","series-title":"Tech. Report 84\/075","article-title":"On proving first order inductive properties in Horn clauses","author":"Hsiang","year":"1984"},{"key":"10.1016\/0304-3975(93)90107-5_BIB41","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1016\/0743-1066(90)90022-W","article-title":"Equivalent logic programs","volume":"8","author":"Hung","year":"1990","journal-title":"J. Logic Programming"},{"key":"10.1016\/0304-3975(93)90107-5_BIB42","article-title":"Soundness and completeness of extended execution of proving properties of Prolog programs","author":"Kanamori","year":"1986","journal-title":"Tech. Report 175"},{"key":"10.1016\/0304-3975(93)90107-5_BIB43","article-title":"ARGUS\/V: a system for verification of Prolog programs","author":"Kanamori","year":"1986","journal-title":"Tech. Report 176 ICOT"},{"key":"10.1016\/0304-3975(93)90107-5_BIB44","series-title":"Foundations of Logic Programming","author":"Lloyd","year":"1987"},{"key":"10.1016\/0304-3975(93)90107-5_BIB45","series-title":"Mathematical Theory of Computation","author":"Manna","year":"1974"},{"key":"10.1016\/0304-3975(93)90107-5_BIB46","series-title":"Report MIP-8810","article-title":"Inductive proofs of constructor-based Horn clauses","author":"Padawitz","year":"1988"},{"key":"10.1016\/0304-3975(93)90107-5_BIB47","first-page":"59","article-title":"Fixpoint induction and proofs of program properties","volume":"5","author":"Park","year":"1969","journal-title":"Machine Intelligence"},{"key":"10.1016\/0304-3975(93)90107-5_BIB48","series-title":"Proc. SLP '86","first-page":"140","article-title":"Characterisation of terminating logic programs","author":"Potter","year":"1986"},{"key":"10.1016\/0304-3975(93)90107-5_BIB49","series-title":"The Art of Prolog","author":"Sterling","year":"1986"},{"key":"10.1016\/0304-3975(93)90107-5_BIB50","series-title":"Proc. SL '88","first-page":"96","article-title":"Logic-programming from a logic point of view","author":"T\u00e4rlund","year":"1986"},{"key":"10.1016\/0304-3975(93)90107-5_BIB51","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","article-title":"A lattice-theoretical fixpoint theorem and its applications","volume":"5","author":"Tarski","year":"1955","journal-title":"Pacific J. Math."},{"key":"10.1016\/0304-3975(93)90107-5_BIB52","series-title":"Ph.D. Dissertation","article-title":"Toward a methodology for logic programming","author":"Vasak","year":"1986"},{"key":"10.1016\/0304-3975(93)90107-5_BIB53","doi-asserted-by":"crossref","first-page":"168","DOI":"10.1145\/322047.322062","article-title":"A new incompleteness result for Hoare's system","volume":"25","author":"Wand","year":"1978","journal-title":"J. ACM"},{"key":"10.1016\/0304-3975(93)90107-5_BIB54_1","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1007\/BF01692511","article-title":"Semantics of context-free languages","volume":"2","author":"Knuth","year":"1968","journal-title":"Math. Systems Theory"},{"key":"10.1016\/0304-3975(93)90107-5_BIB54_2","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1007\/BF01702865","article-title":"Semantics of context-free languages","volume":"5","author":"Knuth","year":"1968","journal-title":"Math. Systems Theory"},{"key":"10.1016\/0304-3975(93)90107-5_BIB55","series-title":"Proc. 18th ACM POPL","first-page":"177","article-title":"Verification of attribute grammars","author":"Katayama","year":"1981"},{"key":"10.1016\/0304-3975(93)90107-5_BIB56","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0004-3702(80)90003-X","article-title":"Definite clause grammars for language analysis\u2014a summary of the formalism and a comparison with augmented transition networks","volume":"13","author":"Pereira","year":"1980","journal-title":"Artificial Intelligence"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0304397593901075?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0304397593901075?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,13]],"date-time":"2019-04-13T00:24:28Z","timestamp":1555115068000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/0304397593901075"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,9]]},"references-count":57,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1993,9]]}},"alternative-id":["0304397593901075"],"URL":"https:\/\/doi.org\/10.1016\/0304-3975(93)90107-5","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[1993,9]]}}}