{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,2]],"date-time":"2025-08-02T19:10:46Z","timestamp":1754161846111,"version":"3.41.2"},"publisher-location":"Cham","reference-count":62,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031999833","type":"print"},{"value":"9783031999840","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T00:00:00Z","timestamp":1753833600000},"content-version":"vor","delay-in-days":210,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We introduce SC-TPTP, an extension of the TPTP derivation format that supports sequent formalism, enabling seamless proof exchange between interactive theorem provers and first-order automated theorem provers. We provide a way to represent non-deductive steps\u2014Skolemization, clausification, and Tseitin normal form\u2014as deductive steps within the format. Building upon the existing support in the Lisa proof assistant and the Go\u00e9land theorem prover, SC-TPTP ecosystem is further enhanced with proof output interfaces for Egg and Prover9, as well as proof reconstruction support for HOL Light, Lean, and Rocq.<\/jats:p>","DOI":"10.1007\/978-3-031-99984-0_18","type":"book-chapter","created":{"date-parts":[[2025,7,29]],"date-time":"2025-07-29T11:47:41Z","timestamp":1753789661000},"page":"325-340","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Interoperability of\u00a0Proof Systems with\u00a0SC-TPTP"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8179-7549","authenticated-orcid":false,"given":"Simon","family":"Guilloud","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6665-8089","authenticated-orcid":false,"given":"Julie","family":"Cailler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5994-1081","authenticated-orcid":false,"given":"Sankalp","family":"Gambhir","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-7868-7185","authenticated-orcid":false,"given":"Auguste","family":"Poiroux","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2329-1029","authenticated-orcid":false,"given":"Yann","family":"Herklotz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8468-8409","authenticated-orcid":false,"given":"Thomas","family":"Bourgeat","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7044-9522","authenticated-orcid":false,"given":"Viktor","family":"Kun\u010dak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,7,30]]},"reference":[{"key":"18_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-25379-9_12","volume-title":"Certified Programs and Proofs","author":"M Armand","year":"2011","unstructured":"Armand, M., Faure, G., Gr\u00e9goire, B., Keller, C., Th\u00e9ry, L., Werner, B.: A modular integration of SAT\/SMT solvers to Coq through proof witnesses. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 135\u2013150. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-25379-9_12"},{"key":"18_CR2","unstructured":"Assaf, A., et al.: A Logical Framework based on the $$\\lambda $$$$\\Pi $$-calculus modulo theory. Tech. rep., arXiv (2023)"},{"key":"18_CR3","doi-asserted-by":"publisher","unstructured":"Avigad, J.: Eliminating definitions and Skolem functions in first-order logic. In: Proceedings 16th Annual IEEE Symposium on Logic in Computer Science, pp. 139\u2013146 (2001).https:\/\/doi.org\/10.1109\/LICS.2001.932490","DOI":"10.1109\/LICS.2001.932490"},{"issue":"2","key":"18_CR4","doi-asserted-by":"crossref","first-page":"669","DOI":"10.2178\/jsl\/1333566645","volume":"77","author":"M Baaz","year":"2012","unstructured":"Baaz, M., Hetzl, S., Weller, D.: On the complexity of proof Deskolemization. J. Symb. Log. 77(2), 669\u2013686 (2012)","journal-title":"J. Symb. Log."},{"key":"18_CR5","doi-asserted-by":"publisher","unstructured":"Baek, S.: A formally verified checker for first-order proofs. In: Cohen, L., Kaliszyk, C. (eds.) 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0193, pp. 6:1\u20136:13. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2021). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2021.6","DOI":"10.4230\/LIPIcs.ITP.2021.6"},{"key":"18_CR6","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: cvc5: A Versatile and Industrial-Strength SMT Solver. In: CPP 2011. LNCS, vol. 7086, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"18_CR7","unstructured":"Barrett, C.W., Stump, A., Tinelli, C.: The SMT-LIB Standard Version 2.0. Tech. rep., Stanford University (2010)"},{"key":"18_CR8","unstructured":"Besson, F.: A flexible proof format for SMT: A Proposal. In: Fontaine, P., Th\u00e9ry, L. (eds.) PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving (2011)"},{"issue":"1","key":"18_CR9","doi-asserted-by":"publisher","first-page":"101","DOI":"10.6092\/issn.1972-5787\/4593","volume":"9","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formalized Reason. 9(1), 101\u2013148 (2016). https:\/\/doi.org\/10.6092\/issn.1972-5787\/4593","journal-title":"J. Formalized Reason."},{"key":"18_CR10","doi-asserted-by":"publisher","unstructured":"Blanqui, F.: Translating HOL-light proofs to Coq. In: Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 1\u201318 (2024). https:\/\/doi.org\/10.29007\/6k4x","DOI":"10.29007\/6k4x"},{"key":"18_CR11","doi-asserted-by":"publisher","first-page":"1539","DOI":"10.1613\/jair.1.14296","volume":"77","author":"B Bogaerts","year":"2023","unstructured":"Bogaerts, B., Gocht, S., McCreesh, C., Nordstr\u00f6m, J.: Certified dominance and symmetry breaking for combinatorial optimisation. J. Artif. Intell. Res. 77, 1539\u20131589 (2023). https:\/\/doi.org\/10.1613\/jair.1.14296","journal-title":"J. Artif. Intell. Res."},{"key":"18_CR12","unstructured":"Bogaerts, B., McCreesh, C., Myreen, M.O., Nordstrom, J., Oertel, A., Tan, Y.K.: Documentation of VeriPB and CakePB for the SAT Competition 2023. Tech. rep. (2023)"},{"key":"18_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-642-25379-9_15","volume-title":"Certified Programs and Proofs","author":"S B\u00f6hme","year":"2011","unstructured":"B\u00f6hme, S., Fox, A., Sewell, T., Weber, T.: Reconstruction of Z3\u2019s bit-vector proofs in HOL4 and Isabelle\/HOL. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 183\u2013198. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-25379-9_15"},{"key":"18_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-642-14052-5_14","volume-title":"Interactive Theorem Proving","author":"S B\u00f6hme","year":"2010","unstructured":"B\u00f6hme, S., Weber, T.: Fast LCF-style proof reconstruction for Z3. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 179\u2013194. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14052-5_14"},{"key":"18_CR15","volume-title":"Specification and Verification of Sequential Machines in Rule-Based Hardware Languages","author":"T Bourgeat","year":"2023","unstructured":"Bourgeat, T.: Specification and Verification of Sequential Machines in Rule-Based Hardware Languages. Thesis, Massachusetts Institute of Technology (Feb (2023)"},{"key":"18_CR16","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-642-02959-2_12","volume-title":"Automated Deduction \u2013 CADE-22","author":"T Bouton","year":"2009","unstructured":"Bouton, T., Caminha B. de Oliveira, D., D\u00e9harbe, D., Fontaine, P.: veriT: an open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 151\u2013156. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_12"},{"key":"18_CR17","doi-asserted-by":"crossref","unstructured":"Cailler, J.: Designing an Automated Concurrent Tableau-Based Theorem Prover for First-Order Logic. Ph.D. thesis, Universit\u00e9 de Montpellier (2023)","DOI":"10.1007\/978-3-031-10769-6_22"},{"key":"18_CR18","unstructured":"Cailler, J., Guilloud, S.: SC-TPTP: an extension of the TPTP derivation format for sequent-based calculus. In: 9th Workshop on Practical Aspects of Automated Reasoning (2024)"},{"key":"18_CR19","doi-asserted-by":"publisher","unstructured":"Cailler, J., Rosain, J., Delahaye, D., Robillard, S., Bouziane, H.L.: Go\u00e9land: a concurrent tableau-based theorem prover (System Description). In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) Automated Reasoning, pp. 359\u2013368. Lecture Notes in Computer Science, Springer International Publishing, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_22","DOI":"10.1007\/978-3-031-10769-6_22"},{"key":"18_CR20","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-319-63046-5_14","volume-title":"Automated Deduction \u2013 CADE 26","author":"L Cruz-Filipe","year":"2017","unstructured":"Cruz-Filipe, L., Heule, M., Hunt, W.A., Kaufmann, M., Schneider-Kamp, P.: Efficient certified RAT verification. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 220\u2013236. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_14"},{"key":"18_CR21","doi-asserted-by":"publisher","unstructured":"Czajka, \u0141, Kaliszyk, C.: Hammer for Coq: automation for dependent type theory. J. Autom. Reason. , 423\u2013453 (2018). https:\/\/doi.org\/10.1007\/s10817-018-9458-4","DOI":"10.1007\/s10817-018-9458-4"},{"key":"18_CR22","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":"18_CR23","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-319-21401-6_26","volume-title":"Automated Deduction \u2013 CADE-25","author":"L de Moura","year":"2015","unstructured":"de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 378\u2013388. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_26"},{"key":"18_CR24","unstructured":"Deducteam: Deducteam\/lambdapi. Deducteam (2024)"},{"key":"18_CR25","doi-asserted-by":"publisher","unstructured":"Flatt, O., Coward, S., Willsey, M., Tatlock, Z., Panchekha, P.: Small proofs from congruence closure. In: 2022 Formal Methods in Computer-Aided Design (FMCAD), pp. 75\u201383 (2022).https:\/\/doi.org\/10.34727\/2022\/isbn.978-3-85448-053-2_13","DOI":"10.34727\/2022\/isbn.978-3-85448-053-2_13"},{"key":"18_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/11691372_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Fontaine","year":"2006","unstructured":"Fontaine, P., Marion, J.-Y., Merz, S., Nieto, L.P., Tiu, A.: Expressiveness + automation + soundness: towards combining SMT solvers and interactive proof assistants. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 167\u2013181. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11691372_11"},{"key":"18_CR27","doi-asserted-by":"publisher","unstructured":"Gocht, S., Nordstr\u00f6m, J.: Certifying parity reasoning efficiently using pseudo-boolean proofs \u2014 supplemental material (2022). https:\/\/doi.org\/10.5281\/zenodo.7083485","DOI":"10.5281\/zenodo.7083485"},{"key":"18_CR28","unstructured":"Guilloud, S., et al.: Interoperability of Proof Systems with SC-TPTP (Full Version). Tech. rep., EPFL (2025). https:\/\/infoscience.epfl.ch\/handle\/20.500.14299\/247663"},{"key":"18_CR29","unstructured":"Guilloud, S., Gambhir, S., Kuncak, V.: LISA \u2013 A modern proof system. In: 14th Conference on Interactive Theorem Proving, pp. 17:1\u201317:19. Leibniz International Proceedings in Informatics, Daghstuhl, Bialystok (2023)"},{"key":"18_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-642-03359-9_4","volume-title":"Theorem Proving in Higher Order Logics","author":"J Harrison","year":"2009","unstructured":"Harrison, J.: HOL light: an overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 60\u201366. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_4"},{"key":"18_CR31","unstructured":"Heule, M.J.H., Iser, M., J\u00e4rvisalo, M., Suda, M.: Proceedings of SAT Ccompetition 2024: Solver, Benchmark and Proof Checker Descriptions. University of Helsinki (2024)"},{"key":"18_CR32","unstructured":"Hoenicke, J., Schindler, T.I.: A Simple Proof Format for SMT. In: International Workshop on Satisfiability Modulo Theories (2022)"},{"key":"18_CR33","unstructured":"Holden, S.B.: Connect++: a new automated theorem prover based on the connection calculus. In: Otten, J., Bibel, W. (eds.) Proceedings of the 1st International Workshop on Automated Reasoning with Connection Calculi (AReCCa 2023) Affiliated with the 32nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2023), Prague, Czech Republic, September 18, 2023. CEUR Workshop Proceedings, vol.\u00a03613, pp. 95\u2013106. CEUR-WS.org (2023)"},{"issue":"2","key":"18_CR34","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s10817-014-9303-3","volume":"53","author":"C Kaliszyk","year":"2014","unstructured":"Kaliszyk, C., Urban, J.: Learning-assisted automated reasoning with flyspeck. J. Autom. Reason. 53(2), 173\u2013213 (2014). https:\/\/doi.org\/10.1007\/s10817-014-9303-3","journal-title":"J. Autom. Reason."},{"key":"18_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":"18_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1007\/978-3-319-66263-3_29","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2017","author":"P Lammich","year":"2017","unstructured":"Lammich, P.: The GRAT tool chain. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 457\u2013463. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66263-3_29"},{"key":"18_CR37","unstructured":"Lean Prover Community: Leanprover-community\/lean-auto. leanprover-community (2025)"},{"key":"18_CR38","unstructured":"McCune, W.: Prover9 and Mace4"},{"issue":"2","key":"18_CR39","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/j.entcs.2005.12.005","volume":"144","author":"S McLaughlin","year":"2006","unstructured":"McLaughlin, S., Barrett, C., Ge, Y.: Cooperating theorem provers: a case study combining HOL-light and CVC lite. Electron. Notes Theor. Comput. Sci. 144(2), 43\u201351 (2006). https:\/\/doi.org\/10.1016\/j.entcs.2005.12.005","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"18_CR40","volume-title":"Metamath: A Computer Language for Mathematical Proofs","author":"N Megill","year":"2019","unstructured":"Megill, N., Wheeler, D.A.: Metamath: A Computer Language for Mathematical Proofs. Lulu.com, Morrisville (2019)"},{"key":"18_CR41","unstructured":"Moura, L.D., Bj\u00f8rner, N.S.: Proofs and refutations, and Z3. In: LPAR Workshops (2008)"},{"issue":"2","key":"18_CR42","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27(2), 356\u2013364 (1980). https:\/\/doi.org\/10.1145\/322186.322198","journal-title":"J. ACM"},{"key":"18_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/978-3-540-32033-3_33","volume-title":"Term Rewriting and Applications","author":"R Nieuwenhuis","year":"2005","unstructured":"Nieuwenhuis, R., Oliveras, A.: Proof-producing congruence closure. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 453\u2013468. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-32033-3_33"},{"issue":"1","key":"18_CR44","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/S0747-7171(03)00037-3","volume":"36","author":"J Otten","year":"2003","unstructured":"Otten, J., Bibel, W.: leanCoP: lean connection-based theorem proving. J. Symb. Comput. 36(1), 139\u2013161 (2003). https:\/\/doi.org\/10.1016\/S0747-7171(03)00037-3","journal-title":"J. Symb. Comput."},{"key":"18_CR45","unstructured":"Otten, J., Holden, S.B.: A syntax for connection proofs. In: Otten, J., Bibel, W. (eds.) Proceedings of the 1st International Workshop on Automated Reasoning with Connection Calculi (AReCCa 2023) Affiliated with the 32nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2023), Prague, Czech Republic, September 18, 2023. CEUR Workshop Proceedings, vol.\u00a03613, pp. 84\u201394. CEUR-WS.org (2023)"},{"key":"18_CR46","doi-asserted-by":"publisher","unstructured":"Paulson, L.C., Susanto, K.W.: Source-level proof reconstruction for interactive theorem proving. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 232\u2013245. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74591-4_18","DOI":"10.1007\/978-3-540-74591-4_18"},{"key":"18_CR47","doi-asserted-by":"crossref","unstructured":"Qian, Y., Clune, J., Barrett, C., Avigad, J.: Lean-auto: an interface between lean 4 and automated theorem provers (2025). https:\/\/arxiv.org\/abs\/2505.14929","DOI":"10.1007\/978-3-031-98682-6_10"},{"key":"18_CR48","doi-asserted-by":"publisher","unstructured":"Rebola-Pardo, A., Cruz-Filipe, L.: Complete and efficient DRAT proof checking. In: 2018 Formal Methods in Computer Aided Design (FMCAD), pp.\u00a01\u20139 (2018).https:\/\/doi.org\/10.23919\/FMCAD.2018.8602993","DOI":"10.23919\/FMCAD.2018.8602993"},{"key":"18_CR49","doi-asserted-by":"crossref","unstructured":"Reger, G., Suda, M.: Checkable proofs for first-order theorem proving. In: ARCADE 2017. 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements, pp. 55\u201363. EasyChair EPiC Series in Computing (2017)","DOI":"10.29007\/s6d1"},{"key":"18_CR50","doi-asserted-by":"publisher","unstructured":"Rosain, J., Bonichon, R., Cailler, J., Hermant, O.: A generic Deskolemization strategy. In: Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 246\u2013227 (2024). https:\/\/doi.org\/10.29007\/g1tm","DOI":"10.29007\/g1tm"},{"key":"18_CR51","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":"18_CR52","doi-asserted-by":"publisher","first-page":"49","DOI":"10.4204\/EPTCS.336.6","volume":"336","author":"HJ Schurr","year":"2021","unstructured":"Schurr, H.J., Fleury, M., Barbosa, H., Fontaine, P.: Alethe: towards a generic SMT proof format (extended abstract). Electron. Proc. Theor. Comput. Sci. 336, 49\u201354 (2021). https:\/\/doi.org\/10.4204\/EPTCS.336.6","journal-title":"Electron. Proc. Theor. Comput. Sci."},{"key":"18_CR53","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/978-3-030-79876-5_26","volume-title":"Automated Deduction \u2013 CADE 28","author":"H-J Schurr","year":"2021","unstructured":"Schurr, H.-J., Fleury, M., Desharnais, M.: Reliable reconstruction of fine-grained proofs in a proof assistant. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 450\u2013467. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_26"},{"key":"18_CR54","doi-asserted-by":"publisher","unstructured":"Stump, A., Oe, D.: Towards an SMT proof format. In: Proceedings of the Joint Workshops of the 6th International Workshop on Satisfiability Modulo Theories and 1st International Workshop on Bit-Precise Reasoning, pp. 27\u201332. SMT \u201908\/BPR \u201908, Association for Computing Machinery, New York, NY, USA (2008).https:\/\/doi.org\/10.1145\/1512464.1512470","DOI":"10.1145\/1512464.1512470"},{"key":"18_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/978-3-540-74510-5_4","volume-title":"Computer Science \u2013 Theory and Applications","author":"G Sutcliffe","year":"2007","unstructured":"Sutcliffe, G.: TPTP, TSTP, CASC, etc. In: Diekert, V., Volkov, M.V., Voronkov, A. (eds.) CSR 2007. LNCS, vol. 4649, pp. 6\u201322. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74510-5_4"},{"key":"18_CR56","unstructured":"Sutcliffe, G.: The SZS ontologies for automated reasoning software. In: Rudnicki, P., Sutcliffe, G., Konev, B., Schmidt, R.A., Schulz, S. (eds.) Proceedings of the LPAR 2008 Workshops, Knowledge Exchange: Automated Provers and Proof Assistants, and the 7th International Workshop on the Implementation of Logics, Doha, Qatar, November 22, 2008. CEUR Workshop Proceedings, vol.\u00a0418. CEUR-WS.org (2008)"},{"issue":"4","key":"18_CR57","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/s10817-017-9407-7","volume":"59","author":"G Sutcliffe","year":"2017","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reason. 59(4), 483\u2013502 (2017). https:\/\/doi.org\/10.1007\/s10817-017-9407-7","journal-title":"J. Autom. Reason."},{"issue":"6","key":"18_CR58","doi-asserted-by":"publisher","first-page":"1153","DOI":"10.1093\/jigpal\/jzac068","volume":"31","author":"G Sutcliffe","year":"2023","unstructured":"Sutcliffe, G.: The logic languages of the TPTP world. Logic J. IGPL 31(6), 1153\u20131169 (2023). https:\/\/doi.org\/10.1093\/jigpal\/jzac068","journal-title":"Logic J. IGPL"},{"key":"18_CR59","unstructured":"Weber, T.: Designing proof formats: a user\u2019s perspective. In: International Workshop on Proof Exchange for Theorem Proving (2011)"},{"key":"18_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-319-09284-3_31","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"N Wetzler","year":"2014","unstructured":"Wetzler, N., Heule, M., Hunt, W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 422\u2013429. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-09284-3_31"},{"key":"18_CR61","doi-asserted-by":"publisher","unstructured":"Willsey, M., Nandi, C., Wang, Y.R., Flatt, O., Tatlock, Z., Panchekha, P.: EGG: fast and extensible equality saturation. Proc. ACM Progr. Lang. 5(POPL), 23:1\u201323:29 (2021). https:\/\/doi.org\/10.1145\/3434304","DOI":"10.1145\/3434304"},{"key":"18_CR62","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/978-3-662-54069-5_4","volume-title":"Logic and Its Applications","author":"R Zach","year":"2017","unstructured":"Zach, R.: Semantics and proof theory of the epsilon calculus. In: Ghosh, S., Prasad, S. (eds.) ICLA 2017. LNCS, vol. 10119, pp. 27\u201347. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54069-5_4"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 30"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-99984-0_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,29]],"date-time":"2025-07-29T11:47:44Z","timestamp":1753789664000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-99984-0_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031999833","9783031999840"],"references-count":62,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-99984-0_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"30 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Stuttgart","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","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":"28 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.dhbw-stuttgart.de\/cade-30\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}