{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,2]],"date-time":"2025-08-02T19:10:47Z","timestamp":1754161847078,"version":"3.41.2"},"publisher-location":"Cham","reference-count":46,"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>The <jats:sc>Vampire<\/jats:sc> automated theorem prover is extended to output proofs in such a way that each inference is represented by a quantifier-free SMT instance. If every instance is unsatisfiable, the proof can be considered verified by an external SMT solver. This pragmatic form of proof checking places only a very light burden on the SMT solver, and can easily handle inferences that other systems may find difficult, such as theory inferences or extensive ground reasoning. The method is considerably easier to implement than proof formats based on small kernels and covers a greater variety of modern-day inferences.<\/jats:p>","DOI":"10.1007\/978-3-031-99984-0_8","type":"book-chapter","created":{"date-parts":[[2025,7,29]],"date-time":"2025-07-29T11:47:45Z","timestamp":1753789665000},"page":"136-149","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Ground Truth: Checking Vampire Proofs via\u00a0Satisfiability Modulo Theories"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7834-1567","authenticated-orcid":false,"given":"Michael","family":"Rawson","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1073-7615","authenticated-orcid":false,"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5550-196X","authenticated-orcid":false,"given":"Johannes","family":"Schoisswohl","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7203-6641","authenticated-orcid":false,"given":"Anja","family":"Petkovi\u0107 Komel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,30]]},"reference":[{"key":"8_CR1","unstructured":"The Agda proof assistant (2021). https:\/\/wiki.portal.chalmers.se\/agda\/"},{"key":"8_CR2","doi-asserted-by":"publisher","unstructured":"Andreotti, B., Lachnitt, H., Barbosa, H.: Carcara: an efficient proof checker and elaborator for SMT proofs in the alethe format. In: Sankaranarayanan, S., Sharygina, N. (eds.) TACAS 2023, Part I. LNCS, vol. 13993, pp. 367\u2013386. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_19","DOI":"10.1007\/978-3-031-30823-9_19"},{"key":"8_CR3","doi-asserted-by":"crossref","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.) Certified Programs and Proofs, pp. 135\u2013150. Springer, Heidelberg (2011)"},{"key":"8_CR4","doi-asserted-by":"publisher","unstructured":"Assaf, A., et al.: Dedukti: a logical framework based on the $$\\lambda \\varPi $$-calculus modulo theory. CoRR abs\/2311.07185 (2023). https:\/\/doi.org\/10.48550\/ARXIV.2311.07185","DOI":"10.48550\/ARXIV.2311.07185"},{"key":"8_CR5","doi-asserted-by":"publisher","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes), pp. 19\u201399. Elsevier and MIT Press (2001). https:\/\/doi.org\/10.1016\/B978-044450813-3\/50004-7","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"key":"8_CR6","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, June 29 to July 1, 2021, Rome, Italy (Virtual Conference). LIPIcs, vol.\u00a0193, pp. 6:1\u20136:13. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPICS.ITP.2021.6","DOI":"10.4230\/LIPICS.ITP.2021.6"},{"key":"8_CR7","unstructured":"Barbosa, H.: New techniques for instantiation and proof production in SMT solving. Ph.D. thesis, Universit\u00e9 de Lorraine (2017)"},{"key":"8_CR8","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: cvc5: A versatile and industrial-strength SMT solver. In: Fisman, D., Rosu, G. (eds.) TACAS 2022, Part I. LNCS, vol. 13243, 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":"8_CR9","unstructured":"Barrett, C., Stump, A., Tinelli, C., et\u00a0al.: The SMT-LIB standard: version 2.0. In: Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, UK), vol.\u00a013, p.\u00a014 (2010)"},{"key":"8_CR10","doi-asserted-by":"publisher","unstructured":"Barrett, C.W., Tinelli, C.: Satisfiability modulo theories. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 305\u2013343. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_11","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"414","DOI":"10.1007\/978-3-642-38574-2_29","volume-title":"Automated Deduction \u2013 CADE-24","author":"JC Blanchette","year":"2013","unstructured":"Blanchette, J.C., Paskevich, A.: TFF1: the TPTP typed first-order form with rank-1 polymorphism. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 414\u2013420. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38574-2_29"},{"key":"8_CR12","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/978-3-540-75560-9_13","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R Bonichon","year":"2007","unstructured":"Bonichon, R., Delahaye, D., Doligez, D.: Zenon: an extensible automated theorem prover producing checkable proofs. In: Dershowitz, N., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning, pp. 151\u2013165. Springer, Heidelberg (2007)"},{"key":"8_CR13","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"},{"issue":"6","key":"8_CR14","doi-asserted-by":"publisher","first-page":"1001","DOI":"10.1007\/s10817-019-09533-z","volume":"64","author":"G Burel","year":"2019","unstructured":"Burel, G., Bury, G., Cauderlier, R., Delahaye, D., Halmagrand, P., Hermant, O.: First-order automated reasoning with theories: when deduction modulo theory meets practice. J. Autom. Reason. 64(6), 1001\u20131050 (2019). https:\/\/doi.org\/10.1007\/s10817-019-09533-z","journal-title":"J. Autom. Reason."},{"key":"8_CR15","unstructured":"Bury, G.: Integrating rewriting, tableau and superposition into SMT. Theses, Universit\u00e9 Sorbonne Paris Cit\u00e9 (2019). https:\/\/theses.hal.science\/tel-02612985"},{"key":"8_CR16","unstructured":"The Coq proof assistant, version 2021.02.2 (2021). https:\/\/coq.inria.fr\/"},{"key":"8_CR17","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.) 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, July 4-8, 2023, Alghero, Italy. 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":"8_CR18","unstructured":"Fleury, M., Blanchette, J.: Translation of proofs provided by external provers. Technical report, Techniche Universit\u00e4t M\u00fcnchen (2014)"},{"key":"8_CR19","unstructured":"Haddad, M.Y.E.: Integrating Automated Theorem Provers in Proof Assistants. (Utiliser des d\u00e9monstrateurs automatiques dans un assistant \u00e0 la preuve). Ph.D. thesis, University of Paris-Saclay, France (2021). https:\/\/tel.archives-ouvertes.fr\/tel-03387912"},{"key":"8_CR20","doi-asserted-by":"publisher","unstructured":"Heule, M., Kiesl, B.: The potential of interference-based proof systems. In: Reger, G., Traytel, D. (eds.) ARCADE 2017, 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements, Gothenburg, Sweden, 6th August 2017. EPiC Series in Computing, vol.\u00a051, pp. 51\u201354. EasyChair (2017). https:\/\/doi.org\/10.29007\/VR7N","DOI":"10.29007\/VR7N"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/3-540-48256-3_21","volume-title":"Theorem Proving in Higher Order Logics","author":"J Hurd","year":"1999","unstructured":"Hurd, J.: Integrating gandalf and HOL. In: Bertot, Y., Dowek, G., Th\u00e9ry, L., Hirschowitz, A., Paulin, C. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 311\u2013321. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48256-3_21"},{"key":"8_CR22","unstructured":"Hurd, J.: First-order proof tactics in higher-order logic theorem provers. Design and Application of Strategies\/Tactics in Higher Order Logics, number NASA\/CP-2003-212448 in NASA Technical reports, pp. 56\u201368 (2003)"},{"key":"8_CR23","unstructured":"Isabelle (2016). https:\/\/isabelle.in.tum.de\/"},{"key":"8_CR24","doi-asserted-by":"crossref","first-page":"292","DOI":"10.1007\/978-3-540-71070-7_24","volume-title":"Automated Reasoning","author":"K Korovin","year":"2008","unstructured":"Korovin, K.: iprover - an instantiation-based theorem prover for first-order logic (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Automated Reasoning, pp. 292\u2013298. Springer, Heidelberg (2008)"},{"key":"8_CR25","doi-asserted-by":"publisher","unstructured":"Korovin, K., Kov\u00e1cs, L., Reger, G., Schoisswohl, J., Voronkov, A.: ALASCA: reasoning in quantified linear arithmetic. In: Sankaranarayanan, S., Sharygina, N. (eds.) TACAS 2023, Part I. LNCS, vol. 13993, pp. 647\u2013665. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_33","DOI":"10.1007\/978-3-031-30823-9_33"},{"key":"8_CR26","doi-asserted-by":"publisher","unstructured":"Kov\u00e1cs, L., Hozzov\u00e1, P., Hajd\u00fa, M., Voronkov, A.: Induction in saturation. In: Benzm\u00fcller, C., Heule, M.J.H., Schmidt, R.A. (eds.) IJCAR 2024, Part I. LNCS, vol. 14739, pp. 21\u201329. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-63498-7_2","DOI":"10.1007\/978-3-031-63498-7_2"},{"key":"8_CR27","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":"8_CR28","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1007\/978-3-031-57246-3_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Lachnitt","year":"2024","unstructured":"Lachnitt, H., et al.: Isarare: automatic verification of SMT rewrites in Isabelle\/HOL. In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 311\u2013330. Springer, Cham (2024)"},{"key":"8_CR29","doi-asserted-by":"crossref","unstructured":"McCune, W.: OTTER 3.3 reference manual. CoRR cs.SC\/0310056 (2003). http:\/\/arxiv.org\/abs\/cs\/0310056","DOI":"10.2172\/822573"},{"key":"8_CR30","doi-asserted-by":"publisher","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","DOI":"10.1007\/S10817-007-9085-Y"},{"key":"8_CR31","doi-asserted-by":"crossref","unstructured":"Moskal, M.: Programming with triggers. In: Proceedings of the 7th International Workshop on Satisfiability Modulo Theories, pp. 20\u201329 (2009)","DOI":"10.1145\/1670412.1670416"},{"key":"8_CR32","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":"8_CR33","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-030-79876-5_22","volume-title":"Automated Deduction \u2013 CADE 28","author":"V Nummelin","year":"2021","unstructured":"Nummelin, V., Bentkamp, A., Tourret, S., Vukmirovi\u0107, P.: Superposition with first-class Booleans and inprocessing clausification. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 378\u2013395. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_22"},{"key":"8_CR34","doi-asserted-by":"publisher","unstructured":"Otten, J., Bibel, W.: leancop: lean connection-based theorem proving. J. Symb. Comput. 36(1-2), 139\u2013161 (2003). https:\/\/doi.org\/10.1016\/S0747-7171(03)00037-3","DOI":"10.1016\/S0747-7171(03)00037-3"},{"key":"8_CR35","doi-asserted-by":"publisher","unstructured":"Petkovi\u0107 Komel, A., Rawson, M., Suda, M.: Case study: verified Vampire proofs in the $$\\lambda \\varPi $$-calculus modulo. CoRR abs\/2503.15541 (2025). https:\/\/doi.org\/10.48550\/ARXIV.2503.15541","DOI":"10.48550\/ARXIV.2503.15541"},{"key":"8_CR36","doi-asserted-by":"publisher","unstructured":"Preiner, M., Schurr, H., Barrett, C.W., Fontaine, P., Niemetz, A., Tinelli, C.: SMT-LIB release 2024 (non-incremental benchmarks) (version 2024.04.23) (2024). https:\/\/doi.org\/10.5281\/ZENODO.11061097. Accessed YYYY-MM-DD","DOI":"10.5281\/ZENODO.11061097"},{"key":"8_CR37","doi-asserted-by":"publisher","unstructured":"Reger, G., Bj\u00f8rner, N.S., Suda, M., Voronkov, A.: AVATAR modulo theories. In: Benzm\u00fcller, C., Sutcliffe, G., Rojas, R. (eds.) GCAI 2016. 2nd Global Conference on Artificial Intelligence, 19 September\u20132 October 2016, Berlin, Germany. EPiC Series in Computing, vol.\u00a041, pp. 39\u201352. EasyChair (2016). https:\/\/doi.org\/10.29007\/K6TP","DOI":"10.29007\/K6TP"},{"key":"8_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-89960-2_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Reger","year":"2018","unstructured":"Reger, G., Suda, M., Voronkov, A.: Unification with abstraction and theory instantiation in saturation-based reasoning. In: Beyer, D., Huisman, M. (eds.) TACAS 2018, Part I. LNCS, vol. 10805, pp. 3\u201322. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_1"},{"key":"8_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-662-46081-8_5","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Reynolds","year":"2015","unstructured":"Reynolds, A., Kuncak, V.: Induction for SMT solvers. In: D\u2019Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 80\u201398. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46081-8_5"},{"key":"8_CR40","doi-asserted-by":"publisher","unstructured":"Schoisswohl, J., Kov\u00e1cs, L., Korovin, K.: VIRAS: conflict-driven quantifier elimination for integer-real arithmetic. In: Bj\u00f8rner, N.S., Heule, M., Voronkov, A. (eds.) LPAR 2024: Proceedings of 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning, Port Louis, Mauritius, 26\u201331 May 2024. EPiC Series in Computing, vol.\u00a0100, pp. 147\u2013164. EasyChair (2024). https:\/\/doi.org\/10.29007\/KG4V","DOI":"10.29007\/KG4V"},{"key":"8_CR41","doi-asserted-by":"publisher","unstructured":"Schurr, H., Fleury, M., Barbosa, H., Fontaine, P.: Alethe: towards a generic SMT proof format (extended abstract). In: Keller, C., Fleury, M. (eds.) Proceedings Seventh Workshop on Proof eXchange for Theorem Proving, PxTP 2021, Pittsburg, PA, USA, 11 July 2021. EPTCS, vol.\u00a0336, pp. 49\u201354 (2021). https:\/\/doi.org\/10.4204\/EPTCS.336.6","DOI":"10.4204\/EPTCS.336.6"},{"key":"8_CR42","doi-asserted-by":"publisher","unstructured":"Sutcliffe, G.: Semantic derivation verification: techniques and implementation. Int. J. Artif. Intell. Tools 15(6), 1053\u20131070 (2006). https:\/\/doi.org\/10.1142\/S0218213006003119","DOI":"10.1142\/S0218213006003119"},{"key":"8_CR43","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":"8_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1007\/978-3-642-28717-6_32","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"G Sutcliffe","year":"2012","unstructured":"Sutcliffe, G., Schulz, S., Claessen, K., Baumgartner, P.: The TPTP typed first-order form with arithmetic. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 406\u2013419. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28717-6_32"},{"key":"8_CR45","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":"8_CR46","doi-asserted-by":"publisher","unstructured":"Xu, Y., Liu, J., Chen, S., Zhong, X., He, X.: Contradiction separation based dynamic multi-clause synergized automated deduction. Inf. Sci. 462, 93\u2013113 (2018). https:\/\/doi.org\/10.1016\/J.INS.2018.04.086","DOI":"10.1016\/J.INS.2018.04.086"}],"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_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,29]],"date-time":"2025-07-29T11:47:49Z","timestamp":1753789669000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-99984-0_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031999833","9783031999840"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-99984-0_8","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 to declare that are relevant to the content of this article.","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"}}]}}