{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,6]],"date-time":"2025-06-06T04:06:56Z","timestamp":1749182816580,"version":"3.41.0"},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[1998,4,1]],"date-time":"1998-04-01T00:00:00Z","timestamp":891388800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1998,4,1]],"date-time":"1998-04-01T00:00:00Z","timestamp":891388800000},"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":[[1998,4]]},"DOI":"10.1023\/a:1005944606876","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T00:10:48Z","timestamp":1040515848000},"page":"27-45","source":"Crossref","is-referenced-by-count":7,"title":["Semantic Generalizations for Proving and Disproving Conjectures by Analogy"],"prefix":"10.1007","volume":"20","author":[{"given":"Gilles","family":"D\u00e9fourneaux","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christophe","family":"Bourely","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicolas","family":"Peltier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"146975_CR1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0004-3702(77)90012-1","volume":"9","author":"W. W. Bledsoe","year":"1977","unstructured":"Bledsoe, W. W.: Non-resolution theorem proving, Artificial Intelligence\n9 (19771), 1\u201335.","journal-title":"Artificial Intelligence"},{"key":"146975_CR2","doi-asserted-by":"crossref","unstructured":"Bourely, C., D\u00e9fourneaux, G. and Peltier, N.: Building proofs or counterexamples by analogy in a resolution framework, in Proc. JELIA 96, LNAI 1126, LNAI, Springer, 1966, pp. 34\u201349.","DOI":"10.1007\/3-540-61630-6_3"},{"key":"146975_CR3","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, LNCS 814, Springer, 1994, pp. 72\u201386.","DOI":"10.1007\/3-540-58156-1_6"},{"key":"146975_CR4","unstructured":"Boy de la Tour, Th. and Caferra, R.: Proof analogy in interactive theorem proving: A method to express and use it via second order pattern matching, in Proc. AAAI 87, Morgan Kaufmann, 1987, pp. 95\u201399."},{"key":"146975_CR5","doi-asserted-by":"crossref","unstructured":"Boy de la Tour, Th. and Kreitz, Ch.: Building proofs by analogy via the Curry-Howard isomorphism, in Proc. LPAR 92, Springer, 1992, pp. 202\u2013213.","DOI":"10.1007\/BFb0013062"},{"key":"146975_CR6","unstructured":"Caferra, R. and Peltier, N.: Extending semantic resolution via automated model building: applications, in Proc. IJCAI'95, Morgan Kaufman, 1995, pp. 328\u2013334."},{"key":"146975_CR7","doi-asserted-by":"crossref","unstructured":"Caferra, R. and Peltier, N.: Model building and interactive theory discovery, in Proc. Tableaux'95, LNAI 918, Springer, 1995, pp. 154\u2013158.","DOI":"10.1007\/3-540-59338-1_34"},{"key":"146975_CR8","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":"146975_CR9","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":"146975_CR10","doi-asserted-by":"crossref","unstructured":"Curien, R., Qian, Z. and Hui-Shi: Efficient second-order matching, in in Harald Ganzinger (ed.), Proc. Rewriting Techniques and Applications Vol. 1103, Lecture Notes in Computer Science, Springer, 1996, pp. 317\u2013331.","DOI":"10.1007\/3-540-61464-8_62"},{"key":"146975_CR11","doi-asserted-by":"crossref","unstructured":"Hall, R. P.: Computational approaches to analogical reasoning: A comparative analysis, Artificial Intelligence (1989), 39\u2013120.","DOI":"10.1016\/0004-3702(89)90003-9"},{"key":"146975_CR12","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. Huet","year":"1975","unstructured":"Huet, G.: A unification algorithm for typed \u03bb-calculus, Theoretical Computer Science\n1 (1975), 27\u201357.","journal-title":"Theoretical Computer Science"},{"key":"146975_CR13","doi-asserted-by":"crossref","unstructured":"Kling, R. E.: A paradigm for reasoning by analogy, Artificial Intelligence\n2 (1971).","DOI":"10.1016\/0004-3702(71)90008-7"},{"key":"146975_CR14","unstructured":"Kolbe, Th. and Walther, Ch.: Second-order matching modulo evaluation \u2013 A technique for reusing proofs, in Chris S. Mellish (ed.), Proc. IJCAI 95, IJCAI, Morgan Kaufmann, 1995, pp. 190\u2013195."},{"key":"146975_CR15","unstructured":"Loveland, D. W.: Automated theorem proving: A logical basis Vol. 6 of Fundamental Studies in Computer Science, North Holland, 1978."},{"key":"146975_CR16","doi-asserted-by":"crossref","unstructured":"Mal'cev, A. I.: The Metamathematics of Algebraic Systems: Collected Papers 1936\u20131967, chapter axiomatizable classes of locally free algebra of various type, pp. 262\u2013281. Benjamin Franklin Wells III (ed.), Ch. 23, North Holland, 1971.","DOI":"10.1016\/S0049-237X(08)70560-3"},{"key":"146975_CR17","unstructured":"Melis, E.: A model of analogy-driven proof-plan construction, in Proc. 14th International Joint Conference on Artificial Intelligence, Montreal, 1995, pp. 182\u2013189."},{"key":"146975_CR18","unstructured":"Munyer,_J. C.: Analogy as a mean of discovery in problem-solving and learning, PhD thesis, Univ. Calif. Santa Cruz, 1981."},{"key":"146975_CR19","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1016\/0004-3702(81)90015-1","volume":"16","author":"D. A. Plaisted","year":"1981","unstructured":"Plaisted, D. A.: Theorem proving with abstraction, Artificial Intelligence\n16 (1981), 47\u2013108.","journal-title":"Artificial Intelligence"},{"key":"146975_CR20","doi-asserted-by":"crossref","unstructured":"Suttner, Ch. B. and Sutcliffe, G.: The TPTP problem library, Technical report, TU M\u00fcunchen\/James Cook University, 1995. V-1.2.0.","DOI":"10.1093\/jigpal\/3.6.957"},{"key":"146975_CR21","unstructured":"Wos, L.: Automated Reasoning: 33 Basic Research Problems, Prentice Hall, 1988."},{"key":"146975_CR22","unstructured":"Wos, L., Overbeek, R., Lusk, E. and Boyle, J.: Automated Reasoning: Introduction and Application, second edition, McGraw-Hill, 1992."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005944606876.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1005944606876\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005944606876.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:46:57Z","timestamp":1749124017000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1005944606876"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,4]]},"references-count":22,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[1998,4]]}},"alternative-id":["146975"],"URL":"https:\/\/doi.org\/10.1023\/a:1005944606876","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[1998,4]]}}}