{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T03:53:05Z","timestamp":1781927585973,"version":"3.54.5"},"publisher-location":"Cham","reference-count":13,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319242453","type":"print"},{"value":"9783319242460","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-24246-0_1","type":"book-chapter","created":{"date-parts":[[2015,9,19]],"date-time":"2015-09-19T04:20:53Z","timestamp":1442636453000},"page":"3-13","source":"Crossref","is-referenced-by-count":1,"title":["Free Variables and Theories: Revisiting 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,11,12]]},"reference":[{"key":"1_CR1","unstructured":"Backeman, P., R\u00fcmmer, P.: Efficient algorithms for bounded rigid E-Unification. In: Tableaux. LNCS. Springer (to appear, 2015)"},{"key":"1_CR2","unstructured":"Backeman, P., R\u00fcmmer, P.: Theorem proving with bounded rigid E-Unification. In: CADE. LNCS. Springer (to appear, 2015)"},{"key":"1_CR3","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.\u00a01092, pp. 178\u2013190. Springer, Heidelberg (1996)"},{"issue":"1","key":"1_CR4","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\u00a020(1), 47\u201380 (1998)","journal-title":"J. Autom. Reasoning"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Degtyarev, A., Voronkov, A.: Equality reasoning in sequent-based calculi. In: Handbook of Automated Reasoning, vol.\u00a02. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50012-6"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Degtyarev, A., Voronkov, A.: Kanger\u2019s Choices in Automated Reasoning. Springer (2001)","DOI":"10.1007\/978-94-010-0630-9_4"},{"key":"1_CR7","series-title":"Graduate Texts in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2360-3","volume-title":"First-Order Logic and Automated Theorem Proving","author":"M.C. Fitting","year":"1996","unstructured":"Fitting, M.C.: First-Order Logic and Automated Theorem Proving, 2nd edn. Graduate Texts in Computer Science. Springer, Berlin (1996)","edition":"2"},{"key":"1_CR8","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":"1_CR9","series-title":"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":"M.A. 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.\u00a02381, pp. 130\u2013144. Springer, Heidelberg (2002)"},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"Halpern, J.Y.: Presburger arithmetic with unary predicates is $\\Pi_1^1$ complete. Journal of Symbolic Logic 56 (1991)","DOI":"10.2307\/2274706"},{"key":"1_CR11","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-1966, pp. 364\u2013371. Springer, Heidelberg (1983). originally appeared in 1963"},{"key":"1_CR12","series-title":"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.\u00a05330, pp. 274\u2013289. Springer, Heidelberg (2008)"},{"key":"1_CR13","series-title":"CADE-17","first-page":"220","volume-title":"CADE","author":"A. Tiwari","year":"2000","unstructured":"Tiwari, A., Bachmair, L., Rue\u00df, H.: Rigid E-Unification revisited. In: CADE. CADE-17, pp. 220\u2013234. Springer, London (2000)"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24246-0_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,30]],"date-time":"2019-08-30T19:25:00Z","timestamp":1567193100000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24246-0_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319242453","9783319242460"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24246-0_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}