{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T23:57:02Z","timestamp":1743119822251,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540875307"},{"type":"electronic","value":"9783540875314"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-87531-4_22","type":"book-chapter","created":{"date-parts":[[2008,8,30]],"date-time":"2008-08-30T08:40:53Z","timestamp":1220085653000},"page":"293-307","source":"Crossref","is-referenced-by-count":3,"title":["Superposition for Fixed Domains"],"prefix":"10.1007","author":[{"given":"Matthias","family":"Horbach","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"22_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":"22_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/BFb0022557","volume-title":"Computational Logic and Proof Theory","author":"L. Bachmair","year":"1993","unstructured":"Bachmair, L., Ganzinger, H., Waldmann, U.: Superposition with simplification as a decision procedure for the monadic class with equality. In: Mundici, D., Gottlob, G., Leitsch, A. (eds.) KGC 1993. LNCS, vol.\u00a0713, pp. 83\u201396. Springer, Heidelberg (1993)"},{"issue":"1","key":"22_CR3","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1006\/jsco.1996.0076","volume":"23","author":"A. Bouhoula","year":"1997","unstructured":"Bouhoula, A.: Automated theorem proving by test set induction. J. Symb. Comp.\u00a023(1), 47\u201377 (1997)","journal-title":"J. Symb. Comp."},{"issue":"6","key":"22_CR4","doi-asserted-by":"publisher","first-page":"613","DOI":"10.1016\/S0747-7171(10)80014-8","volume":"13","author":"R. Caferra","year":"1992","unstructured":"Caferra, R., Zabel, N.: A method for simultanous search for refutations and models by equational constraint solving. J. Symb. Comp.\u00a013(6), 613\u2013642 (1992)","journal-title":"J. Symb. Comp."},{"issue":"3-4","key":"22_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":"22_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"},{"key":"22_CR7","first-page":"295","volume-title":"Proc. of LICS 1999","author":"H. Ganzinger","year":"1999","unstructured":"Ganzinger, H., Nivelle, H.D.: A superposition decision procedure for the guarded fragment with equality. In: Proc. of LICS 1999, pp. 295\u2013305. IEEE, Los Alamitos (1999)"},{"key":"22_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"226","DOI":"10.1007\/3-540-56393-8_17","volume-title":"Conditional Term Rewriting Systems","author":"H. Ganzinger","year":"1993","unstructured":"Ganzinger, H., Stuber, J.: Inductive theorem proving by consistency for first-order clauses. In: Rusinowitch, M., Remy, J.-L. (eds.) CTRS 1992. LNCS, vol.\u00a0656, pp. 226\u2013241. Springer, Heidelberg (1993)"},{"key":"22_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/BFb0052362","volume-title":"Rewriting Techniques and Applications","author":"F. Jacquemard","year":"1998","unstructured":"Jacquemard, F., Meyer, C., Weidenbach, C.: Unification in extensions of shallow equational theories. In: Nipkow, T. (ed.) RTA 1998. LNCS, vol.\u00a01379, pp. 76\u201390. Springer, Heidelberg (1998)"},{"key":"22_CR10","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1007\/11814771_45","volume-title":"Automated Reasoning","author":"F. Jacquemard","year":"2006","unstructured":"Jacquemard, F., Rusinowitch, M., Vigneron, L.: Tree automata with equality constraints modulo equational theories. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 557\u2013571. Springer, Heidelberg (2006)"},{"issue":"1\/2","key":"22_CR11","first-page":"81","volume":"11","author":"D. Kapur","year":"1991","unstructured":"Kapur, D., Narendran, P., Zhang, H.: Automating inductionless induction using test sets. Journal of Symbolic Computation\u00a011(1\/2), 81\u2013111 (1991)","journal-title":"Journal of Symbolic Computation"},{"key":"22_CR12","first-page":"473","volume-title":"Proc. of LICS 1996","author":"R. Nieuwenhuis","year":"1996","unstructured":"Nieuwenhuis, R.: Basic paramodulation and decidable theories (extended abstract). In: Proc. of LICS 1996, pp. 473\u2013482. IEEE Computer Society Press, Los Alamitos (1996)"},{"key":"22_CR13","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: Handbook of Automated Reasoning, ch. 7, vol.\u00a0I, pp. 371\u2013443. Elsevier, Amsterdam (2001)"},{"issue":"1-2","key":"22_CR14","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/S0747-7171(03)00028-2","volume":"36","author":"N. Peltier","year":"2003","unstructured":"Peltier, N.: Model building with ordered resolution: extracting models from saturated clause sets. Journal of Symbolic Computation\u00a036(1-2), 5\u201348 (2003)","journal-title":"Journal of Symbolic Computation"},{"key":"22_CR15","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. 314\u2013328. Springer, Heidelberg (1999)"},{"key":"22_CR16","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: Handbook of Automated Reasoning, ch. 27, vol.\u00a02, pp. 1965\u20132012. Elsevier, Amsterdam (2001)"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-87531-4_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,7]],"date-time":"2024-05-07T05:13:30Z","timestamp":1715058810000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-540-87531-4_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540875307","9783540875314"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-87531-4_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}