{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,29]],"date-time":"2026-09-29T12:59:38Z","timestamp":1790686778125,"version":"4.1.0"},"publisher-location":"Cham","reference-count":88,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319231648","type":"print"},{"value":"9783319231655","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":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-23165-5_8","type":"book-chapter","created":{"date-parts":[[2015,8,26]],"date-time":"2015-08-26T03:57:43Z","timestamp":1440561463000},"page":"181-204","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["On First-Order Model-Based Reasoning"],"prefix":"10.1007","author":[{"given":"Maria Paola","family":"Bonacina","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ulrich","family":"Furbach","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Viorica","family":"Sofronie-Stokkermans","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,8,27]]},"reference":[{"key":"8_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)"},{"issue":"2","key":"8_CR2","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1006\/jsco.1999.0358","volume":"29","author":"C Aravindan","year":"2000","unstructured":"Aravindan, C., Baumgartner, P.: Theorem proving techniques for view deletion in databases. J. Symbolic Comput. 29(2), 119\u2013148 (2000)","journal-title":"J. Symbolic Comput."},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/978-3-642-36675-8_9","volume-title":"Automated Reasoning and Mathematics: Essays in Memory of William W. McCune","author":"R Arthan","year":"2013","unstructured":"Arthan, R., Oliva, P.: (Dual) Hoops have unique halving. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics: Essays in Memory of William W. McCune. LNCS (LNAI), vol. 7788, pp. 165\u2013180. Springer, Heidelberg (2013)"},{"issue":"3","key":"8_CR4","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. Log. Comput. 4(3), 217\u2013247 (1994)","journal-title":"J. Log. Comput."},{"issue":"6","key":"8_CR5","doi-asserted-by":"publisher","first-page":"1007","DOI":"10.1145\/293347.293352","volume":"45","author":"L Bachmair","year":"1998","unstructured":"Bachmair, L., Ganzinger, H.: Ordered chaining calculi for first-order theories of transitive relations. J. ACM 45(6), 1007\u20131049 (1998)","journal-title":"J. ACM"},{"key":"8_CR6","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":"8_CR7","first-page":"825","volume-title":"Handbook of Satisfiability, chap. 26","author":"C Barrett","year":"2009","unstructured":"Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M., Van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, chap. 26, pp. 825\u2013886. IOS Press, Amsterdam (2009)"},{"key":"8_CR8","unstructured":"Baumgartner, P., Fr\u00f6hlich, P., Furbach, U., Nejdl, W.: Semantically guided theorem proving for diagnosis applications. In: Proceedings of IJCAI-16, vol. 1, pp. 460\u2013465 (1997)"},{"issue":"1","key":"8_CR9","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1142\/S0218213006002552","volume":"15","author":"P Baumgartner","year":"2006","unstructured":"Baumgartner, P., Fuchs, A., Tinelli, C.: Implementing the model evolution calculus. Int. J. Artif. Intell. Tools 15(1), 21\u201352 (2006)","journal-title":"Int. J. Artif. Intell. Tools"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-61630-6_1","volume-title":"Logics in Artificial Intelligence","author":"P Baumgartner","year":"1996","unstructured":"Baumgartner, P., Furbach, U., Niemel\u00e4, I.: Hyper tableaux. In: Alferes, J.J., Moniz Pereira, L., Or\u0142owska, E. (eds.) JELIA 1996. LNCS (LNAI), vol. 1126, pp. 1\u201317. Springer, Heidelberg (1996)"},{"issue":"1","key":"8_CR11","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1093\/logcom\/exn061","volume":"20","author":"P Baumgartner","year":"2008","unstructured":"Baumgartner, P., Furbach, U., Pelzer, B.: The hyper tableaux calculus with equality and an application to finite model computation. J. Logic Comput. 20(1), 77\u2013109 (2008)","journal-title":"J. Logic Comput."},{"issue":"9","key":"8_CR12","doi-asserted-by":"publisher","first-page":"1011","DOI":"10.1016\/j.jsc.2011.12.031","volume":"47","author":"P Baumgartner","year":"2012","unstructured":"Baumgartner, P., Pelzer, B., Tinelli, C.: Model evolution calculus with equality - revised and implemented. J. Symbolic Comput. 47(9), 1011\u20131045 (2012)","journal-title":"J. Symbolic Comput."},{"issue":"4\u20135","key":"8_CR13","doi-asserted-by":"publisher","first-page":"591","DOI":"10.1016\/j.artint.2007.09.005","volume":"172","author":"P Baumgartner","year":"2008","unstructured":"Baumgartner, P., Tinelli, C.: The model evolution calculus as a first-order DPLL method. Artif. Intell. 172(4\u20135), 591\u2013632 (2008)","journal-title":"Artif. Intell."},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-642-02959-2_2","volume-title":"Automated Deduction \u2013 CADE-22","author":"P Baumgartner","year":"2009","unstructured":"Baumgartner, P., Waldmann, U.: Superposition and model evolution combined. In: Schmidt, R.A. (ed.) CADE-22. LNCS (LNAI), vol. 5663, pp. 17\u201334. Springer, Heidelberg (2009)"},{"key":"8_CR15","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-24. LNCS (LNAI), vol. 7898, pp. 39\u201357. Springer, Heidelberg (2013)"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-642-38574-2_8","volume-title":"Automated Deduction \u2013 CADE-24","author":"M Bender","year":"2013","unstructured":"Bender, M., Pelzer, B., Schon, C.: System description: E-KRHyper 1.4 \u2013 Extensions for unique names and description logic. In: Bonacina, M.P. (ed.) CADE-24. LNCS (LNAI), vol. 7898, pp. 126\u2013134. Springer, Heidelberg (2013)"},{"key":"8_CR17","volume-title":"Automated Deduction - A Basis for Applications (in 2 volumes)","year":"1998","unstructured":"Bibel, W., Schmitt, P.H. (eds.): Automated Deduction - A Basis for Applications (in 2 volumes). Kluwer Academic Publishers, Dordrecht (1998)"},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/3-540-48317-9_3","volume-title":"Artificial Intelligence Today - Recent Trends and Developments","author":"MP Bonacina","year":"1999","unstructured":"Bonacina, M.P.: A taxonomy of theorem-proving strategies. In: Veloso, M.M., Wooldridge, M.J. (eds.) Artificial Intelligence Today - Recent Trends and Developments. LNCS (LNAI), vol. 1600, pp. 43\u201384. Springer, Heidelberg (1999)"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Bonacina, M.P.: On theorem proving for program checking - Historical perspective and recent developments. In: Fern\u00e1ndez, M. (eds.): Proceedings of PPDP-12, pp. 1\u201311. ACM Press (2010)","DOI":"10.1145\/1836089.1836090"},{"issue":"2","key":"8_CR20","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1016\/j.jsc.2008.10.008","volume":"45","author":"MP Bonacina","year":"2010","unstructured":"Bonacina, M.P., Echenim, M.: Theory decision by decomposition. J. Symbolic Comput. 45(2), 229\u2013260 (2010)","journal-title":"J. Symbolic Comput."},{"key":"8_CR21","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1016\/0304-3975(94)00187-N","volume":"146","author":"MP Bonacina","year":"1995","unstructured":"Bonacina, M.P., Hsiang, J.: Towards a foundation of completion procedures as semidecision procedures. Theoret. Comput. Sci. 146, 199\u2013242 (1995)","journal-title":"Theoret. Comput. Sci."},{"issue":"2","key":"8_CR22","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/BF03037315","volume":"16","author":"MP Bonacina","year":"1998","unstructured":"Bonacina, M.P., Hsiang, J.: On semantic resolution with lemmaizing and contraction and a formal treatment of caching. New Gener. Comput. 16(2), 163\u2013200 (1998)","journal-title":"New Gener. Comput."},{"issue":"4","key":"8_CR23","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/s10817-015-9325-5","volume":"54","author":"MP Bonacina","year":"2015","unstructured":"Bonacina, M.P., Johansson, M.: Interpolation of ground proofs in automated deduction: a survey. J. Autom. Reasoning 54(4), 353\u2013390 (2015)","journal-title":"J. Autom. Reasoning"},{"issue":"1","key":"8_CR24","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/s10817-014-9314-0","volume":"54","author":"MP Bonacina","year":"2015","unstructured":"Bonacina, M.P., Johansson, M.: On interpolation in automated theorem proving. J. Autom. Reasoning 54(1), 69\u201397 (2015)","journal-title":"J. Autom. Reasoning"},{"issue":"2","key":"8_CR25","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.A., de Moura, L.: On deciding satisfiability by theorem proving with speculative inferences. J. Autom. Reasoning 47(2), 161\u2013189 (2011)","journal-title":"J. Autom. Reasoning"},{"key":"8_CR26","first-page":"47","volume-title":"Proceedings of UNIF-28, RISC Technical Reports","author":"MP Bonacina","year":"2014","unstructured":"Bonacina, M.P., Plaisted, D.A.: Constraint manipulation in SGGS. In: Kutsia, T., Ringeissen, C. (eds.) Proceedings of UNIF-28, RISC Technical Reports, pp. 47\u201354. Johannes Kepler Universit\u00e4t, Linz (2014)"},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"Bonacina, M.P., Plaisted, D.A.: SGGS theorem proving: an exposition. In: Schulz, S., de Moura, L., Konev, B. (eds.) Proceedings of PAAR-4, EasyChair Proceedings in Computing (EPiC), pp. 25\u201338 (2015)","DOI":"10.29007\/m2vf"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"Bonacina, M.P., Plaisted, D.A.: Semantically guided goal-sensitive reasoning: inference system and completeness (2015, in preparation)","DOI":"10.1007\/s10817-015-9334-4"},{"issue":"1","key":"8_CR29","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-015-9322-8","volume":"55","author":"MP Bonacina","year":"2015","unstructured":"Bonacina, M.P., Plaisted, D.A.: Semantically-guided goal-sensitive reasoning: model representation. J. Autom. Reasoning 55(1), 1\u201329 (2015). doi:10.1007\/s10817-015-9334-4","journal-title":"J. Autom. Reasoning"},{"key":"8_CR30","doi-asserted-by":"crossref","unstructured":"Boy de la Tour, T., Echenim, M.: Permutative rewriting and unification. Inf. Comput. 205(4), 624\u2013650 (2007)","DOI":"10.1016\/j.ic.2006.11.001"},{"key":"8_CR31","volume-title":"Symbolic logic and mechanical theorem proving","author":"C-L Chang","year":"1973","unstructured":"Chang, C.-L., Lee, R.C.-T.: Symbolic logic and mechanical theorem proving. Academic Press, New York (1973)"},{"issue":"7","key":"8_CR32","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"key":"8_CR33","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7, 201\u2013215 (1960)","journal-title":"J. ACM"},{"issue":"9","key":"8_CR34","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/1995376.1995394","volume":"54","author":"L de Moura","year":"2011","unstructured":"de Moura, L., Bj\u00f8rner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69\u201377 (2011)","journal-title":"Commun. ACM"},{"key":"8_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-35873-9_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"L de Moura","year":"2013","unstructured":"de Moura, L., Jovanovi\u0107, D.: A model-constructing satisfiability calculus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 1\u201312. Springer, Heidelberg (2013)"},{"key":"8_CR36","first-page":"243","volume-title":"Handbook of Theoretical Computer Science","author":"N Dershowitz","year":"1990","unstructured":"Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 243\u2013320. Elsevier, Amsterdam (1990)"},{"key":"8_CR37","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/j.entcs.2009.05.015","volume":"238","author":"S Escobar","year":"2009","unstructured":"Escobar, S., Meseguer, J., Sasse, R.: Variant narrowing and equational unification. Electron. Notes Theoret. Comput. Sci. 238, 103\u2013119 (2009)","journal-title":"Electron. Notes Theoret. Comput. Sci."},{"key":"8_CR38","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/978-3-642-36675-8_10","volume-title":"Automated Reasoning and Mathematics: Essays in Memory of William W. McCune","author":"B Fitelson","year":"2013","unstructured":"Fitelson, B.: Gibbard\u2019s collapse theorem for the indicative conditional: an axiomatic approach. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics: Essays in Memory of William W. McCune. LNCS (LNAI), vol. 7788, pp. 181\u2013188. Springer, Heidelberg (2013)"},{"key":"8_CR39","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-642-40537-2_13","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"U Furbach","year":"2013","unstructured":"Furbach, U., Schon, C.: Semantically guided evolution of $${\\cal S}{\\cal H}{\\cal I}$$ ABoxes. In: Galmiche, D., Larchey-Wendling, D. (eds.) TABLEAUX 2013. LNCS (LNAI), vol. 8123, pp. 17\u201334. Springer, Heidelbeg (2013)"},{"key":"8_CR40","first-page":"273","volume":"40","author":"JH Gallier","year":"1990","unstructured":"Gallier, J.H., Snyder, W.: Designing unification procedures using transformations: a survey. EATCS Bull. 40, 273\u2013326 (1990)","journal-title":"EATCS Bull."},{"issue":"10","key":"8_CR41","doi-asserted-by":"publisher","first-page":"1453","DOI":"10.1016\/j.ic.2005.10.002","volume":"240","author":"H Ganzinger","year":"2006","unstructured":"Ganzinger, H., Sofronie-Stokkermans, V., Waldmann, U.: Modular proof systems for partial functions with Evans equality. Inf. Comput. 240(10), 1453\u20131492 (2006)","journal-title":"Inf. Comput."},{"key":"8_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/3-540-61511-3_102","volume-title":"Automated Deduction - Cade-13","author":"H Ganzinger","year":"1996","unstructured":"Ganzinger, H., Waldmann, U.: Theorem proving in cancellative abelian monoids. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE-13. LNCS, vol. 1104, pp. 388\u2013402. Springer, Heidelberg (1996)"},{"issue":"4","key":"8_CR43","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1016\/S0747-7171(89)80036-7","volume":"8","author":"J Goguen","year":"1989","unstructured":"Goguen, J., Meseguer, J.: Order-sorted unification. J. Symbolic Comput. 8(4), 383\u2013413 (1989)","journal-title":"J. Symbolic Comput."},{"issue":"2","key":"8_CR44","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(92)90302-V","volume":"105","author":"J Goguen","year":"1992","unstructured":"Goguen, J., Meseguer, J.: Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoret. Comput. Sci. 105(2), 217\u2013273 (1992)","journal-title":"Theoret. Comput. Sci."},{"key":"8_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/978-3-540-32033-3_13","volume-title":"Term Rewriting and Applications","author":"J Hendrix","year":"2005","unstructured":"Hendrix, J., Clavel, M., Meseguer, J.: A sufficient completeness reasoning tool for partial specifications. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 165\u2013174. Springer, Heidelberg (2005)"},{"issue":"3","key":"8_CR46","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/j.entcs.2012.11.010","volume":"290","author":"J Hendrix","year":"2012","unstructured":"Hendrix, J., Meseguer, J.: Order-sorted equational unification revisited. Electron. Notes Theoret. Comput. Sci. 290(3), 37\u201350 (2012)","journal-title":"Electron. Notes Theoret. Comput. Sci."},{"key":"8_CR47","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/11814771_14","volume-title":"Automated Reasoning","author":"J Hendrix","year":"2006","unstructured":"Hendrix, J., Meseguer, J., Ohsaki, H.: A sufficient completeness checker for linear order-sorted specifications modulo axioms. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 151\u2013155. Springer, Heidelberg (2006)"},{"issue":"3","key":"8_CR48","doi-asserted-by":"publisher","first-page":"559","DOI":"10.1145\/116825.116833","volume":"38","author":"J Hsiang","year":"1991","unstructured":"Hsiang, J., Rusinowitch, M.: Proving refutational completeness of theorem proving strategies: the transfinite semantic tree method. J. ACM 38(3), 559\u2013587 (1991)","journal-title":"J. ACM"},{"key":"8_CR49","unstructured":"Hsiang, J., Rusinowitch, M., Sakai, K.: Complete inference rules for the cancellation laws. In: Proceedings of IJCAI-10, pp. 990\u2013992 (1987)"},{"key":"8_CR50","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. 4963, pp. 265\u2013281. Springer, Heidelberg (2008)"},{"key":"8_CR51","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","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. 6173, pp. 30\u201345. Springer, Heidelberg (2010)"},{"key":"8_CR52","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP: a new search algorithm for satisfiability. In: Proceedings of ICCAD 1996, pp. 220\u2013227 (1997)","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"8_CR53","first-page":"257","volume-title":"Computational Logic - Essays in Honor of Alan Robinson","author":"J-P Jouannaud","year":"1991","unstructured":"Jouannaud, J.-P., Kirchner, C.: Solving equations in abstract algebras: a rule-based survey of unification. In: Lassez, J.-L., Plotkin, G. (eds.) Computational Logic - Essays in Honor of Alan Robinson, pp. 257\u2013321. MIT Press, Cambridge (1991)"},{"issue":"4","key":"8_CR54","doi-asserted-by":"publisher","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"J-P Jouannaud","year":"1986","unstructured":"Jouannaud, J.-P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput. 15(4), 1155\u20131194 (1986)","journal-title":"SIAM J. Comput."},{"key":"8_CR55","doi-asserted-by":"crossref","unstructured":"Jovanovi\u0107, D., Barrett, C., de Moura, L.: The design and implementation of the model-constructing satisfiability calculus. In: Jobstman, B., Ray, S. (eds.) Proceedings of FMCAD-13. ACM and IEEE (2013)","DOI":"10.1109\/FMCAD.2013.7027033"},{"key":"8_CR56","doi-asserted-by":"crossref","unstructured":"Kapur, D.: An automated tool for analyzing completeness of equational specifications. In: Proceedings of ISSTA-94, pp. 28\u201343. ACM (1994)","DOI":"10.1145\/186258.186496"},{"issue":"4","key":"8_CR57","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/BF01893885","volume":"28","author":"D Kapur","year":"1991","unstructured":"Kapur, D., Narendran, P., Rosenkrantz, D.J., Zhang, H.: Sufficient-completeness, ground-reducibility and their complexity. Acta Informatica 28(4), 311\u2013350 (1991)","journal-title":"Acta Informatica"},{"key":"8_CR58","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/BF00247825","volume":"9","author":"S-J Lee","year":"1992","unstructured":"Lee, S.-J., Plaisted, D.A.: Eliminating duplication with the hyperlinking strategy. J. Autom. Reasoning 9, 25\u201342 (1992)","journal-title":"J. Autom. Reasoning"},{"key":"8_CR59","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S1574-6526(07)03001-5","volume-title":"Handbook of Knowledge Representation","author":"V Lifschitz","year":"2008","unstructured":"Lifschitz, V., Morgenstern, L., Plaisted, D.A.: Knowledge representation and classical logic. In: van Harmelen, F., Lifschitz, V., Porter, B. (eds.) Handbook of Knowledge Representation, vol. 1, pp. 3\u201388. Elsevier, Amsterdam (2008)"},{"issue":"8","key":"8_CR60","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1145\/1536616.1536637","volume":"52","author":"S Malik","year":"2009","unstructured":"Malik, S., Zhang, L.: Boolean satisfiability: from theoretical hardness to practical success. Commun. ACM 52(8), 76\u201382 (2009)","journal-title":"Commun. ACM"},{"key":"8_CR61","unstructured":"McCune, W.W.: OTTER 3.3 reference manual. Technical Report ANL\/MCS-TM-263, MCS Division, Argonne National Laboratory, Argonne (2003)"},{"key":"8_CR62","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Blaauw, D., Lavagno, L. (eds.) Proceedings of DAC-39, pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"8_CR63","first-page":"201","volume-title":"Automatic Theorem Proving: After 25 Years","author":"G Nelson","year":"1983","unstructured":"Nelson, G.: Combining satisfiability procedures by equality sharing. In: Bledsoe, W.W., Loveland, D.W. (eds.) Automatic Theorem Proving: After 25 Years, pp. 201\u2013211. American Mathematical Society, Providence (1983)"},{"issue":"2","key":"8_CR64","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. 1(2), 245\u2013257 (1979)","journal-title":"ACM Trans. Program. Lang."},{"issue":"6","key":"8_CR65","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"},{"issue":"2","key":"8_CR66","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"GE Peterson","year":"1981","unstructured":"Peterson, G.E., Stickel, M.E.: Complete sets of reductions for some equational theories. J. ACM 28(2), 233\u2013264 (1981)","journal-title":"J. ACM"},{"key":"8_CR67","first-page":"269","volume-title":"Formal Techniques in Artificial Intelligence","author":"DA Plaisted","year":"1990","unstructured":"Plaisted, D.A.: Mechanical theorem proving. In: Banerji, R.B. (ed.) Formal Techniques in Artificial Intelligence, pp. 269\u2013320. Elsevier, Amsterdam (1990)"},{"key":"8_CR68","doi-asserted-by":"crossref","unstructured":"Plaisted, D.A.: Equational reasoning and term rewriting systems. In: Gabbay, D.M., Hogger, C.J., Robinson, J.A. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming. Vol. I: Logical Foundations, pp. 273\u2013364. Oxford University Press, Oxford (1993)","DOI":"10.1093\/oso\/9780198537458.003.0005"},{"issue":"2","key":"8_CR69","first-page":"115","volume":"5","author":"DA Plaisted","year":"2014","unstructured":"Plaisted, D.A.: Automated theorem proving. Wiley Interdisciplinary Reviews: Cognitive Science 5(2), 115\u2013128 (2014)","journal-title":"Wiley Interdisciplinary Reviews: Cognitive Science"},{"key":"8_CR70","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-322-93862-6","volume-title":"The Efficiency of Theorem Proving Strategies","author":"DA Plaisted","year":"1997","unstructured":"Plaisted, D.A., Zhu, Y.: The Efficiency of Theorem Proving Strategies. Friedrich Vieweg & Sohns, Braunschweig (1997)"},{"key":"8_CR71","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1023\/A:1006376231563","volume":"25","author":"DA Plaisted","year":"2000","unstructured":"Plaisted, D.A., Zhu, Y.: Ordered semantic hyper linking. J. Autom. Reasoning 25, 167\u2013217 (2000)","journal-title":"J. Autom. Reasoning"},{"key":"8_CR72","first-page":"73","volume":"7","author":"G Plotkin","year":"1972","unstructured":"Plotkin, G.: Building in equational theories. Mach. Intell. 7, 73\u201390 (1972)","journal-title":"Mach. Intell."},{"key":"8_CR73","first-page":"135","volume":"4","author":"GA Robinson","year":"1969","unstructured":"Robinson, G.A., Wos, L.: Paramodulation and theorem proving in first order theories with equality. Mach. Intell. 4, 135\u2013150 (1969)","journal-title":"Mach. Intell."},{"key":"8_CR74","first-page":"227","volume":"1","author":"JA Robinson","year":"1965","unstructured":"Robinson, J.A.: Automatic deduction with hyper-resolution. Int. J. Comput. Math. 1, 227\u2013234 (1965)","journal-title":"Int. J. Comput. Math."},{"issue":"1","key":"8_CR75","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine oriented logic based on the resolution principle. J. ACM 12(1), 23\u201341 (1965)","journal-title":"J. ACM"},{"key":"8_CR76","volume-title":"Handbook of Automated Reasoning","year":"2001","unstructured":"Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning. Elsevier and MIT Press, Amsterdam (2001)"},{"issue":"1 & 2","key":"8_CR77","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/S0747-7171(08)80131-9","volume":"11","author":"M Rusinowitch","year":"1991","unstructured":"Rusinowitch, M.: Theorem-proving with resolution and superposition. J. Symbolic Comput. 11(1 & 2), 21\u201350 (1991)","journal-title":"J. Symbolic Comput."},{"key":"8_CR78","unstructured":"Shearer, R., Motik, B., Horrocks, I.: HermiT: a highly efficient OWL reasoner. In: Ruttenberg, A., Sattler, U., Dolbear, C. (eds.) Proceedings of OWLED-5, vol. 432 of CEUR (2008)"},{"issue":"4","key":"8_CR79","doi-asserted-by":"publisher","first-page":"687","DOI":"10.1145\/321420.321428","volume":"14","author":"JR Slagle","year":"1967","unstructured":"Slagle, J.R.: Automatic theorem proving with renamable and semantic resolution. J. ACM 14(4), 687\u2013697 (1967)","journal-title":"J. ACM"},{"key":"8_CR80","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"764","DOI":"10.1007\/3-540-58156-1_56","volume-title":"Automated Deduction \u2013 CADE-12","author":"J Slaney","year":"1994","unstructured":"Slaney, J., Lusk, E., McCune, W.: SCOTT: semantically constrained Otter system description. In: Bundy, A. (ed.) CADE-12. LNCS (LNAI), vol. 814, pp. 764\u2013768. Springer, Heidelberg (1994)"},{"key":"8_CR81","series-title":"Lecture Notes in Computer Science (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-20. LNCS (LNAI), vol. 3632, pp. 219\u2013234. Springer, Heidelberg (2005)"},{"key":"8_CR82","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-540-74621-8_3","volume-title":"Frontiers of Combining Systems","author":"V Sofronie-Stokkermans","year":"2007","unstructured":"Sofronie-Stokkermans, V.: Hierarchical and modular reasoning in complex theories: the case of local theory extensions. In: Konev, B., Wolter, F. (eds.) FroCos 2007. LNCS (LNAI), vol. 4720, pp. 47\u201371. Springer, Heidelberg (2007)"},{"key":"8_CR83","doi-asserted-by":"crossref","unstructured":"Sofronie-Stokkermans, V.: Interpolation in local theory extensions. Logical Methods in Computer Science, 4(4), 1\u201331, Paper 1 (2008)","DOI":"10.2168\/LMCS-4(4:1)2008"},{"issue":"1\u20132","key":"8_CR84","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/S0304-3975(98)00082-6","volume":"208","author":"J Stuber","year":"1998","unstructured":"Stuber, J.: Superposition theorem proving for abelian groups represented as integer modules. Theoret. Comput. Sci. 208(1\u20132), 149\u2013177 (1998)","journal-title":"Theoret. Comput. Sci."},{"key":"8_CR85","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/BFb0054257","volume-title":"Automated Deduction - CADE-15","author":"U Waldmann","year":"1998","unstructured":"Waldmann, U.: Superposition for divisible torsion-free abelian groups. In: Kirchner, C., Kirchner, H. (eds.) CADE-15. LNCS (LNAI), vol. 1421, pp. 144\u2013159. Springer, Heidelberg (1998)"},{"key":"8_CR86","doi-asserted-by":"publisher","first-page":"536","DOI":"10.1145\/321296.321302","volume":"12","author":"L Wos","year":"1965","unstructured":"Wos, L., Carson, D., Robinson, G.: Efficiency and completeness of the set of support strategy in theorem proving. J. ACM 12, 536\u2013541 (1965)","journal-title":"J. ACM"},{"key":"8_CR87","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/978-3-642-36675-8_5","volume-title":"Automated Reasoning and Mathematics: Essays in Memory of William W. McCune","author":"H Zhang","year":"2013","unstructured":"Zhang, H., Zhang, J.: MACE4 and SEM: a comparison of finite model generators. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics: Essays in Memory of William W. McCune. LNCS (LNAI), vol. 7788, pp. 101\u2013130. Springer, Heidelberg (2013)"},{"key":"8_CR88","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/3-540-45620-1_26","volume-title":"Automated Deduction - CADE-18","author":"L Zhang","year":"2002","unstructured":"Zhang, L., Malik, S.: The quest for efficient boolean satisfiability solvers. In: Voronkov, A. (ed.) CADE-18. LNCS (LNAI), vol. 2392, pp. 295\u2013313. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Logic, Rewriting, and Concurrency"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-23165-5_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T04:40:00Z","timestamp":1748580000000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-23165-5_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319231648","9783319231655"],"references-count":88,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-23165-5_8","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":"27 August 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}