{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:20:58Z","timestamp":1747592458939,"version":"3.37.0"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642029585"},{"type":"electronic","value":"9783642029592"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02959-2_30","type":"book-chapter","created":{"date-parts":[[2009,7,25]],"date-time":"2009-07-25T05:02:22Z","timestamp":1248498142000},"page":"404-420","source":"Crossref","is-referenced-by-count":7,"title":["Decidability Results for Saturation-Based Model Building"],"prefix":"10.1007","author":[{"given":"Matthias","family":"Horbach","sequence":"first","affiliation":[]},{"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"30_CR1","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L. Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation\u00a04(3), 217\u2013247 (1994)","journal-title":"Journal of Logic and Computation"},{"key":"30_CR2","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/B978-044450813-3\/50004-7","volume-title":"Handbook of Automated Reasoning, ch. 2","author":"L. Bachmair","year":"2001","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 2, vol.\u00a0I, pp. 19\u201399. Elsevier, Amsterdam (2001)"},{"key":"30_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/978-3-540-45085-6_32","volume-title":"Automated Deduction \u2013 CADE-19","author":"P. Baumgartner","year":"2003","unstructured":"Baumgartner, P., Tinelli, C.: The model evolution calculus. In: Baader, F. (ed.) CADE 2003. LNCS, vol.\u00a02741, pp. 350\u2013364. Springer, Heidelberg (2003)"},{"key":"30_CR4","series-title":"Applied Logic Series","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4020-2653-9","volume-title":"Automated Model Building","author":"R. Caferra","year":"2004","unstructured":"Caferra, R., Leitsch, A., Peltier, N.: Automated Model Building. Applied Logic Series, vol.\u00a031. Kluwer, Dordrecht (2004)"},{"issue":"3-4","key":"30_CR5","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1016\/S0747-7171(89)80017-3","volume":"7","author":"H. Comon","year":"1989","unstructured":"Comon, H., Lescanne, P.: Equational problems and disunification. Journal of Symbolic Computation\u00a07(3-4), 371\u2013425 (1989)","journal-title":"Journal of Symbolic Computation"},{"issue":"1\/2","key":"30_CR6","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1006\/inco.2000.2875","volume":"159","author":"H. Comon","year":"2000","unstructured":"Comon, H., Nieuwenhuis, R.: Induction = I-Axiomatization + First-Order Consistency. Information and Computation\u00a0159(1\/2), 151\u2013186 (2000)","journal-title":"Information and Computation"},{"issue":"2","key":"30_CR7","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1093\/logcom\/6.2.173","volume":"6","author":"C.G. Ferm\u00fcller","year":"1996","unstructured":"Ferm\u00fcller, C.G., Leitsch, A.: Hyperresolution and automated model building. Journal of Logic and Computation\u00a06(2), 173\u2013203 (1996)","journal-title":"Journal of Logic and Computation"},{"key":"30_CR8","doi-asserted-by":"publisher","first-page":"1791","DOI":"10.1016\/B978-044450813-3\/50027-8","volume-title":"Handbook of Automated Reasoning, ch. 25","author":"C.G. Ferm\u00fcller","year":"2001","unstructured":"Ferm\u00fcller, C.G., Leitsch, A., Hustadt, U., Tamet, T.: Resolution decision procedures. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 25, vol.\u00a0II, pp. 1791\u20131849. Elsevier, Amsterdam (2001)"},{"issue":"3","key":"30_CR9","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1093\/logcom\/exm008","volume":"17","author":"C.G. Ferm\u00fcller","year":"2007","unstructured":"Ferm\u00fcller, C.G., Pichler, R.: Model representation over finite and infinite signatures. Journal of Logic and Computation\u00a017(3), 453\u2013477 (2007)","journal-title":"Journal of Logic and Computation"},{"key":"30_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/3-540-56393-8_17","volume-title":"Conditional Term Rewriting Systems","author":"H. Ganzinger","year":"1992","unstructured":"Ganzinger, H., Stuber, J.: Inductive theorem proving by consistency for first-order clauses. In: Rusinowitch, M., R\u00e9my, J. (eds.) CTRS 1992. LNCS, vol.\u00a0656, pp. 226\u2013241. Springer, Heidelberg (1992)"},{"key":"30_CR11","unstructured":"Hillenbrand, T., Weidenbach, C.: Superposition for finite domains. Research Report MPI-I-2007-RG1-002, Max Planck Institute for Computer Science, Saarbr\u00fccken, Germany (April 2007)"},{"key":"30_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/978-3-540-87531-4_22","volume-title":"Computer Science Logic","author":"M. Horbach","year":"2008","unstructured":"Horbach, M., Weidenbach, C.: Superposition for fixed domains. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol.\u00a05213, pp. 293\u2013307. Springer, Heidelberg (2008)"},{"key":"30_CR13","doi-asserted-by":"crossref","unstructured":"Horbach, M., Weidenbach, C.: Decidability results for saturation-based model building. Technical Report MPI-I-2009-RG1-004, Max Planck Institute for Computer Science, Saarbr\u00fccken, Germany (2009)","DOI":"10.1007\/978-3-642-02959-2_30"},{"key":"30_CR14","first-page":"251","volume":"1","author":"U. Hustadt","year":"2004","unstructured":"Hustadt, U., Schmidt, R., Georgieva, L.: A survey of decidable first-order fragments and description logics. J. of Relational Methods in CS\u00a01, 251\u2013276 (2004)","journal-title":"J. of Relational Methods in CS"},{"issue":"3","key":"30_CR15","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/BF00243794","volume":"3","author":"J.-L. Lassez","year":"1987","unstructured":"Lassez, J.-L., Marriott, K.: Explicit representation of terms defined by counter examples. Journal of Automated Reasoning\u00a03(3), 301\u2013317 (1987)","journal-title":"Journal of Automated Reasoning"},{"key":"30_CR16","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1016\/B978-044450813-3\/50009-6","volume-title":"Handbook of Automated Reasoning, ch. 7","author":"R. Nieuwenhuis","year":"2001","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 7, vol.\u00a0I, pp. 371\u2013443. Elsevier, Amsterdam (2001)"},{"key":"30_CR17","doi-asserted-by":"publisher","first-page":"1965","DOI":"10.1016\/B978-044450813-3\/50029-1","volume-title":"Handbook of Automated Reasoning, ch. 27","author":"C. Weidenbach","year":"2001","unstructured":"Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 27, vol.\u00a02, pp. 1965\u20132012. Elsevier, Amsterdam (2001)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-22"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02959-2_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,11]],"date-time":"2025-02-11T12:01:51Z","timestamp":1739275311000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02959-2_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642029585","9783642029592"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02959-2_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}