{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T00:05:22Z","timestamp":1759017922054,"version":"3.44.0"},"publisher-location":"Cham","reference-count":42,"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>Proof search in non-confluent tableau calculi, such as the connection tableau calculus, suffers from excess backtracking, but simple restrictions on backtracking are incomplete. We adopt <jats:italic>constraint learning<\/jats:italic> to reduce backtracking in the classical first-order connection calculus, while retaining completeness. An initial constraint learning language for connection-driven search is iteratively refined to greatly reduce backtracking in practice. The approach may be useful for proof search in other non-confluent tableau calculi.<\/jats:p>","DOI":"10.1007\/978-3-032-06085-3_6","type":"book-chapter","created":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T10:45:10Z","timestamp":1758969910000},"page":"103-119","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Constraint Learning for\u00a0Non-confluent Proof Search"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7834-1567","authenticated-orcid":false,"given":"Michael","family":"Rawson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0339-1580","authenticated-orcid":false,"given":"Clemens","family":"Eisenhofer","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":"2","key":"6_CR1","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/S10817-013-9286-5","volume":"52","author":"J Alama","year":"2014","unstructured":"Alama, J., Heskes, T., K\u00fchlwein, D., Tsivtsivadze, E., Urban, J.: Premise selection for mathematics by corpus analysis and kernel methods. J. Autom. Reason. 52(2), 191\u2013213 (2014). https:\/\/doi.org\/10.1007\/S10817-013-9286-5","journal-title":"J. Autom. Reason."},{"issue":"2","key":"6_CR2","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"PB Andrews","year":"1981","unstructured":"Andrews, P.B.: Theorem proving via general matings. J. ACM 28(2), 193\u2013214 (1981). https:\/\/doi.org\/10.1145\/322248.322249","journal-title":"J. ACM"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/3-540-55602-8_168","volume-title":"Automated Deduction\u2014CADE-11","author":"OL Astrachan","year":"1992","unstructured":"Astrachan, O.L., Stickel, M.E.: Caching and lemmaizing in model elimination theorem provers. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 224\u2013238. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55602-8_168"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"572","DOI":"10.1007\/978-3-319-21401-6_39","volume-title":"Automated Deduction - CADE-25","author":"P Backeman","year":"2015","unstructured":"Backeman, P., R\u00fcmmer, P.: Theorem proving with bounded rigid E-unification. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 572\u2013587. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_39"},{"key":"6_CR5","doi-asserted-by":"publisher","unstructured":"Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. 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. 1267\u20131329. IOS Press (2021). https:\/\/doi.org\/10.3233\/FAIA201017","DOI":"10.3233\/FAIA201017"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Bibel, W.: Automated Theorem Proving, 2nd edn. Artificial intelligence, Vieweg (1987). https:\/\/www.worldcat.org\/oclc\/16641802","DOI":"10.1007\/978-3-322-90102-6"},{"key":"6_CR7","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/978-3-031-24950-1_5","volume-title":"VMCAI","author":"NS Bj\u00f8rner","year":"2023","unstructured":"Bj\u00f8rner, N.S., Eisenhofer, C., Kov\u00e1cs, L.: Satisfiability modulo custom theories in Z3. In: Dragoi, C., Emmi, M., Wang, J. (eds.) VMCAI. LNCS, vol. 13881, pp. 91\u2013105. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-24950-1_5"},{"issue":"4","key":"6_CR8","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":"6_CR9","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-031-10769-6_22","volume-title":"IJCAR","author":"J Cailler","year":"2022","unstructured":"Cailler, J., Rosain, J., Delahaye, D., Robillard, S., Bouziane, H.: Go\u00e9land: a concurrent tableau-based theorem prover (system description). In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) IJCAR. LNCS, vol. 13385, pp. 359\u2013368. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_22"},{"key":"6_CR10","doi-asserted-by":"publisher","unstructured":"D\u2019Agostino, M., Gabbay, D.M., H\u00e4hnle, R., Posegga, J., (eds): Handbook of tableau methods. J. Log. Lang. Inf. 10(4), 518\u2013523 (2001). https:\/\/doi.org\/10.1023\/A:1017520120752","DOI":"10.1023\/A:1017520120752"},{"key":"6_CR11","unstructured":"Dechter, R.: Learning while searching in constraint-satisfaction-problems. In: Proceedings of the 5th National Conference on Artificial Intelligence, pp. 178\u2013185. Morgan Kaufmann (1986). http:\/\/www.aaai.org\/Library\/AAAI\/1986\/aaai86-029.php"},{"key":"6_CR12","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":"6_CR13","unstructured":"Eisenhofer, C., Rawson, M., Kov\u00e1cs, L.: Spanning matrices via satisfiability solving (2025). https:\/\/doi.org\/to-appear, appears in the same TABLEAUX 2025 inproceeding"},{"key":"6_CR14","unstructured":"F\u00e4rber, M.: A curiously effective backtracking strategy for connection tableaux. In: Otten, J., Bibel, W. (eds.) AReCCa. CEUR Workshop Proceedings, vol.\u00a03613, pp. 23\u201340. CEUR-WS.org (2023). https:\/\/ceur-ws.org\/Vol-3613\/AReCCa2023_paper2.pdf"},{"key":"6_CR15","doi-asserted-by":"publisher","unstructured":"Fazekas, K., Niemetz, A., Preiner, M., Kirchweger, M., Szeider, S., Biere, A.: IPASIR-UP: user propagators for CDCL. In: Mahajan, M., Slivovsky, F. (eds.) SAT. LIPIcs, vol.\u00a0271, pp. 8:1\u20138:13. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023). https:\/\/doi.org\/10.4230\/LIPICS.SAT.2023.8","DOI":"10.4230\/LIPICS.SAT.2023.8"},{"key":"6_CR16","doi-asserted-by":"publisher","unstructured":"Ganzinger, H., Korovin, K.: New directions in instantiation-based theorem proving. In: LICS, pp. 55\u201364. IEEE Computer Society (2003). https:\/\/doi.org\/10.1109\/LICS.2003.1210045","DOI":"10.1109\/LICS.2003.1210045"},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/3-540-69778-0_22","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"U Hustadt","year":"1998","unstructured":"Hustadt, U., Schmidt, R.A.: Simplification and backjumping in modal tableau. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol. 1397, pp. 187\u2013201. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/3-540-69778-0_22"},{"key":"6_CR18","unstructured":"ISO\/IEC: Information technology\u2014Programming languages\u2014Prolog\u2014Part 1: General Core. Standard, International Organization for Standardization (1995)"},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-319-24312-2_8","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C.: Efficient low-level connection tableaux. In: De Nivelle, H. (ed.) TABLEAUX 2015. LNCS (LNAI), vol. 9323, pp. 102\u2013111. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24312-2_8"},{"key":"6_CR20","unstructured":"Kaliszyk, C., Urban, J., Michalewski, H., Ols\u00e1k, M.: Reinforcement learning of theorem proving. In: NeurIPS, pp. 8836\u20138847 (2018). https:\/\/proceedings.neurips.cc\/paper\/2018\/hash\/55acf8539596d25624059980986aaa78-Abstract.html"},{"key":"6_CR21","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"},{"issue":"2","key":"6_CR22","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/321450.321456","volume":"15","author":"DW Loveland","year":"1968","unstructured":"Loveland, D.W.: Mechanical theorem-proving by model elimination. J. ACM 15(2), 236\u2013251 (1968). https:\/\/doi.org\/10.1145\/321450.321456","journal-title":"J. ACM"},{"issue":"1","key":"6_CR23","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/S10817-007-9085-Y","volume":"40","author":"J Meng","year":"2008","unstructured":"Meng, J., Paulson, L.C.: Translating higher-order clauses to first-order clauses. J. Autom. Reason. 40(1), 35\u201360 (2008). https:\/\/doi.org\/10.1007\/S10817-007-9085-Y","journal-title":"J. Autom. Reason."},{"key":"6_CR24","doi-asserted-by":"publisher","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: DAC, pp. 530\u2013535. ACM (2001). https:\/\/doi.org\/10.1145\/378239.379017","DOI":"10.1145\/378239.379017"},{"key":"6_CR25","doi-asserted-by":"publisher","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Handbook of Automated Reasoning (in 2 volumes), pp. 371\u2013443 (2001). https:\/\/doi.org\/10.1016\/B978-044450813-3\/50009-6","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"6_CR26","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"},{"issue":"2\u20133","key":"6_CR27","doi-asserted-by":"publisher","first-page":"159","DOI":"10.3233\/AIC-2010-0464","volume":"23","author":"J Otten","year":"2010","unstructured":"Otten, J.: Restricting backtracking in connection calculi. AI Commun. 23(2\u20133), 159\u2013182 (2010). https:\/\/doi.org\/10.3233\/AIC-2010-0464","journal-title":"AI Commun."},{"key":"6_CR28","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-319-08587-6_20","volume-title":"Automated Reasoning","author":"J Otten","year":"2014","unstructured":"Otten, J.: MleanCoP: a connection prover for first-order modal logic. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 269\u2013276. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_20"},{"key":"6_CR29","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/978-3-319-40229-1_21","volume-title":"Automated Reasoning","author":"J Otten","year":"2016","unstructured":"Otten, J.: nanoCoP: a non-clausal connection prover. In: Olivetti, N., Tiwari, A. (eds.) IJCAR 2016. LNCS (LNAI), vol. 9706, pp. 302\u2013312. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_21"},{"key":"6_CR30","unstructured":"Otten, J.: The pocket reasoner \u2013 automatic reasoning on small devices. In: NIK. Bibsys Open Journal Systems, Norway (2018). https:\/\/ojs.bibsys.no\/index.php\/NIK\/article\/view\/512"},{"key":"6_CR31","unstructured":"Otten, J.: 20 years of leanCoP - an overview of the provers. In: AReCCa. CEUR Workshop Proceedings, vol.\u00a03613, pp. 4\u201322. CEUR-WS.org (2023). https:\/\/ceur-ws.org\/Vol-3613\/AReCCa2023_paper1.pdf"},{"issue":"2\u20133","key":"6_CR32","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/S10817-007-9089-7","volume":"40","author":"A Paskevich","year":"2008","unstructured":"Paskevich, A.: Connection tableaux with lazy paramodulation. J. Autom. Reason. 40(2\u20133), 179\u2013194 (2008). https:\/\/doi.org\/10.1007\/S10817-007-9089-7","journal-title":"J. Autom. Reason."},{"key":"6_CR33","unstructured":"Prusak, G., Kaliszyk, C.: Lazy paramodulation in practice. In: 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\u201312 August 2022. CEUR Workshop Proceedings, vol.\u00a03201. CEUR-WS.org (2022). https:\/\/ceur-ws.org\/Vol-3201\/paper3.pdf"},{"key":"6_CR34","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"},{"issue":"2","key":"6_CR35","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1017\/S1471068420000435","volume":"21","author":"E Robbins","year":"2021","unstructured":"Robbins, E., King, A., Howe, J.M.: Backjumping is exception handling. Theory Pract. Log. Program. 21(2), 125\u2013144 (2021). https:\/\/doi.org\/10.1017\/S1471068420000435","journal-title":"Theory Pract. Log. Program."},{"key":"6_CR36","unstructured":"R\u00f8mming, F., Otten, J., Holden, S.B.: Connections: Markov decision processes for classical, intuitionistic and modal connection calculi. In: AReCCa. CEUR Workshop Proceedings, vol.\u00a03613, pp. 107\u2013118. CEUR-WS.org (2023). https:\/\/ceur-ws.org\/Vol-3613\/AReCCa2023_paper8.pdf"},{"key":"6_CR37","doi-asserted-by":"publisher","unstructured":"Silva, J.P.M., Sakallah, K.A.: GRASP\u2014a new search algorithm for satisfiability. In: ICCAD, pp. 220\u2013227. IEEE Computer Society\/ACM (1996). https:\/\/doi.org\/10.1109\/ICCAD.1996.569607","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"6_CR38","doi-asserted-by":"publisher","unstructured":"Stickel, M.E.: A Prolog technology theorem prover. In: 9th International Conference on Automated Deduction, Argonne, Illinois, USA, 23\u201326 May 1988, Proceedings. LNCS, vol.\u00a0310, pp. 752\u2013753. Springer, Cham (1988). https:\/\/doi.org\/10.1007\/BFB0012881","DOI":"10.1007\/BFB0012881"},{"key":"6_CR39","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1007\/S10817-017-9407-7","DOI":"10.1007\/S10817-017-9407-7"},{"key":"6_CR40","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"492","DOI":"10.1007\/978-3-642-33353-8_41","volume-title":"Logics in Artificial Intelligence","author":"D Tishkovsky","year":"2012","unstructured":"Tishkovsky, D., Schmidt, R.A., Khodadadi, M.: The tableau prover generator MetTeL$$^{2}$$. In: del Cerro, L.F., Herzig, A., Mengin, J. (eds.) JELIA 2012. LNCS (LNAI), vol. 7519, pp. 492\u2013495. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33353-8_41"},{"issue":"4","key":"6_CR41","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/S10817-024-09711-8","volume":"68","author":"C Wernhard","year":"2024","unstructured":"Wernhard, C., Bibel, W.: Investigations into proof structures. J. Autom. Reason. 68(4), 24 (2024). https:\/\/doi.org\/10.1007\/S10817-024-09711-8","journal-title":"J. Autom. Reason."},{"key":"6_CR42","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/978-3-030-51054-1_33","volume-title":"Automated Reasoning","author":"Z Zombori","year":"2020","unstructured":"Zombori, Z., Urban, J., Brown, C.E.: Prolog technology reinforcement\u00a0learning prover. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12167, pp. 489\u2013507. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51054-1_33"}],"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_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T10:45:12Z","timestamp":1758969912000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-06085-3_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,25]]},"ISBN":["9783032060846","9783032060853"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-06085-3_6","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"}}]}}