{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:40:06Z","timestamp":1747593606937,"version":"3.40.5"},"publisher-location":"Cham","reference-count":56,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031634970"},{"type":"electronic","value":"9783031634987"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,1]],"date-time":"2024-07-01T00:00:00Z","timestamp":1719792000000},"content-version":"vor","delay-in-days":182,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Given a finite consistent set of ground literals, we present an algorithm that generates a complete first-order logic interpretation, i.e., an interpretation for all ground literals over the signature and not just those in the input set, that is also a model for the input set. The interpretation is represented by first-order linear literals. It can be effectively used to evaluate clauses. A particular application are SCL stuck states. The SCL (Simple Clause Learning) calculus always computes with respect to a finite number of ground literals. It then finds either a contradiction or a stuck state being a model with respect to the considered ground literals. Our algorithm builds a complete literal interpretation out of such a stuck state model that can then be used to evaluate the clause set. If all clauses are satisfied an overall model has been found. If it does not satisfy some clause, this information can be effectively explored to extend the scope of ground literals considered by SCL.<\/jats:p>","DOI":"10.1007\/978-3-031-63498-7_9","type":"book-chapter","created":{"date-parts":[[2024,6,30]],"date-time":"2024-06-30T19:01:44Z","timestamp":1719774104000},"page":"133-153","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["First-Order Automatic Literal Model Generation"],"prefix":"10.1007","author":[{"given":"Martin","family":"Bromberger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Florent","family":"Krasnopol","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sibylle","family":"M\u00f6hle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,7,1]]},"reference":[{"key":"9_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. Logic 10(1), 4:1\u20134:51 (2009)","DOI":"10.1145\/1459010.1459014"},{"key":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/BFb0022557","volume-title":"Computational Logic and Proof Theory","author":"L Bachmair","year":"1993","unstructured":"Bachmair, L., Ganzinger, H., Waldmann, U.: Superposition with simplification as a decision procedure for the monadic class with equality. In: Gottlob, G., Leitsch, A., Mundici, D. (eds.) KGC 1993. LNCS, vol. 713, pp. 83\u201396. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/BFb0022557"},{"issue":"1","key":"9_CR3","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1016\/j.jal.2007.07.005","volume":"7","author":"P Baumgartner","year":"2009","unstructured":"Baumgartner, P., Fuchs, A., de Nivelle, H., Tinelli, C.: Computing finite models by reduction to function-free clause logic. J. Appl. Log. 7(1), 58\u201374 (2009)","journal-title":"J. Appl. Log."},{"issue":"4","key":"9_CR4","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/s10817-014-9309-x","volume":"53","author":"H Bensaid","year":"2014","unstructured":"Bensaid, H., Peltier, N.: A complete superposition calculus for primal grammars. J. Autom. Reason. 53(4), 317\u2013350 (2014)","journal-title":"J. Autom. Reason."},{"key":"9_CR5","doi-asserted-by":"publisher","unstructured":"Bromberger, M., Desharnais, M., Weidenbach, C.: An Isabelle\/HOL formalization of the SCL(FOL) calculus. In: Pientka, B., Tinelli, C. (eds.) Automated Deduction - CADE 29 - 29th International Conference on Automated Deduction. LNCS, vol. 14132, pp. 116\u2013133. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-38499-8_7","DOI":"10.1007\/978-3-031-38499-8_7"},{"key":"9_CR6","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":"9_CR7","unstructured":"Bromberger, M., Schwarz, S., Weidenbach, C.: Exploring partial models with SCL. In: Konev, B., Schon, C., Steen, A. (eds.) Proceedings of the Workshop on Practical Aspects of Automated Reasoning Co-located with the 11th International Joint Conference on Automated Reasoning (FLoC\/IJCAR 2022), Haifa, Israel, 11 - 12 August 2022. CEUR Workshop Proceedings, vol.\u00a03201 (2022)"},{"key":"9_CR8","doi-asserted-by":"publisher","unstructured":"Bromberger, M., Schwarz, S., Weidenbach, C.: Exploring partial models with SCL. In: Piskac, R., Voronkov, A. (eds.) Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning. EPiC Series in Computing, vol.\u00a094, pp. 48\u201372. EasyChair (2023). https:\/\/doi.org\/10.29007\/8br1","DOI":"10.29007\/8br1"},{"key":"9_CR9","doi-asserted-by":"publisher","unstructured":"Bromberger, M., Schwarz, S., Weidenbach, C.: SCL(FOL) revisited (2023). https:\/\/doi.org\/10.48550\/ARXIV.2302.05954, https:\/\/arxiv.org\/abs\/2302.05954","DOI":"10.48550\/ARXIV.2302.05954"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Caferra, R., Leitsch, A., Peltier, N.: Automated Model Building, Applied Logic Series, vol.\u00a031. Kluwer (2004)","DOI":"10.1007\/978-1-4020-2653-9"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Cantone, D., Cutello, V.: A decidable fragment of the elementary theory of relations and some applications. In: Watanabe, S., Nagata, M. (eds.) Symbolic and Algebraic Computation, Proceedings of the International Symposium, Tokyo, Japan, pp. 24\u201329. ACM Press (August 1990)","DOI":"10.1145\/96877.96887"},{"key":"9_CR12","unstructured":"Claessen, K., Soerensson, N.: New techniques that improve MACE-style finite model finding. In: Proceedings of the CADE-19 Workshop: Model Computation - Principles, Algorithms, Applications (2003)"},{"issue":"1","key":"9_CR13","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/BF01294596","volume":"28","author":"H Comon","year":"1995","unstructured":"Comon, H.: On unification of terms with integer exponents. Math. Syst. Theory 28(1), 67\u201388 (1995)","journal-title":"Math. Syst. Theory"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/3-540-44881-0_12","volume-title":"Rewriting Techniques and Applications","author":"H Comon-Lundh","year":"2003","unstructured":"Comon-Lundh, H., Cortier, V.: New decidability results for fragments of first-order logic and application to cryptographic protocols. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 148\u2013164. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-44881-0_12"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/3-540-54487-9_56","volume-title":"Computer Science Logic","author":"C Ferm\u00fcller","year":"1991","unstructured":"Ferm\u00fcller, C.: A resolution variant deciding some classes of clause sets. In: B\u00f6rger, E., Kleine B\u00fcning, H., Richter, M.M., Sch\u00f6nfeld, W. (eds.) CSL 1990. LNCS, vol. 533, pp. 128\u2013144. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/3-540-54487-9_56"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/3-540-56992-8_10","volume-title":"Computer Science Logic","author":"CG Ferm\u00fcller","year":"1993","unstructured":"Ferm\u00fcller, C.G., Leitsch, A.: Model building by resolution. In: B\u00f6rger, E., J\u00e4ger, G., Kleine B\u00fcning, H., Martini, S., Richter, M.M. (eds.) CSL 1992. LNCS, vol. 702, pp. 134\u2013148. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-56992-8_10"},{"issue":"2","key":"9_CR17","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1093\/logcom\/6.2.173","volume":"6","author":"CG Ferm\u00fcller","year":"1996","unstructured":"Ferm\u00fcller, C.G., Leitsch, A.: Hyperresolution and automated model building. J. Log. Comput. 6(2), 173\u2013203 (1996)","journal-title":"J. Log. Comput."},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Ferm\u00fcller, C.G., Leitsch, A., Hustadt, U., Tamet, T.: Resolution decision procedures. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a0II, chap.\u00a025, pp. 1791\u20131849. Elsevier (2001)","DOI":"10.1016\/B978-044450813-3\/50027-8"},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56732-1","volume-title":"Resolution Methods for the Decision Problem","year":"1993","unstructured":"Ferm\u00fcller, C., Leitsch, A., Tammet, T., Zamov, N. (eds.): Resolution Methods for the Decision Problem. LNCS, vol. 679. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-56732-1"},{"issue":"3","key":"9_CR20","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1093\/logcom\/exm008","volume":"17","author":"CG Ferm\u00fcller","year":"2007","unstructured":"Ferm\u00fcller, C.G., Pichler, R.: Model representation over finite and infinite signatures. J. Log. Comput. 17(3), 453\u2013477 (2007)","journal-title":"J. Log. Comput."},{"key":"9_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":"9_CR22","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., de\u00a0Nivelle, H.: A superposition decision procedure for the guarded fragment with equality. In: LICS, pp. 295\u2013304 (1999)","DOI":"10.1109\/LICS.1999.782624"},{"key":"9_CR23","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). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_25"},{"issue":"2","key":"9_CR24","doi-asserted-by":"publisher","first-page":"195","DOI":"10.3233\/AIC-2011-0496","volume":"24","author":"M Gebser","year":"2011","unstructured":"Gebser, M., Sabuncu, O., Schaub, T.: An incremental answer set programming based system for finite model computation. AI Commun. 24(2), 195\u2013212 (2011)","journal-title":"AI Commun."},{"key":"9_CR25","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/3-540-45620-1_21","volume-title":"Automated Deduction\u2014CADE-18","author":"L Georgieva","year":"2002","unstructured":"Georgieva, L., Hustadt, U., Schmidt, R.A.: A new clausal class decidable by hyperresolution. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 260\u2013274. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45620-1_21"},{"key":"9_CR26","doi-asserted-by":"crossref","unstructured":"Goubault-Larrecq, J.: Deciding $$\\cal{H} _1$$ by resolution. In: Information Processing Letters, pp. 401\u2013408 (2005)","DOI":"10.1016\/j.ipl.2005.04.007"},{"key":"9_CR27","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-642-36675-8_4","volume-title":"Automated Reasoning and Mathematics","author":"T Hillenbrand","year":"2013","unstructured":"Hillenbrand, T., Weidenbach, C.: Superposition for bounded domains. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. LNCS (LNAI), vol. 7788, pp. 68\u2013100. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36675-8_4"},{"key":"9_CR28","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","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. 5663, pp. 404\u2013420. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_30"},{"key":"9_CR29","unstructured":"Hustadt, U., Schmidt, R.A.: On evaluating decision procedures for modal logics. In: Proceedings of 15th International Joint Conference on Artificial Intelligence, IJCAI-97, pp. 202\u2013207 (1997)"},{"key":"9_CR30","first-page":"251","volume":"1","author":"U Hustadt","year":"2004","unstructured":"Hustadt, U., Schmidt, R.A., Georgieva, L.: A survey of decidable first-order fragments and description logics. J. Relational Methods Comput. Sci. 1, 251\u2013276 (2004)","journal-title":"J. Relational Methods Comput. Sci."},{"key":"9_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/BFb0052362","volume-title":"Rewriting Techniques and Applications","author":"F Jacquemard","year":"1998","unstructured":"Jacquemard, F., Meyer, C., Weidenbach, C.: Unification in extensions of shallow equational theories. In: Nipkow, T. (ed.) RTA 1998. LNCS, vol. 1379, pp. 76\u201390. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0052362"},{"key":"9_CR32","doi-asserted-by":"crossref","unstructured":"Janota, M., Suda, M.: Towards smarter MACE-style model finders. In: Barthe, G., Sutcliffe, G., Veanes, M. (eds.) LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, 16-21 November 2018. EPiC Series in Computing, vol.\u00a057, pp. 454\u2013470. EasyChair (2018)","DOI":"10.29007\/w42s"},{"issue":"3","key":"9_CR33","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1145\/321958.321960","volume":"23","author":"WH Joyner Jr","year":"1976","unstructured":"Joyner, W.H., Jr.: Resolution strategies as decision procedures. J. ACM 23(3), 398\u2013417 (1976)","journal-title":"J. ACM"},{"key":"9_CR34","unstructured":"Jr., R.J.B., Schrag, R.: Using CSP look-back techniques to solve real-world SAT instances. In: Kuipers, B., Webber, B.L. (eds.) Proceedings of the Fourteenth National Conference on Artificial Intelligence and Ninth Innovative Applications of Artificial Intelligence Conference, AAAI 97, IAAI 97, 27-31 July 1997, Providence, Rhode Island, USA, pp. 203\u2013208 (1997)"},{"key":"9_CR35","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). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1"},{"issue":"2","key":"9_CR36","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1093\/logcom\/exu074","volume":"27","author":"M Lamotte-Schubert","year":"2017","unstructured":"Lamotte-Schubert, M., Weidenbach, C.: BDI: a new decidable clause class. J. Log. Comput. 27(2), 441\u2013468 (2017)","journal-title":"J. Log. Comput."},{"key":"9_CR37","doi-asserted-by":"publisher","unstructured":"Leidinger, H., Weidenbach, C.: SCL(EQ): SCL for first-order logic with equality. In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) Automated Reasoning - 11th International Joint Conference, IJCAR 2022. LNCS, vol. 13385, pp. 228\u2013247. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_14","DOI":"10.1007\/978-3-031-10769-6_14"},{"key":"9_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/3-540-52753-2_42","volume-title":"CSL \u201989","author":"A Leitsch","year":"1990","unstructured":"Leitsch, A.: Deciding Horn classes by hyperresolution. In: B\u00f6rger, E., B\u00fcning, H.K., Richter, M.M. (eds.) CSL 1989. LNCS, vol. 440, pp. 225\u2013241. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-52753-2_42"},{"key":"9_CR39","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/978-3-540-45085-6_37","volume-title":"Automated Deduction \u2013 CADE-19","author":"C Lynch","year":"2003","unstructured":"Lynch, C.: Schematic saturation for decision and unification problems. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 427\u2013441. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45085-6_37"},{"key":"9_CR40","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability - Second Edition, Frontiers in Artificial Intelligence and Applications, vol.\u00a0336, pp. 133\u2013182. IOS Press (2021)","DOI":"10.3233\/FAIA200987"},{"key":"9_CR41","doi-asserted-by":"crossref","unstructured":"McCune, W.: Mace4 reference manual and guide. CoRR cs.SC\/0310055 (2003)","DOI":"10.2172\/822574"},{"key":"9_CR42","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Design Automation Conference 2001. Proceedings, pp. 530\u2013535. ACM (2001)","DOI":"10.1145\/378239.379017"},{"key":"9_CR43","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R.: Basic paramodulation and decidable theories (extended abstract). In: Proceedings 11th IEEE Symposium on Logic in Computer Science, LICS 1996, pp. 473\u2013482. IEEE Computer Society Press (1996)","DOI":"10.1109\/LICS.1996.561464"},{"issue":"1","key":"9_CR44","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/S0747-7171(02)00092-5","volume":"35","author":"H de Nivelle","year":"2003","unstructured":"de Nivelle, H., de Rijke, M.: Deciding the guarded fragments by resolution. J. Symb. Comput. 35(1), 21\u201358 (2003)","journal-title":"J. Symb. Comput."},{"key":"9_CR45","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/3-540-49545-2_14","volume-title":"Logics in Artificial Intelligence","author":"R Pichler","year":"1998","unstructured":"Pichler, R.: Algorithms on atomic representations of herbrand models. In: Dix, J., del Cerro, L.F., Furbach, U. (eds.) JELIA 1998. LNCS (LNAI), vol. 1489, pp. 199\u2013215. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/3-540-49545-2_14"},{"key":"9_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-642-37651-1_15","volume-title":"Programming Logics","author":"RA Schmidt","year":"2013","unstructured":"Schmidt, R.A., Hustadt, U.: First-order resolution methods for modal logics. In: Voronkov, A., Weidenbach, C. (eds.) Programming Logics. LNCS, vol. 7797, pp. 345\u2013391. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37651-1_15"},{"key":"9_CR47","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/978-3-030-29436-6_29","volume-title":"Automated Deduction \u2013 CADE 27","author":"S Schulz","year":"2019","unstructured":"Schulz, S., Cruanes, S., Vukmirovi\u0107, P.: Faster, higher, stronger: E 2.3. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 495\u2013507. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_29"},{"key":"9_CR48","doi-asserted-by":"crossref","unstructured":"Shumsky, O., Wilkerson, R.W., McCune, W., Er\u00e7al, F.: Direct finite first-order model generation with negative constraint propagation heuristic. In: Bryant, B.R., Carroll, J.H., Oppenheim, D., Hightower, J., George, K.M. (eds.) Proceedings of the 1997 ACM symposium on Applied Computing, SAC 1997, San Jose, CA, USA, 28 February - 1 March, pp. 25\u201329. ACM (1997)","DOI":"10.1145\/331697.331704"},{"key":"9_CR49","unstructured":"Silva, J.P.M., Sakallah, K.A.: Grasp - a new search algorithm for satisfiability. In: International Conference on Computer Aided Design, ICCAD, pp. 220\u2013227. IEEE Computer Society Press (1996)"},{"key":"9_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"798","DOI":"10.1007\/3-540-58156-1_63","volume-title":"Automated Deduction \u2014 CADE-12","author":"J Slaney","year":"1994","unstructured":"Slaney, J.: FINDER: finite domain enumerator system description. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 798\u2013801. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58156-1_63"},{"key":"9_CR51","doi-asserted-by":"crossref","unstructured":"Slaney, J.K., Surendonk, T.: Combining finite model generation with theorem proving: Problems and prospects. In: Baader, F., Schulz, K.U. (eds.) Frontiers of Combining Systems, First International Workshop FroCoS 1996, Munich, Germany, 26-29 March 1996, Proceedings. Applied Logic Series, vol.\u00a03, pp. 141\u2013155. Kluwer Academic Publishers (1996)","DOI":"10.1007\/978-94-009-0349-4_7"},{"key":"9_CR52","doi-asserted-by":"crossref","unstructured":"Sturm, T., Voigt, M., Weidenbach, C.: Deciding first-order satisfiability when universal and existential variables are separated. In: Grohe, M., Koskinen, E., Shankar, N. (eds.) Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2016, New York, USA, 5-8 July 2016, pp. 86\u201395. ACM (2016)","DOI":"10.1145\/2933575.2934532"},{"key":"9_CR53","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/978-3-642-14203-1_38","volume-title":"Automated Reasoning","author":"M Suda","year":"2010","unstructured":"Suda, M., Weidenbach, C., Wischnewski, P.: On the saturation of YAGO. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 441\u2013456. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14203-1_38"},{"key":"9_CR54","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-319-63046-5_13","volume-title":"Automated Deduction \u2013 CADE 26","author":"A Teucke","year":"2017","unstructured":"Teucke, A., Weidenbach, C.: Decidability of the monadic shallow linear first-order fragment with straight dismatching constraints. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 202\u2013219. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_13"},{"key":"9_CR55","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/3-540-48660-7_29","volume-title":"Automated Deduction \u2014 CADE-16","author":"C Weidenbach","year":"1999","unstructured":"Weidenbach, C.: Towards an automatic analysis of security protocols in first-order logic. In: CADE 1999. LNCS (LNAI), vol. 1632, pp. 314\u2013328. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48660-7_29"},{"key":"9_CR56","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). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_10"}],"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-63498-7_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:17:23Z","timestamp":1747592243000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-63498-7_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031634970","9783031634987"],"references-count":56,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-63498-7_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"1 July 2024","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":"Nancy","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/merz.gitlabpages.inria.fr\/2024-ijcar\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}