{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T00:05:20Z","timestamp":1759017920517,"version":"3.44.0"},"publisher-location":"Cham","reference-count":60,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032060846","type":"print"},{"value":"9783032060853","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,9,25]],"date-time":"2025-09-25T00:00:00Z","timestamp":1758758400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,9,25]],"date-time":"2025-09-25T00:00:00Z","timestamp":1758758400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Commonly used proof strategies by automated reasoners organise proof search either by ordering-based saturation or by reducing goals to subgoals. In this paper, we combine these two approaches and advocate a SAT-based method with symmetry breaking for connection calculi in first-order logic, with the purpose of further pushing the automation in first-order classical logic proofs. In contrast to classical ways of reducing first-order logic to propositional logic, our method encodes the structure of the proof search itself. We present three distinct SAT encodings for connection calculi, analyse their theoretical properties, and discuss the effect of using SAT\/SMT solvers on these encodings. We implemented our work in the new solver <jats:sc>UPCoP<\/jats:sc> and showcase its practical feasibility.<\/jats:p>","DOI":"10.1007\/978-3-032-06085-3_5","type":"book-chapter","created":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T10:45:20Z","timestamp":1758969920000},"page":"82-102","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Finding Connections via\u00a0Satisfiability Solving"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0339-1580","authenticated-orcid":false,"given":"Clemens","family":"Eisenhofer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7834-1567","authenticated-orcid":false,"given":"Michael","family":"Rawson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8299-2714","authenticated-orcid":false,"given":"Laura","family":"Kov\u00e1cs","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,9,25]]},"reference":[{"issue":"5","key":"5_CR1","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1109\/TC.2006.75","volume":"55","author":"FA Aloul","year":"2006","unstructured":"Aloul, F.A., Sakallah, K.A., Markov, I.L.: Efficient symmetry breaking for Boolean satisfiability. IEEE Trans. Comput. 55(5), 549\u2013558 (2006). https:\/\/doi.org\/10.1109\/TC.2006.75","journal-title":"IEEE Trans. Comput."},{"issue":"3","key":"5_CR2","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/BF00248320","volume":"5","author":"PB Andrews","year":"1989","unstructured":"Andrews, P.B.: On connections and higher-order logic. J. Autom. Reason. 5(3), 257\u2013291 (1989). https:\/\/doi.org\/10.1007\/BF00248320","journal-title":"J. Autom. Reason."},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)","DOI":"10.1017\/CBO9781139172752"},{"key":"5_CR4","doi-asserted-by":"publisher","unstructured":"Baaz, M., Egly, U., Leitsch, A.: Normal form transformations. In: Handbook of Automated Reasoning (in 2 volumes), pp. 273\u2013333. Elsevier and MIT Press (2001). https:\/\/doi.org\/10.1016\/B978-044450813-3\/50007-2","DOI":"10.1016\/B978-044450813-3\/50007-2"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-45193-8_8","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2003","author":"O Bailleux","year":"2003","unstructured":"Bailleux, O., Boufkhad, Y.: Efficient CNF encoding of boolean cardinality constraints. In: Rossi, F. (ed.) CP 2003. LNCS, vol. 2833, pp. 108\u2013122. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45193-8_8"},{"key":"5_CR6","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The satisfiability modulo theories library (SMT-LIB) (2016). https:\/\/www.SMT-LIB.org"},{"issue":"1\u20132","key":"5_CR7","doi-asserted-by":"publisher","first-page":"21","DOI":"10.3233\/SAT190028","volume":"3","author":"CW Barrett","year":"2007","unstructured":"Barrett, C.W., Shikanian, I., Tinelli, C.: An abstract decision procedure for a theory of inductive data types. J. Satisf. Boolean Model. Comput. 3(1\u20132), 21\u201346 (2007). https:\/\/doi.org\/10.3233\/SAT190028","journal-title":"J. Satisf. Boolean Model. Comput."},{"issue":"1","key":"5_CR8","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/S13218-010-0002-X","volume":"24","author":"P Baumgartner","year":"2010","unstructured":"Baumgartner, P., Thorstensen, E.: Instance based methods - a brief overview. K\u00fcnstliche Intell. 24(1), 35\u201342 (2010). https:\/\/doi.org\/10.1007\/S13218-010-0002-X","journal-title":"K\u00fcnstliche Intell."},{"issue":"11","key":"5_CR9","doi-asserted-by":"publisher","first-page":"844","DOI":"10.1145\/182.183","volume":"26","author":"W Bibel","year":"1983","unstructured":"Bibel, W.: Matings in matrices. Commun. ACM 26(11), 844\u2013852 (1983). https:\/\/doi.org\/10.1145\/182.183","journal-title":"Commun. ACM"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Bibel, W.: Automated theorem proving. Artificial intelligence, Vieweg, 2., rev. ed. edn. (1987)","DOI":"10.1007\/978-3-322-90102-6"},{"key":"5_CR11","unstructured":"Bibel, W.: Comparison of proof methods. In: AReCCa, pp. 119\u2013132 (2023). https:\/\/ceur-ws.org\/Vol-3613\/"},{"key":"5_CR12","unstructured":"Biere, A., Fazekas, K., Fleury, M., Heisinger, M.: CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In: Proceedings of SAT Competition 2020 \u2013 Solver and Benchmark Descriptions, pp. 51\u201353. Department of Computer Science Report Series B, University of Helsinki (2020)"},{"key":"5_CR13","doi-asserted-by":"publisher","unstructured":"Biere, A., Froleyks, N., Wang, W.: CadiBack: extracting backbones with CaDiCaL. In: SAT. LIPIcs, vol.\u00a0271, pp. 3:1\u20133:12 (2023). https:\/\/doi.org\/10.4230\/LIPICS.SAT.2023.3","DOI":"10.4230\/LIPICS.SAT.2023.3"},{"key":"5_CR14","doi-asserted-by":"publisher","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability - Second Edition, Frontiers in Artificial Intelligence and Applications, vol.\u00a0336. IOS Press (2021). https:\/\/doi.org\/10.3233\/FAIA336","DOI":"10.3233\/FAIA336"},{"key":"5_CR15","doi-asserted-by":"publisher","unstructured":"Bj\u00f8rner, N.S., Eisenhofer, C., Kov\u00e1cs, L.: Satisfiability modulo custom theories in Z3. In: VMCAI. LNCS, vol. 13881, pp. 91\u2013105 (2023). https:\/\/doi.org\/10.1007\/978-3-031-24950-1_5","DOI":"10.1007\/978-3-031-24950-1_5"},{"key":"5_CR16","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","author":"MP Bonacina","year":"1999","unstructured":"Bonacina, M.P.: A taxonomy of theorem-proving strategies. In: Wooldridge, M.J., Veloso, M. (eds.) Artificial Intelligence Today. LNCS (LNAI), vol. 1600, pp. 43\u201384. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48317-9_3"},{"key":"5_CR17","doi-asserted-by":"publisher","unstructured":"Bongio, J., Katrak, C., Lin, H., Lynch, C., McGregor, R.E.: Encoding first order proofs in SMT. In: SMT. ENTCS, vol.\u00a0198, pp. 71\u201384 (2007). https:\/\/doi.org\/10.1016\/J.ENTCS.2008.04.081","DOI":"10.1016\/J.ENTCS.2008.04.081"},{"issue":"4","key":"5_CR18","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1137\/0204036","volume":"4","author":"D Brand","year":"1975","unstructured":"Brand, D.: Proving theorems with the modification method. SIAM J. Comput. 4(4), 412\u2013430 (1975). https:\/\/doi.org\/10.1137\/0204036","journal-title":"SIAM J. Comput."},{"key":"5_CR19","doi-asserted-by":"publisher","unstructured":"Brown, C.E., Kaliszyk, C.: Lash 1.0 (system description). CoRR abs\/2205.06640 (2022). https:\/\/doi.org\/10.48550\/ARXIV.2205.06640","DOI":"10.48550\/ARXIV.2205.06640"},{"key":"5_CR20","doi-asserted-by":"publisher","unstructured":"Chai, D., Kuehlmann, A.: A fast pseudo-Boolean constraint solver. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 24(3), 305\u2013317 (2005). https:\/\/doi.org\/10.1109\/TCAD.2004.842808","DOI":"10.1109\/TCAD.2004.842808"},{"key":"5_CR21","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1613\/JAIR.3196","volume":"40","author":"A Cimatti","year":"2011","unstructured":"Cimatti, A., Griggio, A., Sebastiani, R.: Computing small unsatisfiable cores in satisfiability modulo theories. J. Artif. Intell. Res. 40, 701\u2013728 (2011). https:\/\/doi.org\/10.1613\/JAIR.3196","journal-title":"J. Artif. Intell. Res."},{"key":"5_CR22","unstructured":"Claessen, K., S\u00f6rensson, N.: New techniques that improve MACE-style finite model finding. In: Proceedings of the CADE-19 Workshop: Model Computation-Principles, Algorithms, Applications, pp. 11\u201327 (2003)"},{"issue":"5","key":"5_CR23","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"EM Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752\u2013794 (2003). https:\/\/doi.org\/10.1145\/876638.876643","journal-title":"J. ACM"},{"key":"5_CR24","doi-asserted-by":"publisher","unstructured":"Coutelier, R., Kov\u00e1cs, L., Rawson, M., Rath, J.: SAT-based subsumption resolution. In: CADE. LNCS, vol. 14132, pp. 190\u2013206 (2023). https:\/\/doi.org\/10.1007\/978-3-031-38499-8_11","DOI":"10.1007\/978-3-031-38499-8_11"},{"key":"5_CR25","unstructured":"D\u2019Agostino, M., Gabbay, D.M., H\u00e4hnle, R., Posegga, J.: Handbook of Tableau Methods. Springer (2013)"},{"key":"5_CR26","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/978-3-540-73595-3_35","volume-title":"Automated Deduction \u2013 CADE-21","author":"T Deshane","year":"2007","unstructured":"Deshane, T., Hu, W., Jablonski, P., Lin, H., Lynch, C., McGregor, R.E.: Encoding first order proofs in SAT. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 476\u2013491. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73595-3_35"},{"key":"5_CR27","unstructured":"Eisenhofer, C., Kov\u00e1cs, L., Rawson, M.: Embedding the connection calculus in satisfiability modulo theories. In: AReCCa, pp. 54\u201363 (2023). https:\/\/ceur-ws.org\/Vol-3613\/"},{"key":"5_CR28","unstructured":"F\u00e4rber, M.: A curiously effective backtracking strategy for connection tableaux. In: AReCCa, pp. 23\u201340 (2023). https:\/\/ceur-ws.org\/Vol-3613\/"},{"key":"5_CR29","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/978-3-319-40229-1_24","volume-title":"Automated Reasoning","author":"M F\u00e4rber","year":"2016","unstructured":"F\u00e4rber, M., Brown, C.: Internal guidance for satallax. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 349\u2013361. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_24"},{"key":"5_CR30","doi-asserted-by":"publisher","unstructured":"Fazekas, K., Niemetz, A., Preiner, M., Kirchweger, M., Szeider, S., Biere, A.: IPASIR-UP: user propagators for CDCL. In: SAT. LIPIcs, vol.\u00a0271, pp. 8:1\u20138:13 (2023). https:\/\/doi.org\/10.4230\/LIPICS.SAT.2023.8","DOI":"10.4230\/LIPICS.SAT.2023.8"},{"key":"5_CR31","doi-asserted-by":"publisher","unstructured":"Galmiche, D.: Connection methods in linear logic and proof nets construction. Theoret. Comput. Sci. 232(1), 231\u2013272 (2000). https:\/\/doi.org\/10.1016\/S0304-3975(99)00176-0. https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0304397599001760","DOI":"10.1016\/S0304-3975(99)00176-0"},{"key":"5_CR32","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., 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"},{"key":"5_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/3-540-57785-8_131","volume-title":"STACS 94","author":"J Goubault","year":"1994","unstructured":"Goubault, J.: The complexity of resource-bounded first-order classical logic. In: Enjalbert, P., Mayr, E.W., Wagner, K.W. (eds.) STACS 1994. LNCS, vol. 775, pp. 59\u201370. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-57785-8_131"},{"key":"5_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-642-37651-1_10","volume-title":"Programming Logics","author":"K Korovin","year":"2013","unstructured":"Korovin, K.: Inst-gen \u2013 a modular approach to instantiation-based automated reasoning. In: Voronkov, A., Weidenbach, C. (eds.) Programming Logics. LNCS, vol. 7797, pp. 239\u2013270. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37651-1_10"},{"key":"5_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"},{"key":"5_CR36","doi-asserted-by":"crossref","unstructured":"Kreitz, C., Otten, J., Schmitt, S., Pientka, B.: Matrix-based constructive theorem proving. In: Intellectics and Computational Logic (to Wolfgang Bibel on the occasion of his 60th birthday). Applied Logic Series, vol.\u00a019, pp. 189\u2013205 (2000)","DOI":"10.1007\/978-94-015-9383-0_12"},{"key":"5_CR37","doi-asserted-by":"publisher","unstructured":"Letz, R.: Using matings for pruning connection tableaux. In: CADE. LNCS, vol.\u00a01421, pp. 381\u2013396 (1998). https:\/\/doi.org\/10.1007\/BFB0054273","DOI":"10.1007\/BFB0054273"},{"issue":"2","key":"5_CR38","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/BF00244282","volume":"8","author":"R Letz","year":"1992","unstructured":"Letz, R., Schumann, J., Bayerl, S., Bibel, W.: SETHEO: a high-performance theorem prover. J. Autom. Reason. 8(2), 183\u2013212 (1992). https:\/\/doi.org\/10.1007\/BF00244282","journal-title":"J. Autom. Reason."},{"key":"5_CR39","doi-asserted-by":"publisher","unstructured":"Letz, R., Stenz, G.: Model elimination and connection tableau procedures. In: Handbook of Automated Reasoning (in 2 volumes), pp. 2015\u20132114. Elsevier and MIT Press (2001). https:\/\/doi.org\/10.1016\/B978-044450813-3\/50030-8","DOI":"10.1016\/B978-044450813-3\/50030-8"},{"key":"5_CR40","unstructured":"Lynce, I., Marques-Silva, J.: On computing minimum unsatisfiable cores. In: SAT (2004). http:\/\/www.satisfiability.org\/SAT04\/programme\/110.pdf"},{"key":"5_CR41","unstructured":"de\u00a0Moura, L., Bj\u00f8rner, N.: Relevancy propagation. Technical Report MSR-TR-2007-140, Microsoft Research, Technical report (2007)"},{"key":"5_CR42","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-540-73595-3_13","volume-title":"Automated Deduction \u2013 CADE-21","author":"L Moura","year":"2007","unstructured":"Moura, L., Bj\u00f8rner, N.: Efficient E-matching for SMT solvers. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 183\u2013198. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73595-3_13"},{"key":"5_CR43","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 Moura","year":"2008","unstructured":"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":"5_CR44","doi-asserted-by":"publisher","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Handbook of Automated Reasoning (in 2 volumes), pp. 371\u2013443. Elsevier and MIT Press (2001). https:\/\/doi.org\/10.1016\/B978-044450813-3\/50009-6","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"5_CR45","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/978-3-540-71070-7_23","volume-title":"Automated Reasoning","author":"J Otten","year":"2008","unstructured":"Otten, J.: leanCoP 2.0 and ileanCoP 1.2: high performance lean theorem proving in classical and intuitionistic logic (system descriptions). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 283\u2013291. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_23"},{"key":"5_CR46","doi-asserted-by":"publisher","unstructured":"Otten, J.: Implementing connection calculi for first-order modal logics. In: IWIL. EPiC Series in Computing, vol.\u00a022, pp. 18\u201332. EasyChair (2012). https:\/\/doi.org\/10.29007\/82M9","DOI":"10.29007\/82M9"},{"key":"5_CR47","doi-asserted-by":"publisher","unstructured":"Ramakrishnan, I.V., Sekar, R., Voronkov, A.: Term indexing. In: Handbook of Automated Reasoning (in 2 volumes), pp. 1853\u20131964. Elsevier and MIT Press (2001). https:\/\/doi.org\/10.1016\/b978-044450813-3\/50028-x","DOI":"10.1016\/b978-044450813-3\/50028-x"},{"key":"5_CR48","doi-asserted-by":"publisher","unstructured":"Rath, J., Biere, A., Kov\u00e1cs, L.: First-order subsumption via SAT solving. In: FMCAD, pp. 160\u2013169 (2022). https:\/\/doi.org\/10.34727\/2022\/ISBN.978-3-85448-053-2_22","DOI":"10.34727\/2022\/ISBN.978-3-85448-053-2_22"},{"key":"5_CR49","doi-asserted-by":"crossref","unstructured":"Rawson, M., Eisenhofer, C., Kov\u00e1cs, L.: Constraint learning for non-confluent proof search. In: Pozzatoand, G.L., Uustalu, T. (eds.) TABLEAUX 2025. LNCS (LNAI), vol. 15980, pp.103\u2013119. Springer, Cham (2026). https:\/\/doi.org\/10.1007\/978-3-032-06085-3_6","DOI":"10.1007\/978-3-032-06085-3_6"},{"key":"5_CR50","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-030-86059-2_15","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"M Rawson","year":"2021","unstructured":"Rawson, M., Reger, G.: Eliminating models during model elimination. In: Das, A., Negri, S. (eds.) TABLEAUX 2021. LNCS (LNAI), vol. 12842, pp. 250\u2013265. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-86059-2_15"},{"key":"5_CR51","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-29007-8_1","volume-title":"Frontiers of Combining Systems","author":"G Reger","year":"2019","unstructured":"Reger, G., Riener, M., Suda, M.: Symmetry avoidance in MACE-style finite model finding. In: Herzig, A., Popescu, A. (eds.) FroCoS 2019. LNCS (LNAI), vol. 11715, pp. 3\u201321. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29007-8_1"},{"key":"5_CR52","doi-asserted-by":"publisher","unstructured":"Reger, G., Suda, M.: The uses of SAT solvers in Vampire. In: Vampire. EPiC Series in Computing, vol.\u00a038, pp. 63\u201369 (2015). https:\/\/doi.org\/10.29007\/4W68","DOI":"10.29007\/4W68"},{"key":"5_CR53","doi-asserted-by":"crossref","unstructured":"Schulz, S.: Light-weight integration of SAT solving into first-order reasoners \u2013 first experiments. Vampire, pp. 9\u201319 (2017)","DOI":"10.29007\/89kc"},{"key":"5_CR54","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":"5_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"827","DOI":"10.1007\/11564751_73","volume-title":"Principles and Practice of Constraint Programming - CP 2005","author":"C Sinz","year":"2005","unstructured":"Sinz, C.: Towards an optimal CNF encoding of boolean cardinality constraints. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 827\u2013831. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11564751_73"},{"key":"5_CR56","doi-asserted-by":"crossref","unstructured":"Smullyan, R.M.: First-Order Logic. Springer (1968)","DOI":"10.1007\/978-3-642-86718-7"},{"key":"5_CR57","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure. from CNF to TH0, TPTP v6.4.0. J. Autom. Reason. 59(4), 483\u2013502 (2017)","DOI":"10.1007\/s10817-017-9407-7"},{"key":"5_CR58","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/3-540-45757-7_26","volume-title":"Logics in Artificial Intelligence","author":"C Tinelli","year":"2002","unstructured":"Tinelli, C.: A DPLL-based calculus for ground satisfiability modulo theories. In: Flesca, S., Greco, S., Ianni, G., Leone, N. (eds.) JELIA 2002. LNCS (LNAI), vol. 2424, pp. 308\u2013319. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45757-7_26"},{"key":"5_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-319-08867-9_46","volume-title":"Computer Aided Verification","author":"A Voronkov","year":"2014","unstructured":"Voronkov, A.: AVATAR: the architecture for first-order theorem provers. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 696\u2013710. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_46"},{"key":"5_CR60","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 with Analytic Tableaux and Related Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-06085-3_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T10:45:24Z","timestamp":1758969924000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-06085-3_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,25]]},"ISBN":["9783032060846","9783032060853"],"references-count":60,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-06085-3_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,25]]},"assertion":[{"value":"25 September 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"TABLEAUX","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Reasoning with Analytic Tableaux and Related Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Reykjavik","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Iceland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 September 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tableaux2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/icetcs.github.io\/frocos-itp-tableaux25\/tableaux\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}