{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T14:11:40Z","timestamp":1753884700092,"version":"3.40.4"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319085869"},{"type":"electronic","value":"9783319085876"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-08587-6_14","type":"book-chapter","created":{"date-parts":[[2014,7,2]],"date-time":"2014-07-02T03:38:32Z","timestamp":1404272312000},"page":"192-207","source":"Crossref","is-referenced-by-count":3,"title":["Locality Transfer: From Constrained Axiomatizations to Reachability Predicates"],"prefix":"10.1007","author":[{"given":"Matthias","family":"Horbach","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Viorica","family":"Sofronie-Stokkermans","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"14_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. J. of Logic and Computation\u00a04(3), 217\u2013247 (1994)","journal-title":"J. of Logic and Computation"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Basin, D., Ganzinger, H.: Complexity analysis based on ordered resolution. In: Proc. LICS 1996, pp. 456\u2013465. IEEE Computer Society Press (1996)","DOI":"10.1109\/LICS.1996.561462"},{"issue":"1","key":"14_CR3","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1145\/363647.363681","volume":"48","author":"D. Basin","year":"2001","unstructured":"Basin, D., Ganzinger, H.: Automated complexity analysis based on ordered resolution. Journal of the ACM\u00a048(1), 70\u2013109 (2001)","journal-title":"Journal of the ACM"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Ganzinger, H.: Relating semantic and proof-theoretic concepts for polynomial time decidability of uniform word problems. In: Proc. LICS 2001, pp. 81\u201392. IEEE Computer Society Press (2001)","DOI":"10.1109\/LICS.2001.932485"},{"key":"14_CR5","unstructured":"Givan, R., McAllester, D.: New results on local inference relations. In: Principles of Knowledge Representation and Reasoning: Proceedings of the Third International Conference (KR 1992), pp. 403\u2013412. Morgan Kaufmann Press (1992)"},{"key":"14_CR6","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/978-3-642-40885-4_14","volume-title":"Frontiers of Combining Systems","author":"M. Horbach","year":"2013","unstructured":"Horbach, M., Sofronie-Stokkermans, V.: Obtaining finite local theory axiomatizations via saturation. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS (LNAI), vol.\u00a08152, pp. 198\u2013213. Springer, Heidelberg (2013)"},{"key":"14_CR7","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)"},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"Horbach, M., Weidenbach, C.: Superposition for Fixed Domains. ACM Transactions on Computational Logic\u00a011(4), 27:1\u201327:35 (2010)","DOI":"10.1145\/1805950.1805957"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-540-78800-3_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C. Ihlemann","year":"2008","unstructured":"Ihlemann, C., Jacobs, S., Sofronie-Stokkermans, V.: On local reasoning in verification. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 265\u2013281. Springer, Heidelberg (2008)"},{"key":"14_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-642-14203-1_4","volume-title":"Automated Reasoning","author":"C. Ihlemann","year":"2010","unstructured":"Ihlemann, C., Sofronie-Stokkermans, V.: On hierarchical reasoning in combinations of theories. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 30\u201345. Springer, Heidelberg (2010)"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Lev-Ami, T., Immerman, N., Reps, T.W., Sagiv, M., Srivastava, S., Yorsh, G.: Simulating reachability using first-order logic with applications to verification of linked data structures. Logical Methods in Computer Science\u00a05(2) (2009)","DOI":"10.2168\/LMCS-5(2:12)2009"},{"key":"14_CR12","unstructured":"Klaessen, K.: Expressing transitive closure for finite domains in pure first-order logic. Unpublished manuscript"},{"key":"14_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/11532231_16","volume-title":"Automated Deduction \u2013 CADE-20","author":"V. Sofronie-Stokkermans","year":"2005","unstructured":"Sofronie-Stokkermans, V.: Hierarchic reasoning in local theory extensions. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 219\u2013234. Springer, Heidelberg (2005)"},{"key":"14_CR14","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-642-02959-2_5","volume-title":"Automated Deduction \u2013 CADE-22","author":"V. Sofronie-Stokkermans","year":"2009","unstructured":"Sofronie-Stokkermans, V.: Locality results for certain extensions of theories with bridging functions. In: Schmidt, R.A. (ed.) CADE-22. LNCS (LNAI), vol.\u00a05663, pp. 67\u201383. Springer, Heidelberg (2009)"},{"key":"14_CR15","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/978-3-642-22438-6_36","volume-title":"Automated Deduction \u2013 CADE-23","author":"T. Wies","year":"2011","unstructured":"Wies, T., Mu\u00f1iz, M., Kuncak, V.: An efficient decision procedure for imperative tree data structures. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol.\u00a06803, pp. 476\u2013491. Springer, Heidelberg (2011)"},{"key":"14_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-642-27705-4_6","volume-title":"Verified Software: Theories, Tools, Experiments","author":"T. Wies","year":"2012","unstructured":"Wies, T., Mu\u00f1iz, M., Kuncak, V.: Deciding functional lists with sublist sets. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol.\u00a07152, pp. 66\u201381. Springer, Heidelberg (2012)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-08587-6_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T16:40:43Z","timestamp":1746290443000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-08587-6_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319085869","9783319085876"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-08587-6_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}