{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,6]],"date-time":"2025-06-06T04:06:55Z","timestamp":1749182815004,"version":"3.41.0"},"reference-count":50,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1997,12,1]],"date-time":"1997-12-01T00:00:00Z","timestamp":880934400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1997,12,1]],"date-time":"1997-12-01T00:00:00Z","timestamp":880934400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[1997,12]]},"DOI":"10.1023\/a:1005878609884","type":"journal-article","created":{"date-parts":[[2002,12,21]],"date-time":"2002-12-21T23:56:21Z","timestamp":1040514981000},"page":"277-318","source":"Crossref","is-referenced-by-count":4,"title":["A New Technique for Verifying and Correcting Logic Programs"],"prefix":"10.1007","volume":"19","author":[{"given":"Ricardo","family":"Caferra","sequence":"first","affiliation":[]},{"given":"Nicolas","family":"Peltier","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"136451_CR1","first-page":"9","volume":"19","author":"R. Apt Krzystof","year":"1994","unstructured":"Krzystof, R. Apt and Roland, N. Bol.: Logic programming and negation: A survey, J. Logic Programming\n19, 20(1994), 9\u201371.","journal-title":"J. Logic Programming"},{"key":"136451_CR2","doi-asserted-by":"crossref","unstructured":"Bourely, Ch., Caferra, R. and Peltier, N.: A method for building models automatically. Experiments with an extension of OTTER, in Proc. CADE-12, LNAI 814, Springer, 1994, pp. 72\u201386.","DOI":"10.1007\/3-540-58156-1_6"},{"key":"136451_CR3","unstructured":"Bourely, Ch. And Peltier, N.: Disc_atinf: a system for implementing strategies and calculi, in Proc. DISCO\u201996.Springer, 1996. To appear."},{"key":"136451_CR4","unstructured":"Caferra, R. and Peltier, N.: Extending semantic resolution via automated model building: applications, in Proc. IJCAI\u201995, Morgan Kaufmann, 1995, pp. 328\u2013334."},{"key":"136451_CR5","doi-asserted-by":"crossref","unstructured":"Caferra, R. and Peltier, N.: Model building and interactive theory discovery, in Proc. Tableaux\u201995, LNAI 918, Springer, 1995, pages 154\u2013168.","DOI":"10.1007\/3-540-59338-1_34"},{"key":"136451_CR6","doi-asserted-by":"crossref","unstructured":"Caferra, R. and Peltier, N.: Decision procedures using model building techniques, in Proc. Computer Science Logic, CSL\u201995, LNCS 1092, Springer, 1996, pp. 130\u2013144.","DOI":"10.1007\/3-540-61377-3_35"},{"key":"136451_CR7","doi-asserted-by":"crossref","unstructured":"Caferra, R. and Peltier, N.: A significant extension of logic programming by adapting model buildings rules, in Proc. Extensions of Logic Programming 96, LNAI 1050, Springer, March 1996, pp. 51\u201365.","DOI":"10.1007\/3-540-60983-0_4"},{"key":"136451_CR8","doi-asserted-by":"crossref","unstructured":"Caferra, R. and Zabel, N.:. Extending resolution for model construction, in Logics in AI, JELIA\u201990, LNAI 478, Springer, 1990, pp. 153\u2013169.","DOI":"10.1007\/BFb0018439"},{"key":"136451_CR9","doi-asserted-by":"crossref","first-page":"613","DOI":"10.1016\/S0747-7171(10)80014-8","volume":"13","author":"R. Caferra","year":"1992","unstructured":"Caferra, R. and Zabel, N.: A method for simultaneous search for refutations and models by equational constraint solving, J. Symbolic Computation\n13(1992), 613\u2013641.","journal-title":"J. Symbolic Computation"},{"key":"136451_CR10","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1093\/logcom\/3.1.3","volume":"3","author":"R. Caferra","year":"1993","unstructured":"Caferra, R. and Zabel, N.: Building models by using tableaux extended by equational problems, J. Logic and Computation\n3(1993), 3\u201325.","journal-title":"J. Logic and Computation"},{"key":"136451_CR11","doi-asserted-by":"crossref","unstructured":"Clark, K. L.: Negation as failure, in Herv\u00e9 Gallaire and Jack Minker (eds), Logic and Data Bases, Plenum Press, 1978, pp. 293\u2013322.","DOI":"10.1007\/978-1-4684-3384-5_11"},{"key":"136451_CR12","unstructured":"Clark, K. L. and Tarnlund, S.-A.: A first order theory of data and programs, in Proc. of IFIP-77, North-Holland, 1977, pp. 939\u2013944."},{"key":"136451_CR13","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1016\/S0747-7171(89)80017-3","volume":"7","author":"H. Comon","year":"1989","unstructured":"Comon, H. and Lescanne, P.: Equational problems and disunification, J. Symbolic Computation\n7(1989), 371\u2013475.","journal-title":"J. Symbolic Computation"},{"key":"136451_CR14","unstructured":"Cooper, D. C.: Theorem proving in arithmetic without multiplication, in Bernard Meltzer and Donald Michie (eds), Machine Intelligence 7, Ch. 5, Edinburgh University Press, 1972, pp. 91\u201399."},{"key":"136451_CR15","doi-asserted-by":"crossref","unstructured":"Davis, M.: A computer program for Presburger arithmetic, in J. Siekmann and G. Wrighston (eds), Automation of Reasoning 1, Springer, 1983, pp. 41\u201348.","DOI":"10.1007\/978-3-642-81952-0_3"},{"issue":"20","key":"136451_CR16","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1016\/0743-1066(94)90029-9","volume":"19","author":"Y. Deville","year":"1994","unstructured":"Deville, Y. Lau, K-K.: Logic program synthesis, J. Logic Programming\n19(20) (1994), 321\u2013350.","journal-title":"J. Logic Programming"},{"key":"136451_CR17","unstructured":"Enderton, H.: A Mathematical Introduction to Logic, Academic Press, 1972."},{"key":"136451_CR18","doi-asserted-by":"crossref","unstructured":"Ferm\u00fcller, Ch, and Leitsch, A.: Hyperresolution and automated model building, J. Logic and Computation(1996), to appear.","DOI":"10.1093\/logcom\/6.2.173"},{"key":"136451_CR19","doi-asserted-by":"crossref","unstructured":"Ferm\u00fcller, Ch, Leitsch, A., Tamet, T. and Zamov, N.: Resolution Methods for the Decision Problem, LNAI 679. Springer, 1993.","DOI":"10.1007\/3-540-56732-1"},{"key":"136451_CR20","doi-asserted-by":"crossref","unstructured":"Flener, P.: Logic Program Synthesis from Incomplete Information, Kluwer Academic Publishers, 1995.","DOI":"10.1007\/978-1-4615-2205-8"},{"key":"136451_CR21","unstructured":"Fujita, M., Slaney, J. and Bennett, F.: Automatic generation of some results in finite algebra, in Proc. IJCAI93, Morgan Kaufmann, 1993."},{"issue":"2","key":"136451_CR22","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1145\/3149.214118","volume":"32","author":"G. Gottlob","year":"1985","unstructured":"Gottlob, G. and Leitsch, A.: On the efficiency of subsumption algorithms, J. ACM\n32(2) (1985), 280\u2013295.","journal-title":"J. ACM"},{"key":"136451_CR23","doi-asserted-by":"crossref","first-page":"372","DOI":"10.1145\/322248.322258","volume":"28","author":"C. J. Hogger","year":"1981","unstructured":"Hogger, C. J.: Derivation of logic programs, J. ACM\n28(1981), 372\u2013422.","journal-title":"J. ACM"},{"key":"136451_CR24","unstructured":"Hogger, Ch. J.: Introduction to Logic Programming, Academic Press, 1984."},{"key":"136451_CR25","doi-asserted-by":"crossref","unstructured":"Huntbach, M. M.: An improved version of Shapiro\u2019s model inference system, in Proc. Third Int. Conf. on Logic Programming, LNCS 225, Springer, 1986, pp. 180\u2013187.","DOI":"10.1007\/3-540-16492-8_74"},{"key":"136451_CR26","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/0304-3975(94)90202-X","volume":"122","author":"T. Kawamura","year":"1994","unstructured":"Kawamura, T.: Logic program synthesis from first order logic specification, Theor. Computer Science\n122(1994), 69\u201396.","journal-title":"Theor. Computer Science"},{"key":"136451_CR27","unstructured":"Kowalski, R.: The relation between logic programming and logic specification, in C. A. R. Hoare and J. C. Shepherdson (eds), Mathematical Logic and Programming Languages, Prentice-Hall, 1985, pp. 11\u201327."},{"key":"136451_CR28","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1016\/0743-1066(87)90007-0","volume":"8","author":"K. Kunen","year":"1987","unstructured":"Kunen, K.: Negation in logic programming, J. Logic Programming\n8(1987), 289\u2013308.","journal-title":"J. Logic Programming"},{"key":"136451_CR29","doi-asserted-by":"crossref","unstructured":"Lloyd, J. W.: Foundations of Logic Programming, second edition, Springer, 1987.","DOI":"10.1007\/978-3-642-83189-8"},{"key":"136451_CR30","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/BF03037396","volume":"5","author":"J. W. Lloyd","year":"1987","unstructured":"Lloyd, J. W.: Declarative error diagnosis, New Generation Computing\n5(1987), 133\u2013154.","journal-title":"New Generation Computing"},{"key":"136451_CR31","unstructured":"Loveland, D. W.: Automated Theorem Proving: A Logical Basis, Fundamental Studies in\nComputer Science, Vol. 6, North Holland, 1978."},{"issue":"3","key":"136451_CR32","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1016\/0743-1066(84)90011-6","volume":"1","author":"J. W. Lloyd","year":"1984","unstructured":"Lloyd, J. W. and Topor, R. W.: Making prolog more expressive. J. Logic Programming\n1(3) (1984), 225\u2013240.","journal-title":"J. Logic Programming"},{"key":"136451_CR33","unstructured":"Lugiez, D.: A deduction procedure for first order programs, in F. Levi and M. Martelli (eds), Proc. Sixth Int. Conf. Logic Programming, The MIT Press, July 1989, pp. 585\u2013599."},{"key":"136451_CR34","unstructured":"Mal\u2019cev, A. I.: The Metamathematics of Algebraic Systems: Collected Papers 1936\u20131967, chapter Axiomatizable classes of locally free algebra of various type, Benjamin Franklin Wells III (ed.), Ch. 23, North Holland, 1971."},{"key":"136451_CR35","doi-asserted-by":"crossref","unstructured":"Manthey, R. and Bry, F.: SATCHMO: A theorem prover implemented in Prolog, in Proc. CADE-9, LNCS 310, Springer, 1988, pp. 415\u2013434.","DOI":"10.1007\/BFb0012847"},{"key":"136451_CR36","unstructured":"McCune, W. W.: OTTER 2.0 Users Guide, Argonne National Laboratory, 1990."},{"key":"136451_CR37","doi-asserted-by":"crossref","unstructured":"Peltier, N.: Increasing the capabilities of model building by constraint solving with terms with integer exponents, 1997, preprint.","DOI":"10.1006\/jsco.1997.0114"},{"key":"136451_CR38","doi-asserted-by":"crossref","unstructured":"Pereira, L-M.: Rational debugging in logic programming, in Proc. Third Int. Conf. Logic Programming, LNCS 225, Springer, 1986, pp. 203\u2013210.","DOI":"10.1007\/3-540-16492-8_76"},{"key":"136451_CR39","unstructured":"Plaisted, D. A.: An efficient bug location algorithm, in Proc. Second Int. Logic Programming Conference, 1984, pp. 151\u2013157."},{"issue":"3","key":"136451_CR40","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF00244944","volume":"4","author":"D. A. Plaisted","year":"1988","unstructured":"Plaisted, D. A.: Non-Horn clause logic programming without contrapositives, J. Automated Reasoning\n4(3) (1988), 287\u2013325.","journal-title":"J. Automated Reasoning"},{"key":"136451_CR41","unstructured":"Presburger, M.: \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchen die Addition als einzige Operation hervortritt, in Comptes Rendus du I Congr\u00e9s de Math\u00e9maticiens des Pays Slaves, 1029, pp. 92\u2013101."},{"key":"136451_CR42","doi-asserted-by":"crossref","unstructured":"Shapiro, E. Y.: Algorithmic Program Debugging, MIT Press, 1983.","DOI":"10.7551\/mitpress\/1192.001.0001"},{"key":"136451_CR43","unstructured":"Sterling, L. and Shapiro, E.: The Art of Prolog, The MIT Press, 1986."},{"key":"136451_CR44","doi-asserted-by":"crossref","first-page":"605","DOI":"10.1016\/S0747-7171(89)80064-1","volume":"8","author":"T. Sato","year":"1988","unstructured":"Sato, T. and Tamaki, H.: First order compiler: A deterministic logic program synthesis algorithm, J. Symbolic Computation\n8(1988), 605\u2013627.","journal-title":"J. Symbolic Computation"},{"issue":"4","key":"136451_CR45","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/BF00244275","volume":"1","author":"M. E. Stickel","year":"1985","unstructured":"Stickel, M. E.: Automated deduction by theory resolution, J. Automated Reasoning\n1(4) (1985), 333\u2013355.","journal-title":"J. Automated Reasoning"},{"key":"136451_CR46","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1006\/inco.1995.1048","volume":"118","author":"P. Stuckey","year":"1995","unstructured":"Stuckey, P.: Negation and constraint logic programming, Information and Computation\n118(1995), 12\u201333.","journal-title":"Information and Computation"},{"issue":"3","key":"136451_CR47","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1145\/131295.131299","volume":"35","author":"D. S. Warren","year":"1992","unstructured":"Warren, D. S.: Memoing for logic programs, Comm. ACM\n35(3) (1992), 93\u2013111.","journal-title":"Comm. ACM"},{"issue":"2","key":"136451_CR48","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1145\/322307.322308","volume":"29","author":"S. Winker","year":"1982","unstructured":"Winker, S.: Generation and verification of finite models and counter-examples using an automated theorem prover answering two open questions, J. ACM\n29(2) (1982), 273\u2013284.","journal-title":"J. ACM"},{"key":"136451_CR49","unstructured":"Wos, L., Overbeek, R., Lusk, E. and Boyle, J.: Automated Reasoning: Introduction and Applications, second edition, McGraw-Hill, 1992."},{"key":"136451_CR50","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF00881795","volume":"10","author":"L. Wos","year":"1993","unstructured":"Wos, L.: The kernel strategy and its use for the study of combinatory logic, J. Automated Reasoning\n10(1993), 287\u2013343.","journal-title":"J. Automated Reasoning"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005878609884.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1005878609884\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005878609884.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:43:11Z","timestamp":1749123791000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1005878609884"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997,12]]},"references-count":50,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1997,12]]}},"alternative-id":["136451"],"URL":"https:\/\/doi.org\/10.1023\/a:1005878609884","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[1997,12]]}}}