{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:23:42Z","timestamp":1753889022387},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030221010"},{"type":"electronic","value":"9783030221027"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-22102-7_2","type":"book-chapter","created":{"date-parts":[[2019,6,25]],"date-time":"2019-06-25T12:21:26Z","timestamp":1561465286000},"page":"15-56","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Hierarchic Superposition Revisited"],"prefix":"10.1007","author":[{"given":"Peter","family":"Baumgartner","sequence":"first","affiliation":[]},{"given":"Uwe","family":"Waldmann","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,6,1]]},"reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-642-04222-5_5","volume-title":"Frontiers of Combining Systems","author":"E Althaus","year":"2009","unstructured":"Althaus, E., Kruglov, E., Weidenbach, C.: Superposition modulo linear arithmetic SUP(LA). In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS (LNAI), vol. 5749, pp. 84\u201399. Springer, Heidelberg (2009). \n                    https:\/\/doi.org\/10.1007\/978-3-642-04222-5_5"},{"issue":"1","key":"2_CR2","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1145\/1459010.1459014","volume":"10","author":"A Armando","year":"2009","unstructured":"Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. ACM Trans. Comput. Log. 10(1), 4 (2009)","journal-title":"ACM Trans. Comput. Log."},{"issue":"3","key":"2_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. Logic Comput. 4(3), 217\u2013247 (1994)","journal-title":"J. Logic Comput."},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Handbook of Automated Reasoning. North Holland (2001)","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"key":"2_CR5","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/BF01190829","volume":"5","author":"L Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H., Waldmann, U.: Refutational theorem proving for hierarchic first-order theories. Appl. Algebra Eng. Commun. Comput 5, 193\u2013212 (1994)","journal-title":"Appl. Algebra Eng. Commun. Comput"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). \n                    https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-3-319-21401-6_25","volume-title":"Automated Deduction - CADE-25","author":"P Baumgartner","year":"2015","unstructured":"Baumgartner, P., Bax, J., Waldmann, U.: Beagle \u2013 a hierarchic superposition theorem prover. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 367\u2013377. Springer, Cham (2015). \n                    https:\/\/doi.org\/10.1007\/978-3-319-21401-6_25"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-540-89439-1_19","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P Baumgartner","year":"2008","unstructured":"Baumgartner, P., Fuchs, A., Tinelli, C.: \n                    \n                      \n                    \n                    $$\\cal{ME}$$\n                  (LIA) - model evolution with linear integer arithmetic constraints. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 258\u2013273. Springer, Heidelberg (2008). \n                    https:\/\/doi.org\/10.1007\/978-3-540-89439-1_19"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-642-22438-6_9","volume-title":"Automated Deduction \u2013 CADE-23","author":"P Baumgartner","year":"2011","unstructured":"Baumgartner, P., Tinelli, C.: Model evolution with equality modulo built-in theories. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 85\u2013100. Springer, Heidelberg (2011). \n                    https:\/\/doi.org\/10.1007\/978-3-642-22438-6_9"},{"key":"2_CR10","unstructured":"Baumgartner, P., Waldmann, U.: Hierarchic superposition: completeness without compactness. In: Ko\u0161ta, M., Sturm, T. (eds.), Fifth International Conference on Mathematical Aspects of Computer and Information Sciences, MACIS 2013, pp. 8\u201312, Nanning, China (2013)"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-642-38574-2_3","volume-title":"Automated Deduction \u2013 CADE-24","author":"P Baumgartner","year":"2013","unstructured":"Baumgartner, P., Waldmann, U.: Hierarchic superposition with weak abstraction. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 39\u201357. Springer, Heidelberg (2013). \n                    https:\/\/doi.org\/10.1007\/978-3-642-38574-2_3"},{"key":"2_CR12","unstructured":"Baumgartner, P., Waldmann, U.: Hierarchic superposition revisited (2019). \n                    http:\/\/arxiv.org\/abs\/1904.03776"},{"issue":"2","key":"2_CR13","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/s10817-010-9213-y","volume":"47","author":"MP Bonacina","year":"2011","unstructured":"Bonacina, M.P., Lynch, C., de Moura, L.M.: On deciding satisfiability by theorem proving with speculative inferences. J. Autom. Reason. 47(2), 161\u2013189 (2011)","journal-title":"J. Autom. Reason."},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/978-3-540-71070-7_40","volume-title":"Automated Reasoning","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Engineering DPLL(T) + saturation. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 475\u2013490. Springer, Heidelberg (2008). \n                    https:\/\/doi.org\/10.1007\/978-3-540-71070-7_40"},{"issue":"4","key":"2_CR15","doi-asserted-by":"publisher","first-page":"413","DOI":"10.2307\/2370405","volume":"35","author":"LE Dickson","year":"1913","unstructured":"Dickson, L.E.: Finiteness of the odd perfect and primitive abundant numbers with \n                    \n                      \n                    \n                    $$n$$\n                   distinct prime factors. Am. J. Math. 35(4), 413\u2013422 (1913)","journal-title":"Am. J. Math."},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/11916277_34","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"H Ganzinger","year":"2006","unstructured":"Ganzinger, H., Korovin, K.: Theory instantiation. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 497\u2013511. Springer, Heidelberg (2006). \n                    https:\/\/doi.org\/10.1007\/11916277_34"},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-540-73595-3_12","volume-title":"Automated Deduction \u2013 CADE-21","author":"Y Ge","year":"2007","unstructured":"Ge, Y., Barrett, C., Tinelli, C.: Solving quantified verification conditions using satisfiability modulo theories. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 167\u2013182. Springer, Heidelberg (2007). \n                    https:\/\/doi.org\/10.1007\/978-3-540-73595-3_12"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-642-02658-4_25","volume-title":"Computer Aided Verification","author":"Y Ge","year":"2009","unstructured":"Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306\u2013320. Springer, Heidelberg (2009). \n                    https:\/\/doi.org\/10.1007\/978-3-642-02658-4_25"},{"key":"2_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-540-74915-8_19","volume-title":"Computer Science Logic","author":"K Korovin","year":"2007","unstructured":"Korovin, K., Voronkov, A.: Integrating linear arithmetic into superposition calculus. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 223\u2013237. Springer, Heidelberg (2007). \n                    https:\/\/doi.org\/10.1007\/978-3-540-74915-8_19"},{"key":"2_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Computer Aided Verification","author":"L Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1\u201335. Springer, Heidelberg (2013). \n                    https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1"},{"key":"2_CR21","unstructured":"Kruglov, E.: Superposition modulo theory. Doctoral dissertation, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, October 2013"},{"key":"2_CR22","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/s11786-012-0135-4","volume":"6","author":"E Kruglov","year":"2012","unstructured":"Kruglov, E., Weidenbach, C.: Superposition decides the first-order logic fragment over ground theories. Math. Comput. Sci. 6, 427\u2013456 (2012)","journal-title":"Math. Comput. Sci."},{"key":"2_CR23","unstructured":"Nieuwenhuis, R.: First-order completion techniques. Technical report, Universidad Polit\u00e9cnica de Catalu\u00f1a, Dept. Lenguajes y Sistemas Inform\u00e1ticos (1991)"},{"issue":"6","key":"2_CR24","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937\u2013977 (2006)","journal-title":"J. ACM"},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Handbook of Automated Reasoning, pp. 371\u2013443. Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"2_CR26","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). \n                    https:\/\/doi.org\/10.1007\/978-3-540-89439-1_20"},{"issue":"4","key":"2_CR27","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/s10817-017-9407-7","volume":"59","author":"G Sutcliffe","year":"2017","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0. J. Autom. Reason. 59(4), 483\u2013502 (2017)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"2_CR28","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/42267.45071","volume":"35","author":"C Walther","year":"1988","unstructured":"Walther, C.: Many-sorted unification. J. ACM 35(1), 1\u201317 (1988)","journal-title":"J. ACM"},{"key":"2_CR29","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-02959-2_10","volume-title":"Automated Deduction \u2013 CADE-22","author":"C Weidenbach","year":"2009","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 140\u2013145. Springer, Heidelberg (2009). \n                    https:\/\/doi.org\/10.1007\/978-3-642-02959-2_10"}],"container-title":["Lecture Notes in Computer Science","Description Logic, Theory Combination, and All That"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-22102-7_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,25]],"date-time":"2019-06-25T12:21:43Z","timestamp":1561465303000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-22102-7_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030221010","9783030221027"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-22102-7_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"1 June 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}