{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,6]],"date-time":"2026-10-06T21:11:13Z","timestamp":1791321073606,"version":"4.3.1"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319214009","type":"print"},{"value":"9783319214016","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21401-6_39","type":"book-chapter","created":{"date-parts":[[2015,7,24]],"date-time":"2015-07-24T06:13:46Z","timestamp":1437718426000},"page":"572-587","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Theorem Proving with Bounded Rigid E-Unification"],"prefix":"10.1007","author":[{"given":"Peter","family":"Backeman","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Philipp","family":"R\u00fcmmer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,7,25]]},"reference":[{"issue":"2","key":"39_CR1","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1023\/B:JARS.0000009518.26415.49","volume":"31","author":"L Bachmair","year":"2003","unstructured":"Bachmair, L., Tiwari, A., Vigneron, L.: Abstract congruence closure. J. Autom. Reasoning 31(2), 129\u2013168 (2003)","journal-title":"J. Autom. Reasoning"},{"key":"39_CR2","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"492","DOI":"10.1007\/978-3-540-73595-3_36","volume-title":"Automated Deduction \u2013 CADE-21","author":"P Baumgartner","year":"2007","unstructured":"Baumgartner, P., Furbach, U., Pelzer, B.: Hyper tableaux with equality. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 492\u2013507. Springer, Heidelberg (2007)"},{"key":"39_CR3","volume-title":"Handbook of Tableau Methods","author":"B Beckert","year":"1999","unstructured":"Beckert, B.: Equality and other theories. In: D\u2019Agostino, M., Gabbay, D., H\u00e4hnle, R., Posegga, J. (eds.) Handbook of Tableau Methods. Kluwer, Dordrecht (1999)"},{"key":"39_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/3-540-61377-3_38","volume-title":"Computer Science Logic","author":"A Degtyarev","year":"1996","unstructured":"Degtyarev, A., Voronkov, A.: Simultaneous rigid E-Unification is undecidable. In: Kleine B\u00fcning, H. (ed.) CSL 1995. LNCS, vol. 1092, pp. 178\u2013190. Springer, Heidelberg (1996)"},{"issue":"1","key":"39_CR5","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1023\/A:1005996623714","volume":"20","author":"A Degtyarev","year":"1998","unstructured":"Degtyarev, A., Voronkov, A.: What you always wanted to know about rigid E-Unification. J. Autom. Reasoning 20(1), 47\u201380 (1998)","journal-title":"J. Autom. Reasoning"},{"key":"39_CR6","doi-asserted-by":"crossref","unstructured":"Degtyarev, A., Voronkov, A.: Equality reasoning in sequent-based calculi. In: Handbook of Automated Reasoning (in 2 volumes). Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50012-6"},{"key":"39_CR7","volume-title":"Kanger\u2019s Choices in Automated Reasoning","author":"A Degtyarev","year":"2001","unstructured":"Degtyarev, A., Voronkov, A.: Kanger\u2019s Choices in Automated Reasoning. Springer, The Netherlands (2001)"},{"key":"39_CR8","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2360-3","volume-title":"First-Order Logic and Automated Theorem Provin. Graduate Texts in Computer Science","author":"MC Fitting","year":"1996","unstructured":"Fitting, M.C.: First-Order Logic and Automated Theorem Provin. Graduate Texts in Computer Science, 2nd edn. Springer-Verlag, Berlin (1996)","edition":"2"},{"key":"39_CR9","unstructured":"Gallier, J.H., Raatz, S., Snyder, W.: Theorem proving using rigid e-unification equational matings. In: LICS. pp. 338\u2013346. IEEE Computer Society (1987)"},{"key":"39_CR10","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1007\/3-540-45744-5_46","volume-title":"Automated Reasoning","author":"MA Giese","year":"2001","unstructured":"Giese, M.A.: Incremental closure of free variable tableaux. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 545\u2013560. Springer, Heidelberg (2001)"},{"key":"39_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/3-540-45616-3_10","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"MA Giese","year":"2002","unstructured":"Giese, M.A.: A model generation style completeness proof for constraint tableaux with superposition. In: Egly, U., Ferm\u00fcller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol. 2381, pp. 130\u2013144. Springer, Heidelberg (2002)"},{"key":"39_CR12","doi-asserted-by":"crossref","unstructured":"Giese, M.: Simplification rules for constrained formula tableaux. In: TABLEAUX, pp. 65\u201380 (2003)","DOI":"10.1007\/978-3-540-45206-5_8"},{"key":"39_CR13","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/978-3-642-81952-0_23","volume-title":"Automation of Reasoning 1: Classical Papers on Computational Logic 1957\u20131966","author":"S Kanger","year":"1983","unstructured":"Kanger, S.: A simplified proof method for elementary logic. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning 1: Classical Papers on Computational Logic 1957\u20131966, pp. 364\u2013371. Springer, Heidelberg (1983). originally appeared in 1963"},{"key":"39_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-540-89439-1_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P R\u00fcmmer","year":"2008","unstructured":"R\u00fcmmer, P.: A constraint sequent calculus for first-order logic with linear integer arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 274\u2013289. Springer, Heidelberg (2008)"},{"key":"39_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-642-28717-6_28","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P R\u00fcmmer","year":"2012","unstructured":"R\u00fcmmer, P.: E-matching with free variables. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol. 7180, pp. 359\u2013374. Springer, Heidelberg (2012)"},{"key":"39_CR16","doi-asserted-by":"crossref","unstructured":"Tiwari, A., Bachmair, L., Rue\u00df, H.: Rigid E-Unification revisited. In: CADE. pp. 220\u2013234, CADE-17. Springer-Verlag, London (2000)","DOI":"10.1007\/10721959_17"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-25"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21401-6_39","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,15]],"date-time":"2023-02-15T08:27:10Z","timestamp":1676449630000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-21401-6_39"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319214009","9783319214016"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21401-6_39","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"25 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}