{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:06:19Z","timestamp":1749125179926},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540581567"},{"type":"electronic","value":"9783540484677"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58156-1_6","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:23:53Z","timestamp":1330269833000},"page":"72-86","source":"Crossref","is-referenced-by-count":15,"title":["A method for building models automatically. Experiments with an extension of OTTER"],"prefix":"10.1007","author":[{"given":"Christophe","family":"Bourely","sequence":"first","affiliation":[]},{"given":"Ricardo","family":"Caferra","sequence":"additional","affiliation":[]},{"given":"Nicolas","family":"Peltier","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"6_CR1","unstructured":"Christophe BOURELY, Ricardo CAFERRA, and Nicolas PELTIER. Model building in automated deduction. Forthcoming, 1994."},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Leo BACHMAIR, Harald GANZINGER, and Uwe WALDMANN. Superposition with simplification as a decision procedure for the monadic class with equality. In Computational Logic and Proof Theory, KGC'93, pages 83\u201396. Springer-Verlag, Lecture Notes in Computer Science 713, 1993.","DOI":"10.1007\/BFb0022557"},{"key":"6_CR3","volume-title":"volume 29 of Contemporary Mathematics","author":"W. W. Bledsoe","year":"1984","unstructured":"W.W. BLEDSOE and D.W. LOVELAND. Automated Theorem Proving after 25 years, volume 29 of Contemporary Mathematics. American Mathematical Society, Providence, RI, USA, 1984."},{"key":"6_CR4","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1016\/S0747-7171(89)80017-3","volume":"7","author":"H. Comon","year":"1989","unstructured":"Hubert COMON and Pierre LESCANNE. Equational problems and disunification. Journal of Symbolic Computation, 7:371\u2013475, 1989.","journal-title":"Journal of Symbolic Computation"},{"key":"6_CR5","unstructured":"Hubert COMON. Disunification: a survey. In Jean-Louis Lassez and Gordon Pl\u00f6tkin, editors, Computational Logic: Essays in Honor of Alan Robinson. MIT Press, 1991."},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Ricardo CAFERRA and Nicolas ZABEL. Extending resolution for model construction. In Logics in AI, JELIA'90, pages 153\u2013169. Springer-Verlag, Lecture Notes in Artificial Intelligence 478, 1991.","DOI":"10.1007\/BFb0018439"},{"key":"6_CR7","doi-asserted-by":"crossref","first-page":"613","DOI":"10.1016\/S0747-7171(10)80014-8","volume":"13","author":"R. Caferra","year":"1992","unstructured":"Ricardo CAFERRA and Nicolas ZABEL. A method for simultaneous search for refutations and models by equational constraint solving. Journal of Symbolic Computation, 13:613\u2013641, 1992.","journal-title":"Journal of Symbolic Computation"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Christian G. FERM\u00fcLLER and Alexander LEITSCH. Model building by resolution. In Computer Science Logic, CSL'92, pages 134\u2013148. Springer-Verlag, Lecture Notes in Computer Science 702, 1992.","DOI":"10.1007\/3-540-56992-8_10"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"C. FERM\u00fcLLER, A. LEITSCH, T. TAMMET, and N. ZAMOV. Resolution Methods for the Decision Problem. Lecture Notes in Artificial Intelligence 679. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-56732-1"},{"key":"6_CR10","unstructured":"Masayuki FUJITA, John SLANEY, and Frank BENNETT. Automatic generation of some results in finite algebra. In Proceedings of IJCAI'93, pages 52\u201367. Morgan and Kaufmann, 1993."},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"H. GELERNTER, J.R. HANSEN, and D.W. LOVELAND. Empirical explorations of the geometry theorem-proving machine. In J\u00f6rg Siekmann and Graham Wrightson, editors, Automation of Reasoning, vol. 1, pages 140\u2013150. Springer-Verlag, 1983. Originally published in 1960.","DOI":"10.1007\/978-3-642-81952-0_10"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Rainer MANTHEY and Fran\u00e7ois BRY. Satchmo: A theorem prover implemented in PROLOG. In Proc. of CADE-9, pages 415\u2013434. Springer-Verlag, Lecture Notes in Computer Science 310, 1988.","DOI":"10.1007\/BFb0012847"},{"key":"6_CR13","unstructured":"William W. McCUNE. OTTER 2.0 Users Guide. Argonne National Laboratory, 1990."},{"issue":"1\u20132","key":"6_CR14","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1007\/BF02759780","volume":"28","author":"S. Shelah","year":"1977","unstructured":"Saharon SHELAH. Decidability of a portion of the predicate calculus. Israel Journal of Mathematics, 28(1\u20132):32\u201344, 1977.","journal-title":"Israel Journal of Mathematics"},{"issue":"4","key":"6_CR15","doi-asserted-by":"crossref","first-page":"687","DOI":"10.1145\/321420.321428","volume":"14","author":"James R. R. Slagle","year":"1967","unstructured":"James R. SLAGLE. Automatic theorem proving with renamable and semantic resolution. Journal of the ACM, 14(4):687\u2013697, October 1967.","journal-title":"Journal of the ACM"},{"key":"6_CR16","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1145\/322307.322308","volume":"29","author":"S. Winker","year":"1982","unstructured":"Steve WINKER. Generation and verification of finite models and counterexamples using an automated theorem prover answering two open questions. Journal of the ACM, 29:273\u2013284, 1982.","journal-title":"Journal of the ACM"},{"issue":"1","key":"6_CR17","first-page":"15","volume":"40","author":"L. Wos","year":"1993","unstructured":"Larry WOS. Automated reasoning. Notices of the American Mathematical Society, 40(1):15\u201326, January 1993.","journal-title":"Notices of the American Mathematical Society"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-12"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58156-1_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:17:44Z","timestamp":1605647864000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58156-1_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581567","9783540484677"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-58156-1_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}