{"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":1749125183681},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540613770"},{"type":"electronic","value":"9783540685074"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61377-3_35","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:36:18Z","timestamp":1330292178000},"page":"130-144","source":"Crossref","is-referenced-by-count":13,"title":["Decision procedures using model building techniques"],"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":"8_CR1","doi-asserted-by":"crossref","unstructured":"Egon B\u00d6RGER. Decision problems in predicate logic. In G. Longo G. Lolli and A. Marcja, editors, Logic Colloquium'82, pages 263\u2013301. North-Holland, 1984.","DOI":"10.1016\/S0049-237X(08)71820-2"},{"key":"8_CR2","unstructured":"Ricardo CAFERRA and Nicolas PELTIER. Extending semantic resolution via automated model building: applications. In Proceeding of IJCAI'95. Morgan Kaufmann, 1995."},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Ricardo CAFERRA and Nicolas PELTIER. Model building and interactive theory discovery. In Proceeding of Tableaux'95, LNAI 918, pages 154\u2013168. Springer-Verlag, 1995.","DOI":"10.1007\/3-540-59338-1_34"},{"key":"8_CR4","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":"8_CR5","unstructured":"Burton DREBEN and Warren D. GOLDFARB. The Decision Problem, Solvable Classes of Quantificational Formulas. Addison-Wesley, 1979."},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Christian FERM\u00dcLLER and Alexander LEITSCH. Model building by resolution. In Computer Science Logic, CSL '92, pages 134\u2013148. Springer-Verlag, LNCS 702, 1992.","DOI":"10.1007\/3-540-56992-8_10"},{"key":"8_CR7","unstructured":"Christian FERM\u00dcLLER and A. LEITSCH. Hyperresolution and automated model building. Journal of Logic and Computation, 1995. To appear."},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"C. FERM\u00dcLLER, A. LEITSCH, T. TAMMET, and N. ZAMOV. Resolution Methods for the Decision Problem. LNAI 679, Springer-Verlag, 1993.","DOI":"10.1007\/3-540-56732-1"},{"key":"8_CR9","doi-asserted-by":"crossref","first-page":"398","DOI":"10.1145\/321958.321960","volume":"23","author":"W.H. Joyner","year":"1976","unstructured":"W.H. Joyner. Resolution strategies as decision procedures. Journal of the ACM, 23:398\u2013417, 1976.","journal-title":"Journal of the ACM"},{"key":"8_CR10","doi-asserted-by":"crossref","first-page":"163","DOI":"10.3233\/FI-1993-182-406","volume":"18","author":"A. Leitsch","year":"1993","unstructured":"Alexander Leitsch. Deciding clause classes by semantic clash resolution. Fundamenta Informaticae, 18:163\u2013182, 1993.","journal-title":"Fundamenta Informaticae"},{"key":"8_CR11","unstructured":"Harry LEWIS. Unsolvable classes of quantificational formulas. Addison-Wesley, 1979."},{"key":"8_CR12","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1007\/BF00244271","volume":"1","author":"W. McCune","year":"1985","unstructured":"William McCune and Lawrence Henschen. Experiments with semantic paramodulation. Journal of Automated Reasoning, 1:231\u2013261, 1985.","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"8_CR13","doi-asserted-by":"crossref","first-page":"385","DOI":"10.2307\/2274689","volume":"56","author":"G. E. Mints","year":"1991","unstructured":"Grigori E. Mints. Proof theory in the USSR 1925\u20131969. Journal of Symbolic Logic, 56(2):385\u2013424, June 1991.","journal-title":"Journal of Symbolic Logic"},{"issue":"4","key":"8_CR14","doi-asserted-by":"crossref","first-page":"687","DOI":"10.1145\/321420.321428","volume":"14","author":"J. 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":"8_CR15","doi-asserted-by":"crossref","unstructured":"Tanel Tammet. Using resolution for deciding solvable classes and building finite models. In Baltic Computer Science, pages 33\u201364. Springer-Verlag, LNCS 502, 1991.","DOI":"10.1007\/BFb0019355"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61377-3_35.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T10:34:27Z","timestamp":1640946867000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61377-3_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540613770","9783540685074"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-61377-3_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}