{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T15:08:40Z","timestamp":1743001720020,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642224379"},{"type":"electronic","value":"9783642224386"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-22438-6_25","type":"book-chapter","created":{"date-parts":[[2011,7,18]],"date-time":"2011-07-18T18:21:44Z","timestamp":1311013304000},"page":"331-337","source":"Crossref","is-referenced-by-count":0,"title":["System Description: SPASS-FD"],"prefix":"10.1007","author":[{"given":"Matthias","family":"Horbach","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"25_CR1","series-title":"Lecture Notes in Artificial Intelligence","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 (LNAI), vol.\u00a02741, pp. 350\u2013364. Springer, Heidelberg (2003)"},{"key":"25_CR2","first-page":"293","volume-title":"Logic and Data Bases","author":"K.L. Clark","year":"1977","unstructured":"Clark, K.L.: Negation as failure. In: Gallaire, H., Minker, J. (eds.) Logic and Data Bases, pp. 293\u2013322. Plenum Press, New York (1977)"},{"issue":"3-4","key":"25_CR3","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":"25_CR4","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"},{"key":"25_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/11532231_30","volume-title":"Automated Deduction \u2013 CADE-20","author":"C.G. Ferm\u00fcller","year":"2005","unstructured":"Ferm\u00fcller, C.G., Pichler, R.: Model representation via contexts and implicit generalizations. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 409\u2013423. Springer, Heidelberg (2005)"},{"key":"25_CR6","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-642-17511-4_17","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M. Horbach","year":"2010","unstructured":"Horbach, M.: Disunification for ultimately periodic interpretations. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS (LNAI), vol.\u00a06355, pp. 290\u2013311. Springer, Heidelberg (2010)"},{"key":"25_CR7","series-title":"LNCS (LNAI)","first-page":"299","volume-title":"CADE-23","author":"M. Horbach","year":"2011","unstructured":"Horbach, M.: Predicate completion for non-Horn clause sets. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol.\u00a06803, pp. 299\u2013314. Springer, Heidelberg (2011)"},{"key":"25_CR8","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1007\/978-3-642-02959-2_30","volume-title":"Automated Deduction \u2013 CADE-22","author":"M. Horbach","year":"2009","unstructured":"Horbach, M., Weidenbach, C.: Decidability results for saturation-based model building. In: Schmidt, R.A. (ed.) CADE-22. LNCS (LNAI), vol.\u00a05663, pp. 404\u2013420. Springer, Heidelberg (2009)"},{"key":"25_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/978-3-642-04027-6_25","volume-title":"Computer Science Logic","author":"M. Horbach","year":"2009","unstructured":"Horbach, M., Weidenbach, C.: Deciding the inductive validity of \u2200\u2009\u2203\u2009* queries. In: Gr\u00e4del, E., Kahle, R. (eds.) CSL 2009. LNCS, vol.\u00a05771, pp. 332\u2013347. Springer, Heidelberg (2009)"},{"issue":"4","key":"25_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1805950.1805957","volume":"11","author":"M. Horbach","year":"2010","unstructured":"Horbach, M., Weidenbach, C.: Superposition for fixed domains. ACM Transactions on Computational Logic\u00a011(4), 27:1\u201327:35 (2010)","journal-title":"ACM Transactions on Computational Logic"},{"key":"25_CR11","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1016\/B978-044450813-3\/50009-6","volume-title":"Handbook of Automated Reasoning, vol. I","author":"R. Nieuwenhuis","year":"2001","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Handbook of Automated Reasoning, ch.7, vol.\u00a0I, pp. 371\u2013443. Elsevier, Amsterdam (2001)"},{"key":"25_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/BFb0054252","volume-title":"Automated Deduction - CADE-15","author":"N. Peltier","year":"1998","unstructured":"Peltier, N.: System description: An equational constraints solver. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol.\u00a01421, pp. 119\u2013123. Springer, Heidelberg (1998)"},{"issue":"4","key":"25_CR13","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G. Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure. Journal of Automomated Reasoning\u00a043(4), 337\u2013362 (2009)","journal-title":"Journal of Automomated Reasoning"},{"key":"25_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/3-540-48660-7_29","volume-title":"Automated Deduction - CADE-16","author":"C. Weidenbach","year":"1999","unstructured":"Weidenbach, C.: Towards an automatic analysis of security protocols in first-order logic. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 378\u2013382. Springer, Heidelberg (1999)"},{"key":"25_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-02959-2_10","volume-title":"Automated Deduction \u2013 CADE-22","author":"C. Weidenbach","year":"2009","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol.\u00a05663, pp. 140\u2013145. Springer, Heidelberg (2009)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-23"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22438-6_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,30]],"date-time":"2019-03-30T02:48:31Z","timestamp":1553914111000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22438-6_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642224379","9783642224386"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22438-6_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}