{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,10]],"date-time":"2026-01-10T00:27:32Z","timestamp":1768004852253,"version":"3.49.0"},"reference-count":54,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2024,6,27]],"date-time":"2024-06-27T00:00:00Z","timestamp":1719446400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,6,27]],"date-time":"2024-06-27T00:00:00Z","timestamp":1719446400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100005192","name":"Technical University of Denmark","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100005192","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2024,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We describe the design, implementation and verification of an automated theorem prover for first-order logic with functions. The proof search procedure is based on sequent calculus and we formally verify its soundness and completeness in Isabelle\/HOL using an existing abstract framework for coinductive proof trees. Our analytic completeness proof covers both open and closed formulas. Since our deterministic prover considers only the subset of terms relevant to proving a given sequent, we do the same when building a countermodel from a failed proof. Finally, we formally connect our prover with the proof system and semantics of the existing SeCaV system. In particular, the prover can generate human-readable SeCaV proofs which are also machine-verifiable proof certificates. The abstract framework we rely on requires us to fix a stream of proof rules in advance, independently of the formula we are trying to prove. We discuss the efficiency implications of this and the difficulties in mitigating them.<\/jats:p>","DOI":"10.1007\/s10817-024-09697-3","type":"journal-article","created":{"date-parts":[[2024,6,27]],"date-time":"2024-06-27T09:03:37Z","timestamp":1719479017000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle\/HOL"],"prefix":"10.1007","volume":"68","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3601-0804","authenticated-orcid":false,"given":"Asta Halkj\u00e6r","family":"From","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3651-8314","authenticated-orcid":false,"given":"Frederik Krogsdal","family":"Jacobsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,6,27]]},"reference":[{"issue":"2","key":"9697_CR1","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s10817-013-9284-7","volume":"52","author":"C Ballarin","year":"2014","unstructured":"Ballarin, C.: Locales: a module system for mathematical theories. J. Autom. Reason. 52(2), 123\u2013153 (2014). https:\/\/doi.org\/10.1007\/s10817-013-9284-7","journal-title":"J. Autom. Reason."},{"key":"9697_CR2","doi-asserted-by":"publisher","unstructured":"Ben-Ari, M.: Mathematical Logic for Computer Science, pp. 149\u2013150. Springer, London (2012). https:\/\/doi.org\/10.1007\/978-1-4471-4129-7","DOI":"10.1007\/978-1-4471-4129-7"},{"key":"9697_CR3","doi-asserted-by":"publisher","unstructured":"Bentkamp, A., Blanchette, J., Tourret, S., Vukmirovi\u0107, P.: Superposition for full higher-order logic. In: Platzer, A., Sutcliffe, G. (eds.) Automated Deduction \u2013 CADE 28. Lecture Notes in Computer Science, vol. 12699, pp. 396\u2013412. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_23","DOI":"10.1007\/978-3-030-79876-5_23"},{"key":"9697_CR4","unstructured":"Berghofer, S.: First-order logic according to Fitting. Archive of Formal Proofs. Formal proof development (2007). https:\/\/isa-afp.org\/entries\/FOL-Fitting.html"},{"key":"9697_CR5","doi-asserted-by":"publisher","unstructured":"Blanchette, J.C., Gheri, L., Popescu, A., Traytel, D.: Bindings as bounded natural functors. Proc. ACM Program. Lang. 3(POPL, Article 22), 1\u201334 (2019). https:\/\/doi.org\/10.1145\/3290335","DOI":"10.1145\/3290335"},{"key":"9697_CR6","unstructured":"Blanchette, J.C., Popescu, A., Traytel, D.: Abstract completeness. Archive of Formal Proofs. Formal proof development (2014). https:\/\/isa-afp.org\/entries\/Abstract_Completeness.html"},{"key":"9697_CR7","doi-asserted-by":"publisher","unstructured":"Blanchette, J.C., Popescu, A., Traytel, D.: Unified classical logic completeness. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) Automated Reasoning. Lecture Notes in Computer Science, vol. 8562, pp. 46\u201360. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_4","DOI":"10.1007\/978-3-319-08587-6_4"},{"key":"9697_CR8","doi-asserted-by":"publisher","unstructured":"Blanchette, J.C., Popescu, A.: Mechanizing the metatheory of Sledgehammer. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) Frontiers of Combining Systems. Lecture Notes in Computer Science, vol. 8152, pp. 245\u2013260. Springer, Berlin (2013). https:\/\/doi.org\/10.1007\/978-3-642-40885-4_17","DOI":"10.1007\/978-3-642-40885-4_17"},{"key":"9697_CR9","doi-asserted-by":"publisher","unstructured":"Blanchette, J.C.: Formalizing the metatheory of logical calculi and automatic provers in Isabelle\/HOL (invited talk). In: Mahboubi, A., Myreen, M.O. (eds.) Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, pp. 1\u201313. ACM, New York (2019). https:\/\/doi.org\/10.1145\/3293880.3294087","DOI":"10.1145\/3293880.3294087"},{"issue":"1\u20134","key":"9697_CR10","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/s10817-018-9455-7","volume":"61","author":"JC Blanchette","year":"2018","unstructured":"Blanchette, J.C., Fleury, M., Lammich, P., Weidenbach, C.: A verified SAT solver framework with learn, forget, restart, and incrementality. J. Autom. Reason. 61(1\u20134), 333\u2013365 (2018). https:\/\/doi.org\/10.1007\/s10817-018-9455-7","journal-title":"J. Autom. Reason."},{"issue":"1","key":"9697_CR11","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/s10817-016-9391-3","volume":"58","author":"JC Blanchette","year":"2017","unstructured":"Blanchette, J.C., Popescu, A., Traytel, D.: Soundness and completeness proofs by coinductive methods. J. Autom. Reason. 58(1), 149\u2013179 (2017). https:\/\/doi.org\/10.1007\/s10817-016-9391-3","journal-title":"J. Autom. Reason."},{"key":"9697_CR12","doi-asserted-by":"publisher","unstructured":"Breitner, J.: Visual theorem proving with the Incredible Proof Machine. In: Blanchette, J., Merz, S. (eds.) Interactive Theorem Proving. Lecture Notes in Computer Science, vol. 9807, pp. 123\u2013139. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-43144-4_8","DOI":"10.1007\/978-3-319-43144-4_8"},{"key":"9697_CR13","doi-asserted-by":"publisher","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 4963, pp. 337\u2013340. Springer, Berlin (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9697_CR14","doi-asserted-by":"publisher","unstructured":"Fleury, M.: Optimizing a verified SAT solver. In: Badger, J.M., Rozier, K.Y. (eds.) NASA Formal Methods. Lecture Notes in Computer Science, vol. 11460, pp. 148\u2013165. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-20652-9_10","DOI":"10.1007\/978-3-030-20652-9_10"},{"key":"9697_CR15","doi-asserted-by":"publisher","unstructured":"From, A.H., Jacobsen, F.K., Villadsen, J.: SeCaV: a sequent calculus verifier in Isabelle\/HOL. In: Ayala-Rinc\u00f3n, M., Bonelli, E. (eds.) 16th Logical and Semantic Frameworks with Applications (LSFA 2021). Electronic Proceedings in Theoretical Computer Science, vol. 357, pp. 38\u201355 (2022). https:\/\/doi.org\/10.4204\/EPTCS.357.4","DOI":"10.4204\/EPTCS.357.4"},{"key":"9697_CR16","unstructured":"From, A.H., Jacobsen, F.K.: A sequent calculus prover for first-order logic with functions. Archive of Formal Proofs. Formal proof development (2022). https:\/\/isa-afp.org\/entries\/FOL_Seq_Calc2.html"},{"key":"9697_CR17","doi-asserted-by":"publisher","unstructured":"From, A.H., Jacobsen, F.K.: Verifying a sequent calculus prover for first-order logic with functions in Isabelle\/HOL. In: Andronick, J., de Moura, L. (eds.) 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol. 237, pp. 1\u201322. Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2022). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2022.13","DOI":"10.4230\/LIPIcs.ITP.2022.13"},{"key":"9697_CR18","doi-asserted-by":"publisher","unstructured":"From, A.H., Jensen, A.B., Schlichtkrull, A., Villadsen, J.: Teaching a formalized logical calculus. In: Quaresma, P., Neuper, W., Marcos, J. (eds.) Theorem Proving Components for Educational Software (ThEdu\u201919). Electronic Proceedings in Theoretical Computer Science, vol. 313, pp. 73\u201392 (2020). https:\/\/doi.org\/10.4204\/EPTCS.313.5","DOI":"10.4204\/EPTCS.313.5"},{"key":"9697_CR19","doi-asserted-by":"publisher","unstructured":"From, A.H., Villadsen, J., Blackburn, P.: Isabelle\/HOL as a meta-language for teaching logic. In: Marcos, J., Neuper, W., Quaresma, P. (eds.) Theorem Proving Components for Educational Software (ThEdu\u201920). Electronic Proceedings in Theoretical Computer Science, vol. 328, pp. 18\u201334 (2020). https:\/\/doi.org\/10.4204\/EPTCS.328.2","DOI":"10.4204\/EPTCS.328.2"},{"key":"9697_CR20","unstructured":"From, A.H.: Epistemic logic: Completeness of modal logics. Archive of Formal Proofs. Formal proof development (2018). https:\/\/isa-afp.org\/entries\/Epistemic_Logic.html"},{"key":"9697_CR21","doi-asserted-by":"publisher","unstructured":"From, A.H.: Formalized soundness and completeness of epistemic logic. In: Silva, A., Wassermann, R., de Queiroz, R. (eds.) Logic, Language, Information, and Computation. Lecture Notes in Computer Science, vol. 13038, pp. 1\u201315. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-88853-4_1","DOI":"10.1007\/978-3-030-88853-4_1"},{"key":"9697_CR22","unstructured":"Jacobsen, F.K.: Formalization of logical systems in Isabelle: an automated theorem prover for the Sequent Calculus Verifier. Master\u2019s thesis, Technical University of Denmark (June 2021). https:\/\/findit.dtu.dk\/en\/catalog\/2691928304"},{"issue":"3","key":"9697_CR23","doi-asserted-by":"publisher","first-page":"281","DOI":"10.3233\/AIC-180764","volume":"31","author":"AB Jensen","year":"2018","unstructured":"Jensen, A.B., Larsen, J.B., Schlichtkrull, A., Villadsen, J.: Programming and verifying a declarative first-order prover in Isabelle\/HOL. AI Commun. 31(3), 281\u2013299 (2018). https:\/\/doi.org\/10.3233\/AIC-180764","journal-title":"AI Commun."},{"key":"9697_CR24","doi-asserted-by":"publisher","unstructured":"Kamm\u00fcller, F., Wenzel, M., Paulson, L.C.: Locales - A sectioning concept for Isabelle. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin-Mohring, C., Th\u00e9ry, L. (eds.) Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science, vol. 1690, pp. 149\u2013165. Springer, Berlin (1999). https:\/\/doi.org\/10.1007\/3-540-48256-3_11","DOI":"10.1007\/3-540-48256-3_11"},{"key":"9697_CR25","unstructured":"Knuth, D.E., van Emde\u00a0Boas, P.: The correspondence between Donald E. Knuth and Peter van Emde Boas on priority deques during the spring of 1977. Facsimile edition (1977). https:\/\/staff.fnwi.uva.nl\/p.vanemdeboas\/knuthnote.pdf"},{"key":"9697_CR26","doi-asserted-by":"publisher","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification. Lecture Notes in Computer Science, vol. 8044, pp. 1\u201335. Springer, Berlin (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1","DOI":"10.1007\/978-3-642-39799-8_1"},{"issue":"2","key":"9697_CR27","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/s10817-018-9464-6","volume":"62","author":"O Kun\u010dar","year":"2019","unstructured":"Kun\u010dar, O., Popescu, A.: From types to sets by local type definition in higher-order logic. J. Autom. Reason. 62(2), 237\u2013260 (2019). https:\/\/doi.org\/10.1007\/s10817-018-9464-6","journal-title":"J. Autom. Reason."},{"key":"9697_CR28","doi-asserted-by":"publisher","unstructured":"Lammich, P.: The GRAT tool chain. In: Gaspers, S., Walsh, T. (eds.) Theory and Applications of Satisfiability Testing\u2014SAT 2017. Lecture Notes in Computer Science, vol. 10491, pp. 457\u2013463. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66263-3_29","DOI":"10.1007\/978-3-319-66263-3_29"},{"issue":"3","key":"9697_CR29","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1007\/s10817-019-09525-z","volume":"64","author":"P Lammich","year":"2020","unstructured":"Lammich, P.: Efficient verified (UN)SAT certificate checking. J. Autom. Reason. 64(3), 513\u2013532 (2020). https:\/\/doi.org\/10.1007\/s10817-019-09525-z","journal-title":"J. Autom. Reason."},{"key":"9697_CR30","unstructured":"Lescuyer, S.: Formalizing and Implementing a Reflexive Tactic for Automated Deduction in Coq. PhD thesis, Universit\u00e9 Paris Sud - Paris XI (January 2011). https:\/\/tel.archives-ouvertes.fr\/tel-00713668"},{"key":"9697_CR31","unstructured":"Lochbihler, A., Stoop, P.: Lazy algebraic types in Isabelle\/HOL. In: Isabelle Workshop 2018 (2018). https:\/\/files.sketis.net\/Isabelle_Workshop_2018\/Isabelle_2018_paper_2.pdf"},{"key":"9697_CR32","unstructured":"Mari\u0107, F., Spasi\u0107, M., Thiemann, R.: An incremental simplex algorithm with unsatisfiable core generation. Archive of Formal Proofs. Formal proof development (2018). https:\/\/isa-afp.org\/entries\/Simplex.html"},{"key":"9697_CR33","unstructured":"Mari\u0107, F.: Formal verification of modern SAT solvers. Archive of Formal Proofs. Formal proof development (2008). https:\/\/isa-afp.org\/entries\/SATSolverVerification.html"},{"issue":"50","key":"9697_CR34","doi-asserted-by":"publisher","first-page":"4333","DOI":"10.1016\/j.tcs.2010.09.014","volume":"411","author":"F Mari\u0107","year":"2010","unstructured":"Mari\u0107, F.: Formal verification of a modern SAT solver by shallow embedding into Isabelle\/HOL. Theor. Comput. Sci. 411(50), 4333\u20134356 (2010). https:\/\/doi.org\/10.1016\/j.tcs.2010.09.014","journal-title":"Theor. Comput. Sci."},{"key":"9697_CR35","doi-asserted-by":"publisher","unstructured":"Michaelis, J., Nipkow, T.: Formalized proof systems for propositional logic. In: Abel, A., Forsberg, F.N., Kaposi, A. (eds.) 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), vol. 104, pp. 1\u201316. Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2018). https:\/\/doi.org\/10.4230\/LIPIcs.TYPES.2017.5","DOI":"10.4230\/LIPIcs.TYPES.2017.5"},{"key":"9697_CR36","unstructured":"Michaelis, J., Nipkow, T.: Propositional proof systems. Archive of Formal Proofs. Formal proof development (2017). https:\/\/isa-afp.org\/entries\/Propositional_Proof_Systems.html"},{"key":"9697_CR37","doi-asserted-by":"publisher","unstructured":"Pastre, D.: Muscadet 2.3: A knowledge-based theorem prover based on natural deduction. In: Gore, R., Leitsch, A., Nipkow, T. (eds.) Automated Reasoning. Lecture Notes in Computer Science, vol. 2083, pp. 685\u2013689. Springer, Berlin (2001). https:\/\/doi.org\/10.1007\/3-540-45744-5_56","DOI":"10.1007\/3-540-45744-5_56"},{"issue":"1","key":"9697_CR38","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1023\/A:1005035316026","volume":"60","author":"FJ Pelletier","year":"1998","unstructured":"Pelletier, F.J.: Automated natural deduction in THINKER. Stud. Logica 60(1), 3\u201343 (1998). https:\/\/doi.org\/10.1023\/A:1005035316026","journal-title":"Stud. Logica"},{"key":"9697_CR39","unstructured":"Peltier, N.: A variant of the superposition calculus. Archive of Formal Proofs. Formal proof development (2016). https:\/\/isa-afp.org\/entries\/SuperCalc.html"},{"key":"9697_CR40","unstructured":"Peltier, N.: Propositional resolution and prime implicates generation. Archive of Formal Proofs. Formal proof development (2016). https:\/\/isa-afp.org\/entries\/PropResPI.html"},{"key":"9697_CR41","doi-asserted-by":"publisher","unstructured":"Ridge, T., Margetson, J.: A mechanically verified, sound and complete theorem prover for first order logic. In: Hurd, J., Melham, T. (eds.) Theorem Proving in Higher Order Logics (TPHOLs 2005). Lecture Notes in Computer Science, vol. 3603, pp. 294\u2013309. Springer, Berlin (2005). https:\/\/doi.org\/10.1007\/11541868_19","DOI":"10.1007\/11541868_19"},{"key":"9697_CR42","doi-asserted-by":"publisher","unstructured":"Schlichtkrull, A., Blanchette, J.C., Traytel, D., Waldmann, U.: Formalizing Bachmair and Ganzinger\u2019s ordered resolution prover. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) Automated Reasoning. Lecture Notes in Computer Science, vol. 10900, pp. 89\u2013107. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_7","DOI":"10.1007\/978-3-319-94205-6_7"},{"key":"9697_CR43","doi-asserted-by":"publisher","unstructured":"Schlichtkrull, A., Blanchette, J.C., Traytel, D.: A verified prover based on ordered resolution. In: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs. CPP 2019, pp. 152\u2013165. Association for Computing Machinery, New York (2019). https:\/\/doi.org\/10.1145\/3293880.3294100","DOI":"10.1145\/3293880.3294100"},{"key":"9697_CR44","unstructured":"Schlichtkrull, A., Villadsen, J.: Paraconsistency. Archive of Formal Proofs. Formal proof development (2016). https:\/\/isa-afp.org\/entries\/Paraconsistency.html"},{"issue":"1\u20134","key":"9697_CR45","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/s10817-017-9447-z","volume":"61","author":"A Schlichtkrull","year":"2018","unstructured":"Schlichtkrull, A.: Formalization of the resolution calculus for first-order logic. J. Autom. Reason. 61(1\u20134), 455\u2013484 (2018). https:\/\/doi.org\/10.1007\/s10817-017-9447-z","journal-title":"J. Autom. Reason."},{"key":"9697_CR46","doi-asserted-by":"publisher","unstructured":"Shankar, N., Vaucher, M.: The mechanical verification of a DPLL-based satisfiability solver. In: Haeusler, E.H., del Cerro, L.F. (eds.) Proceedings of the Fifth Logical and Semantic Frameworks, with Applications Workshop (LSFA 2010). Electronic Notes in Theoretical Computer Science, vol. 269, pp. 3\u201317 (2011). https:\/\/doi.org\/10.1016\/j.entcs.2011.03.002","DOI":"10.1016\/j.entcs.2011.03.002"},{"key":"9697_CR47","volume-title":"First-Order Logic","author":"RM Smullyan","year":"1995","unstructured":"Smullyan, R.M.: First-Order Logic. Dover, Mineola (1995)"},{"key":"9697_CR48","doi-asserted-by":"publisher","unstructured":"Spasi\u0107, M., Mari\u0107, F.: Formalization of incremental simplex algorithm by stepwise refinement. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012: Formal Methods. Lecture Notes in Computer Science, vol. 7436, pp. 434\u2013449. Springer, Berlin (2012). https:\/\/doi.org\/10.1007\/978-3-642-32759-9_35","DOI":"10.1007\/978-3-642-32759-9_35"},{"issue":"4","key":"9697_CR49","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. 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","journal-title":"J. Autom. Reason."},{"key":"9697_CR50","doi-asserted-by":"publisher","unstructured":"Villadsen, J., From, A.H., Jensen, A.B., Schlichtkrull, A.: Interactive theorem proving for logic and information. In: Loukanova, R. (ed.) Natural Language Processing in Artificial Intelligence\u2014NLPinAI 2021. Studies in Computational Intelligence, vol. 999, pp. 25\u201348. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-90138-7_2","DOI":"10.1007\/978-3-030-90138-7_2"},{"key":"9697_CR51","doi-asserted-by":"publisher","unstructured":"Villadsen, J., From, A.H., Schlichtkrull, A.: Natural Deduction Assistant (NaDeA). In: Quaresma, P., Neuper, W. (eds.) Theorem Proving Components for Educational Software (ThEdu\u201918). Electronic Proceedings in Theoretical Computer Science, vol. 290, pp. 14\u201329 (2019). https:\/\/doi.org\/10.4204\/EPTCS.290.2","DOI":"10.4204\/EPTCS.290.2"},{"key":"9697_CR52","doi-asserted-by":"publisher","unstructured":"Villadsen, J., Jacobsen, F.K.: Using Isabelle in two courses on logic and automated reasoning. In: Ferreira, J.F., Mendes, A., Menghi, C. (eds.) Formal Methods Teaching. Lecture Notes in Computer Science, vol. 13122, pp. 117\u2013132. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-91550-6_9","DOI":"10.1007\/978-3-030-91550-6_9"},{"key":"9697_CR53","unstructured":"Villadsen, J., Schlichtkrull, A., From, A.H.: A verified simple prover for first-order logic. In: Konev, B., Urban, J., R\u00fcmmer, P. (eds.) Practical Aspects of Automated Reasoning. CEUR Workshop Proceedings, vol. 2162, pp. 88\u2013104. CEUR-WS, Aachen (2018). https:\/\/ceur-ws.org\/Vol-2162\/paper-08.pdf"},{"key":"9697_CR54","doi-asserted-by":"publisher","unstructured":"Villadsen, J., Schlichtkrull, A.: Formalizing a paraconsistent logic in the Isabelle proof assistant. In: Hameurlain, A., K\u00fcng, J., Wagner, R., Decker, H. (eds.) Transactions on Large-Scale Data- and Knowledge-Centered Systems XXXIV: Special Issue on Consistency and Inconsistency in Data-Centric Applications. Lecture Notes in Computer Science, vol. 10620, pp. 92\u2013122. Springer, Berlin (2017). https:\/\/doi.org\/10.1007\/978-3-662-55947-5_5","DOI":"10.1007\/978-3-662-55947-5_5"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09697-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-024-09697-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09697-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T09:08:33Z","timestamp":1725613713000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-024-09697-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,27]]},"references-count":54,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2024,9]]}},"alternative-id":["9697"],"URL":"https:\/\/doi.org\/10.1007\/s10817-024-09697-3","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,27]]},"assertion":[{"value":"29 March 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"28 March 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 June 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors have no relevant financial or non-financial interests to disclose.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}],"article-number":"15"}}