{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:22:48Z","timestamp":1770279768712,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642408847","type":"print"},{"value":"9783642408854","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40885-4_14","type":"book-chapter","created":{"date-parts":[[2013,9,11]],"date-time":"2013-09-11T07:20:19Z","timestamp":1378884019000},"page":"198-213","source":"Crossref","is-referenced-by-count":9,"title":["Obtaining Finite Local Theory Axiomatizations via Saturation"],"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":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. ACM Trans. Comput. Log.\u00a010(1) (2009)","DOI":"10.1145\/1459010.1459014"},{"issue":"2","key":"14_CR2","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1016\/S0890-5401(03)00020-8","volume":"183","author":"A. Armando","year":"2003","unstructured":"Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. Inf. Comput.\u00a0183(2), 140\u2013164 (2003)","journal-title":"Inf. Comput."},{"issue":"3","key":"14_CR3","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_CR4","unstructured":"Basin, D., Ganzinger, H.: Complexity analysis based on ordered resolution. In: Proc. 11th IEEE Symposium on Logic in Computer Science (LICS 1996), pp. 456\u2013465. IEEE Computer Society Press (1996)"},{"issue":"1","key":"14_CR5","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1145\/363647.363681","volume":"48","author":"D.A. Basin","year":"2001","unstructured":"Basin, D.A., 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_CR6","unstructured":"Ganzinger, H.: Relating semantic and proof-theoretic concepts for polynomial time decidability of uniform word problems. In: Proc. 16th IEEE Symposium on Logic in Computer Science (LICS 2001), pp. 81\u201392. IEEE Computer Society Press (2001)"},{"key":"14_CR7","unstructured":"Horbach, M.: Superposition-based Decision Procedures for Fixed Domain and Minimal Model Semantics. PhD thesis, Max Planck Institute for Computer Science and Saarland University (2010)"},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"Horbach, M., Sofronie-Stokkermans, V.: Obtaining finite local theory axiomatizations via saturation. Technical Report ATR 93, Sonderforschungsbereich\/Transregio 14 AVACS (2013)","DOI":"10.1007\/978-3-642-40885-4_14"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/978-3-540-87531-4_22","volume-title":"Computer Science Logic","author":"M. Horbach","year":"2008","unstructured":"Horbach, M., Weidenbach, C.: Superposition for fixed domains. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol.\u00a05213, pp. 293\u2013307. Springer, Heidelberg (2008)"},{"key":"14_CR10","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 2009. LNCS (LNAI), vol.\u00a05663, pp. 404\u2013420. Springer, Heidelberg (2009)"},{"key":"14_CR11","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\u2203* queries. In: Gr\u00e4del, E., Kahle, R. (eds.) CSL 2009. LNCS, vol.\u00a05771, pp. 332\u2013347. Springer, Heidelberg (2009)"},{"key":"14_CR12","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_CR13","series-title":"LNAI","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 (LNAI), vol.\u00a06173, pp. 30\u201345. Springer, Heidelberg (2010)"},{"key":"14_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"594","DOI":"10.1007\/11560647_39","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2005","author":"H. Kirchner","year":"2005","unstructured":"Kirchner, H., Ranise, S., Ringeissen, C., Tran, D.-K.: On superposition-based satisfiability procedures and their combination. In: Van Hung, D., Wirsing, M. (eds.) ICTAC 2005. LNCS, vol.\u00a03722, pp. 594\u2013608. Springer, Heidelberg (2005)"},{"key":"14_CR15","unstructured":"Lynch, C., Morawska, B.: Automatic decidability. In: 17th IEEE Symposium on Logic in Computer Science (LICS 2002), pp. 7\u201316. IEEE Comp. Soc. (2002)"},{"issue":"7","key":"14_CR16","doi-asserted-by":"publisher","first-page":"1026","DOI":"10.1016\/j.ic.2011.03.005","volume":"209","author":"C. Lynch","year":"2011","unstructured":"Lynch, C., Ranise, S., Ringeissen, C., Tran, D.-K.: Automatic decidability and combinability. Inf. Comput.\u00a0209(7), 1026\u20131047 (2011)","journal-title":"Inf. Comput."},{"key":"14_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"477","DOI":"10.1007\/3-540-55602-8_186","volume-title":"Automated Deduction - CADE-11","author":"R. Nieuwenhuis","year":"1992","unstructured":"Nieuwenhuis, R., Rubio, A.: Theorem proving with ordering constrained clauses. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 477\u2013491. Springer, Heidelberg (1992)"},{"key":"14_CR18","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_CR19","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_CR20","unstructured":"Tushkanova, E., Ringeissen, C., Giorgetti, A., Kouchnarenko, O.: Automatic decidability: A schematic calculus for theories with counting operators. In: Proceedings the RTA 2013 (to appear, 2013)"},{"key":"14_CR21","doi-asserted-by":"crossref","unstructured":"Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a02, ch. 27, pp. 1965\u20132012. Elsevier (2001)","DOI":"10.1016\/B978-044450813-3\/50029-1"}],"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-642-40885-4_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,17]],"date-time":"2019-05-17T01:01:30Z","timestamp":1558054890000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40885-4_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642408847","9783642408854"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40885-4_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}