{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:06:23Z","timestamp":1749125183768},"publisher-location":"Berlin, Heidelberg","reference-count":6,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540593386"},{"type":"electronic","value":"9783540492351"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-59338-1_34","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:13:48Z","timestamp":1330276428000},"page":"154-168","source":"Crossref","is-referenced-by-count":10,"title":["Model building and interactive theory discovery"],"prefix":"10.1007","author":[{"given":"Ricardo","family":"Caferra","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicolas","family":"Peltier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Christophe BOURELY, Ricardo CAFERRA, and Nicolas PELTIER. A method for building models automatically. experiments with an extension of otter. In Proc. of CADE-12, pages 72\u201386. Springer Verlag, 1994. LNAI 814.","DOI":"10.1007\/3-540-58156-1_6"},{"key":"11_CR2","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":"11_CR3","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1093\/logcom\/3.1.3","volume":"3","author":"R. Caferra","year":"1993","unstructured":"Ricardo CAFERRA and Nicolas ZABEL. Building models by using tableaux extended by equational problems. Journal of Logic and Computation, 3:3\u201325, 1993.","journal-title":"Journal of Logic and Computation"},{"key":"11_CR4","unstructured":"Burton DREBEN and Warren D. GOLDFARB. The Decision Problem, Solvable Classes of Quantificational Formulas. Addison-Wesley, 1979."},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"C. FERM\u00dcLLER, A. LEITSH, T. TAMMET, and N. ZAMOV. Resolution Methods for the Decision Problem. Lecture Notes in Artificial Intelligence. Springer-Verlag, 1993. LNAI 679.","DOI":"10.1007\/3-540-56732-1"},{"key":"11_CR6","unstructured":"Nicolas PELTIER. Model building by constraint solving with terms with integer exponents. Submitted to CP95, 1995."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-59338-1_34.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:26:51Z","timestamp":1605648411000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-59338-1_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540593386","9783540492351"],"references-count":6,"URL":"https:\/\/doi.org\/10.1007\/3-540-59338-1_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}