{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T16:01:29Z","timestamp":1742918489942,"version":"3.40.3"},"publisher-location":"Cham","reference-count":63,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031107689"},{"type":"electronic","value":"9783031107696"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T00:00:00Z","timestamp":1659312000000},"content-version":"vor","delay-in-days":212,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The importance of subsumption testing for redundancy elimination in first-order logic automatic reasoning is well-known. Although the problem is already NP-complete for first-order clauses, the meanwhile developed test pipelines efficiently decide subsumption in almost all practical cases. We consider subsumption between first-oder clauses of the Bernays-Sch\u00f6nfinkel fragment over linear real arithmetic constraints: BS(LRA). The bottleneck in this setup is deciding implication between the LRA constraints of two clauses. Our new <jats:italic>sample point heuristic<\/jats:italic> preempts expensive implication decisions in about 94% of all cases in benchmarks. Combined with filtering techniques for the first-order BS part of clauses, it results again in an efficient subsumption test pipeline for BS(LRA) clauses.<\/jats:p>","DOI":"10.1007\/978-3-031-10769-6_10","type":"book-chapter","created":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T01:02:56Z","timestamp":1659315776000},"page":"147-168","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["An Efficient Subsumption Test Pipeline for\u00a0BS(LRA) Clauses"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7256-2190","authenticated-orcid":false,"given":"Martin","family":"Bromberger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0391-3430","authenticated-orcid":false,"given":"Lorenz","family":"Leutgeb","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6002-0458","authenticated-orcid":false,"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,8,1]]},"reference":[{"key":"10_CR1","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-319-24246-0_5","volume-title":"Frontiers of Combining Systems","author":"G Alagi","year":"2015","unstructured":"Alagi, G., Weidenbach, C.: NRCL - a model building approach to\u00a0the Bernays-Sch\u00f6nfinkel fragment. In: Lutz, C., Ranise, S. (eds.) FroCoS 2015. LNCS (LNAI), vol. 9322, pp. 69\u201384. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24246-0_5"},{"key":"10_CR2","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). https:\/\/doi.org\/10.1007\/978-3-642-04222-5_5"},{"issue":"2","key":"10_CR3","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994). https:\/\/doi.org\/10.1016\/0304-3975(94)90010-8","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"10_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). https:\/\/doi.org\/10.1093\/logcom\/4.3.217","journal-title":"J. Log. Comput."},{"key":"10_CR5","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/b978-044450813-3\/50004-7","volume-title":"Handbook of Automated Reasoning (in 2 volumes)","author":"L Bachmair","year":"2001","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes), pp. 19\u201399. Elsevier and MIT Press, Cambridge (2001). https:\/\/doi.org\/10.1016\/b978-044450813-3\/50004-7"},{"key":"10_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). https:\/\/doi.org\/10.1007\/BF01190829","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-030-22102-7_2","volume-title":"Description Logic, Theory Combination, and All That","author":"P Baumgartner","year":"2019","unstructured":"Baumgartner, P., Waldmann, U.: Hierarchic superposition revisited. In: Lutz, C., Sattler, U., Tinelli, C., Turhan, A.-Y., Wolter, F. (eds.) Description Logic, Theory Combination, and All That. LNCS, vol. 11560, pp. 15\u201356. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-22102-7_2"},{"volume-title":"Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications","year":"2009","key":"10_CR8","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press, Amsterdam (2009)"},{"key":"10_CR9","unstructured":"Bromberger, M., et al.: A sorted datalog hammer for supervisor verification conditions modulo simple linear arithmetic. CoRR abs\/2201.09769 (2022). https:\/\/arxiv.org\/abs\/2201.09769"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-86205-3_1","volume-title":"Frontiers of Combining Systems","author":"M Bromberger","year":"2021","unstructured":"Bromberger, M., Dragoste, I., Faqeh, R., Fetzer, C., Kr\u00f6tzsch, M., Weidenbach, C.: A datalog hammer for supervisor verification conditions modulo simple linear arithmetic. In: Konev, B., Reger, G. (eds.) FroCoS 2021. LNCS (LNAI), vol. 12941, pp. 3\u201324. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-86205-3_1"},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1007\/978-3-030-67067-2_23","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M Bromberger","year":"2021","unstructured":"Bromberger, M., Fiori, A., Weidenbach, C.: Deciding the Bernays-Schoenfinkel Fragment over bounded difference constraints by simple clause learning over theories. In: Henglein, F., Shoham, S., Vizel, Y. (eds.) VMCAI 2021. LNCS, vol. 12597, pp. 511\u2013533. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-67067-2_23"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-030-29436-6_7","volume-title":"Automated Deduction \u2013 CADE 27","author":"M Bromberger","year":"2019","unstructured":"Bromberger, M., Fleury, M., Schwarz, S., Weidenbach, C.: SPASS-SATT. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 111\u2013122. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_7"},{"key":"10_CR13","doi-asserted-by":"publisher","unstructured":"Bromberger, M., Leutgeb, L., Weidenbach, C.: An Efficient subsumption test pipeline for BS(LRA) clauses (2022). https:\/\/doi.org\/10.5281\/zenodo.6544456. Supplementary Material","DOI":"10.5281\/zenodo.6544456"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-319-40229-1_9","volume-title":"Automated Reasoning","author":"M Bromberger","year":"2016","unstructured":"Bromberger, M., Weidenbach, C.: Fast cube tests for LIA constraint solving. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 116\u2013132. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_9"},{"key":"10_CR15","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N Dershowitz","year":"1982","unstructured":"Dershowitz, N.: Orderings for term-rewriting systems. Theor. Comput. Sci. 17, 279\u2013301 (1982). https:\/\/doi.org\/10.1016\/0304-3975(82)90026-3","journal-title":"Theor. Comput. Sci."},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81\u201394. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_11"},{"key":"10_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-642-24364-6_9","volume-title":"Frontiers of Combining Systems","author":"A Eggers","year":"2011","unstructured":"Eggers, A., Kruglov, E., Kupferschmid, S., Scheibler, K., Teige, T., Weidenbach, C.: Superposition Modulo Non-linear Arithmetic. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS (LNAI), vol. 6989, pp. 119\u2013134. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24364-6_9"},{"key":"10_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1007\/978-3-030-61470-6_25","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles","author":"R Faqeh","year":"2020","unstructured":"Faqeh, R., Fetzer, C., Hermanns, H., Hoffmann, J., Klauck, M., K\u00f6hl, M.A., Steinmetz, M., Weidenbach, C.: towards dynamic dependable systems through evidence-based continuous certification. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12477, pp. 416\u2013439. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61470-6_25"},{"key":"10_CR19","doi-asserted-by":"publisher","unstructured":"Fietzke, A.: Labelled superposition. Ph.D. thesis, Universit\u00e4t des Saarlandes (2014). https:\/\/doi.org\/10.22028\/D291-26569","DOI":"10.22028\/D291-26569"},{"issue":"4","key":"10_CR20","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/s11786-012-0134-5","volume":"6","author":"A Fietzke","year":"2012","unstructured":"Fietzke, A., Weidenbach, C.: Superposition as a decision procedure for timed automata. Math. Comput. Sci. 6(4), 409\u2013425 (2012). https:\/\/doi.org\/10.1007\/s11786-012-0134-5","journal-title":"Math. Comput. Sci."},{"key":"10_CR21","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-030-29436-6_14","volume-title":"Automated Deduction \u2013 CADE 27","author":"A Fiori","year":"2019","unstructured":"Fiori, A., Weidenbach, C.: SCL clause learning from simple models. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 233\u2013249. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_14"},{"key":"10_CR22","unstructured":"Fiori, A., Weidenbach, C.: SCL with theory constraints. CoRR abs\/2003.04627 (2020). https:\/\/arxiv.org\/abs\/2003.04627"},{"issue":"3\u20134","key":"10_CR23","doi-asserted-by":"publisher","first-page":"209","DOI":"10.3233\/sat190012","volume":"1","author":"M Fr\u00e4nzle","year":"2007","unstructured":"Fr\u00e4nzle, M., Herde, C., Teige, T., Ratschan, S., Schubert, T.: Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. J. Satisf. Boolean Model. Comput. 1(3\u20134), 209\u2013236 (2007). https:\/\/doi.org\/10.3233\/sat190012","journal-title":"J. Satisf. Boolean Model. Comput."},{"issue":"2","key":"10_CR24","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1023\/B:JARS.0000029963.64213.ac","volume":"32","author":"H Ganzinger","year":"2004","unstructured":"Ganzinger, H., Nieuwenhuis, R., Nivela, P.: Fast term indexing with coded context trees. J. Autom. Reason. 32(2), 103\u2013120 (2004). https:\/\/doi.org\/10.1023\/B:JARS.0000029963.64213.ac","journal-title":"J. Autom. Reason."},{"key":"10_CR25","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/978-3-030-51074-9_17","volume-title":"Automated Reasoning","author":"B Gleiss","year":"2020","unstructured":"Gleiss, B., Kov\u00e1cs, L., Rath, J.: Subsumption demodulation in first-order theorem proving. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12166, pp. 297\u2013315. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51074-9_17"},{"issue":"2","key":"10_CR26","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/0020-0190(87)90103-7","volume":"24","author":"G Gottlob","year":"1987","unstructured":"Gottlob, G.: Subsumption and implication. Inf. Process. Lett. 24(2), 109\u2013111 (1987). https:\/\/doi.org\/10.1016\/0020-0190(87)90103-7","journal-title":"Inf. Process. Lett."},{"issue":"2","key":"10_CR27","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1145\/3149.214118","volume":"32","author":"G Gottlob","year":"1985","unstructured":"Gottlob, G., Leitsch, A.: On the efficiency of subsumption algorithms. J. ACM 32(2), 280\u2013295 (1985). https:\/\/doi.org\/10.1145\/3149.214118","journal-title":"J. ACM"},{"key":"10_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/3-540-58156-1_37","volume-title":"Automated Deduction \u2014 CADE-12","author":"P Graf","year":"1994","unstructured":"Graf, P.: Extended path-indexing. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 514\u2013528. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58156-1_37"},{"key":"10_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/3-540-59200-8_52","volume-title":"Rewriting Techniques and Applications","author":"P Graf","year":"1995","unstructured":"Graf, P.: Substitution tree indexing. In: Hsiang, J. (ed.) RTA 1995. LNCS, vol. 914, pp. 117\u2013131. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-59200-8_52"},{"key":"10_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61040-5","volume-title":"Term Indexing","year":"1995","unstructured":"Graf, P. (ed.): Term Indexing. LNCS, vol. 1053. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-61040-5"},{"key":"10_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-642-15582-6_18","volume-title":"Mathematical Software \u2013 ICMS 2010","author":"WB Hart","year":"2010","unstructured":"Hart, W.B.: Fast library for number theory: an introduction. In: Fukuda, K., Hoeven, J., Joswig, M., Takayama, N. (eds.) ICMS 2010. LNCS, vol. 6327, pp. 88\u201391. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15582-6_18"},{"key":"10_CR32","unstructured":"Horbach, M., Voigt, M., Weidenbach, C.: The universal fragment of presburger arithmetic with unary uninterpreted predicates is undecidable. CoRR abs\/1703.01212 (2017). http:\/\/arxiv.org\/abs\/1703.01212"},{"key":"10_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/3-540-15976-2_21","volume-title":"Rewriting Techniques and Applications","author":"PW Purdom","year":"1985","unstructured":"Purdom, P.W., Brown, C.A.: Fast many-to-one matching algorithms. In: Jouannaud, J.-P. (ed.) RTA 1985. LNCS, vol. 202, pp. 407\u2013416. Springer, Heidelberg (1985). https:\/\/doi.org\/10.1007\/3-540-15976-2_21"},{"key":"10_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/3-540-61551-2_65","volume-title":"Principles and Practice of Constraint Programming \u2014 CP96","author":"RJ Bayardo","year":"1996","unstructured":"Bayardo, R.J., Schrag, R.: Using CSP look-back techniques to solve exceptionally hard SAT instances. In: Freuder, E.C. (ed.) CP 1996. LNCS, vol. 1118, pp. 46\u201360. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61551-2_65"},{"key":"10_CR35","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). https:\/\/doi.org\/10.1007\/978-3-540-74915-8_19"},{"key":"10_CR36","doi-asserted-by":"publisher","unstructured":"Kruglov, E.: Superposition modulo theory. Ph.D. thesis, Universit\u00e4t des Saarlandes (2013). https:\/\/doi.org\/10.22028\/D291-26547","DOI":"10.22028\/D291-26547"},{"issue":"4","key":"10_CR37","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(4), 427\u2013456 (2012). https:\/\/doi.org\/10.1007\/s11786-012-0135-4","journal-title":"Math. Comput. Sci."},{"issue":"8","key":"10_CR38","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/361082.361093","volume":"17","author":"L Lamport","year":"1974","unstructured":"Lamport, L.: A new solution of dijkstra\u2019s concurrent programming problem. Commun. ACM 17(8), 453\u2013455 (1974). https:\/\/doi.org\/10.1145\/361082.361093","journal-title":"Commun. ACM"},{"key":"10_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"663","DOI":"10.1007\/3-540-52885-7_131","volume-title":"10th International Conference on Automated Deduction","author":"W McCune","year":"1990","unstructured":"McCune, W.: Otter 2.0. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 663\u2013664. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-52885-7_131"},{"issue":"2","key":"10_CR40","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF00245458","volume":"9","author":"W McCune","year":"1992","unstructured":"McCune, W.: Experiments with discrimination-tree indexing and path indexing for term retrieval. J. Autom. Reason. 9(2), 147\u2013167 (1992). https:\/\/doi.org\/10.1007\/BF00245458","journal-title":"J. Autom. Reason."},{"key":"10_CR41","doi-asserted-by":"publisher","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference, DAC 2001, Las Vegas, NV, USA, 18\u201322 June 2001, pp. 530\u2013535. ACM (2001). https:\/\/doi.org\/10.1145\/378239.379017","DOI":"10.1145\/378239.379017"},{"key":"10_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"10_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/3-540-45744-5_19","volume-title":"Automated Reasoning","author":"R Nieuwenhuis","year":"2001","unstructured":"Nieuwenhuis, R., Hillenbrand, T., Riazanov, A., Voronkov, A.: On the evaluation of indexing techniques for theorem proving. In: Gor\u00e9, R., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS, vol. 2083, pp. 257\u2013271. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45744-5_19"},{"key":"10_CR44","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1016\/b978-044450813-3\/50009-6","volume-title":"Handbook of Automated Reasoning (in 2 volumes)","author":"R Nieuwenhuis","year":"2001","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes), pp. 371\u2013443. Elsevier and MIT Press, Cambridge (2001). https:\/\/doi.org\/10.1016\/b978-044450813-3\/50009-6"},{"key":"10_CR45","unstructured":"Ohlbach, H.J.: Abstraction tree indexing for terms. In: 9th European Conference on Artificial Intelligence, ECAI 1990, Stockholm, Sweden, pp. 479\u2013484 (1990)"},{"key":"10_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/3-540-10009-1_19","volume-title":"5th Conference on Automated Deduction Les Arcs, France, July 8\u201311, 1980","author":"RA Overbeek","year":"1980","unstructured":"Overbeek, R.A., Lusk, E.L.: Data structures and control architecture for implementation of theorem-proving programs. In: Bibel, W., Kowalski, R. (eds.) CADE 1980. LNCS, vol. 87, pp. 232\u2013249. Springer, Heidelberg (1980). https:\/\/doi.org\/10.1007\/3-540-10009-1_19"},{"key":"10_CR47","doi-asserted-by":"publisher","first-page":"1853","DOI":"10.1016\/b978-044450813-3\/50028-x","volume-title":"Handbook of Automated Reasoning (in 2 volumes)","author":"IV Ramakrishnan","year":"2001","unstructured":"Ramakrishnan, I.V., Sekar, R.C., Voronkov, A.: Term indexing. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes), pp. 1853\u20131964. Elsevier and MIT Press, Cambridge (2001). https:\/\/doi.org\/10.1016\/b978-044450813-3\/50028-x"},{"key":"10_CR48","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-40006-0_15","volume-title":"Logics in Artificial Intelligence","author":"A Riazanov","year":"2000","unstructured":"Riazanov, A., Voronkov, A.: Partially adaptive code trees. In: Ojeda-Aciego, M., de Guzm\u00e1n, I.P., Brewka, G., Moniz Pereira, L. (eds.) JELIA 2000. LNCS (LNAI), vol. 1919, pp. 209\u2013223. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-40006-0_15"},{"issue":"1\u20132","key":"10_CR49","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1016\/j.ic.2004.10.012","volume":"199","author":"A Riazanov","year":"2005","unstructured":"Riazanov, A., Voronkov, A.: Efficient instance retrieval with standard and relational path indexing. Inf. Comput. 199(1\u20132), 228\u2013252 (2005). https:\/\/doi.org\/10.1016\/j.ic.2004.10.012","journal-title":"Inf. Comput."},{"key":"10_CR50","doi-asserted-by":"publisher","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM, 12(1), 23\u201341 (1965). https:\/\/doi.org\/10.1145\/321250.321253, http:\/\/doi.acm.org\/10.1145\/321250.321253","DOI":"10.1145\/321250.321253"},{"key":"10_CR51","volume-title":"Theory of Linear and Integer Programming","author":"A Schrijver","year":"1999","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. Wiley-Interscience series in discrete mathematics and optimization, Wiley, Hoboken (1999)"},{"key":"10_CR52","unstructured":"Schulz, S.: Simple and efficient clause subsumption with feature vector indexing. In: Proceedings of the IJCAR-2004 Workshop on Empirically Successful First-Order Theorem Proving. Elsevier Science (2004)"},{"key":"10_CR53","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-642-31365-3_37","volume-title":"Automated Reasoning","author":"S Schulz","year":"2012","unstructured":"Schulz, S.: Fingerprint Indexing for Paramodulation and Rewriting. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 477\u2013483. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_37"},{"key":"10_CR54","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-3-642-36675-8_3","volume-title":"Automated Reasoning and Mathematics","author":"S Schulz","year":"2013","unstructured":"Schulz, S.: Simple and efficient clause subsumption with feature vector indexing. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. LNCS (LNAI), vol. 7788, pp. 45\u201367. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36675-8_3"},{"key":"10_CR55","doi-asserted-by":"publisher","unstructured":"Silva, J.P.M., Sakallah, K.A.: GRASP - a new search algorithm for satisfiability. In: Rutenbar, R.A., Otten, R.H.J.M. (eds.) Proceedings of the 1996 IEEE\/ACM International Conference on Computer-Aided Design, ICCAD 1996, San Jose, CA, USA, 10\u201314 November 1996, pp. 220\u2013227. IEEE Computer Society\/ACM (1996). https:\/\/doi.org\/10.1109\/ICCAD.1996.569607","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"10_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/BFb0012858","volume-title":"9th International Conference on Automated Deduction","author":"R Socher","year":"1988","unstructured":"Socher, R.: A subsumption algorithm based on characteristic matrices. In: Lusk, E., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, pp. 573\u2013581. Springer, Heidelberg (1988). https:\/\/doi.org\/10.1007\/BFb0012858"},{"key":"10_CR57","doi-asserted-by":"publisher","unstructured":"Soos, M., Kulkarni, R., Meel, K.S.: $$\\sf CrystalBall$$: gazing in the black box of SAT solving. In: Janota, M., Lynce, I. (eds.) SAT 2019. LNCS, vol. 11628, pp. 371\u2013387. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-24258-9_26","DOI":"10.1007\/978-3-030-24258-9_26"},{"issue":"4","key":"10_CR58","doi-asserted-by":"publisher","first-page":"648","DOI":"10.1145\/321784.321792","volume":"20","author":"RB Stillman","year":"1973","unstructured":"Stillman, R.B.: The concept of weak substitution in theorem-proving. J. ACM 20(4), 648\u2013667 (1973). https:\/\/doi.org\/10.1145\/321784.321792","journal-title":"J. ACM"},{"key":"10_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/BFb0054276","volume-title":"Automated Deduction \u2014 CADE-15","author":"T Tammet","year":"1998","unstructured":"Tammet, T.: Towards efficient subsumption. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS, vol. 1421, pp. 427\u2013441. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0054276"},{"issue":"3","key":"10_CR60","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/s10817-020-09567-8","volume":"65","author":"M Voigt","year":"2020","unstructured":"Voigt, M.: Decidable $${\\exists }^*{\\forall }^*$$ first-order fragments of linear rational arithmetic with uninterpreted predicates. J. Autom. Reason. 65(3), 357\u2013423 (2020). https:\/\/doi.org\/10.1007\/s10817-020-09567-8","journal-title":"J. Autom. Reason."},{"issue":"2","key":"10_CR61","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/BF00881918","volume":"15","author":"A Voronkov","year":"1995","unstructured":"Voronkov, A.: The anatomy of vampire implementing bottom-up procedures with code trees. J. Autom. Reason. 15(2), 237\u2013265 (1995). https:\/\/doi.org\/10.1007\/BF00881918","journal-title":"J. Autom. Reason."},{"key":"10_CR62","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/3-540-45744-5_3","volume-title":"Automated Reasoning","author":"A Voronkov","year":"2001","unstructured":"Voronkov, A.: Algorithms, datastructures, and other issues in efficient automated deduction. In: Gor\u00e9, R., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS, vol. 2083, pp. 13\u201328. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45744-5_3"},{"key":"10_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-319-23506-6_12","volume-title":"Correct System Design","author":"C Weidenbach","year":"2015","unstructured":"Weidenbach, C.: Automated reasoning building blocks. In: Meyer, R., Platzer, A., Wehrheim, H. (eds.) Correct System Design. LNCS, vol. 9360, pp. 172\u2013188. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-23506-6_12"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-10769-6_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T01:13:45Z","timestamp":1659316425000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-10769-6_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031107689","9783031107696"],"references-count":63,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-10769-6_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"1 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 August 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/easychair.org\/smart-program\/FLoC2022\/IJCAR-index.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"85","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"32","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"38% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5.2","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}