{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,31]],"date-time":"2025-12-31T00:33:31Z","timestamp":1767141211562,"version":"build-2238731810"},"reference-count":60,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2022,10,1]],"date-time":"2022-10-01T00:00:00Z","timestamp":1664582400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,10,1]],"date-time":"2022-10-01T00:00:00Z","timestamp":1664582400000},"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":["J Autom Reasoning"],"published-print":{"date-parts":[[2022,11]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Special relativity is a cornerstone of modern physical theory. While a standard coordinate model is well known and widely taught today, multiple axiomatic systems for SR have been constructed over the past century. This paper reports on the formalisation of one such system, which is closer in spirit to Hilbert\u2019s axiomatic approach to Euclidean geometry than to the vector space approach employed by Minkowski. We present a mechanisation in Isabelle\/HOL of the system of axioms as well as theorems relating to temporal order. Some proofs are discussed, particularly where the formal work required additional steps, alternative approaches or corrections to Schutz\u2019 prose.<\/jats:p>","DOI":"10.1007\/s10817-022-09643-1","type":"journal-article","created":{"date-parts":[[2022,10,1]],"date-time":"2022-10-01T02:03:11Z","timestamp":1664589791000},"page":"953-988","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Towards Formalising Schutz\u2019 Axioms for Minkowski Spacetime in Isabelle\/HOL"],"prefix":"10.1007","volume":"66","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1473-071X","authenticated-orcid":false,"given":"Richard","family":"Schmoetten","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jake E.","family":"Palmer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jacques D.","family":"Fleuriot","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,10,1]]},"reference":[{"key":"9643_CR1","doi-asserted-by":"crossref","unstructured":"Andr\u00e9ka, H., N\u00e9meti, I., Madar\u00e1sz, J.X., Sz\u00e9kely, G.: On logical analysis of relativity theories. arXiv:1105.0885 (2011)","DOI":"10.1007\/978-3-7091-0177-3_11"},{"key":"9643_CR2","unstructured":"Andr\u00e9ka, H., Madar\u00e1sz, J.X., N\u00e9meti, I., Sz\u00e9kely, G.: An axiom system for general relativity complete with respect to Lorentzian manifolds. arXiv:1310.1475 (2013)"},{"issue":"4","key":"9643_CR3","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/s11873-010-0132-1","volume":"131","author":"A Bernard","year":"2010","unstructured":"Bernard, A.: The significance of Ptolemy\u2019s Almagest for its early readers. Rev. Synth. 131(4), 495\u2013521 (2010). https:\/\/doi.org\/10.1007\/s11873-010-0132-1","journal-title":"Rev. Synth."},{"issue":"8","key":"9643_CR4","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1007\/BF01379806","volume":"35","author":"M Born","year":"1926","unstructured":"Born, M., Heisenberg, W., Jordan, P.: Zur Quantenmechanik. II. Zeitschrift f\u00fcr Physik 35(8), 557\u2013615 (1926). https:\/\/doi.org\/10.1007\/BF01379806","journal-title":"Zur Quantenmechanik. II. Zeitschrift f\u00fcr Physik"},{"key":"9643_CR5","doi-asserted-by":"crossref","unstructured":"Braun, G., Narboux, J.: From Tarski to Hilbert. In: T.\u00a0Ida, J.D. Fleuriot (eds.) Automated Deduction in geometry\u20149th international workshop, ADG 2012, Edinburgh, UK, September 17\u201319, 2012. Revised selected papers, lecture notes in computer science, vol. 7993, pp. 89\u2013109. Springer (2012)","DOI":"10.1007\/978-3-642-40672-0_7"},{"issue":"1","key":"9643_CR6","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/s10992-020-09565-6","volume":"50","author":"L Cocco","year":"2021","unstructured":"Cocco, L., Babic, J.: A system of axioms for Minkowski spacetime. J. Philos. Log. 50(1), 149\u2013185 (2021). https:\/\/doi.org\/10.1007\/s10992-020-09565-6","journal-title":"J. Philos. Log."},{"key":"9643_CR7","doi-asserted-by":"publisher","unstructured":"de Bruijn, N.G.: A survey of the project automath. In: R.P. Nederpelt, J.H. Geuvers, R.C. de Vrijer (eds.) Studies in logic and the foundations of mathematics, selected papers on automath, vol. 133, pp. 141\u2013161. Elsevier (1994). https:\/\/doi.org\/10.1016\/S0049-237X(08)70203-9. Reprinted from: Seldin, J. P. and Hindley, J. R., eds., To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, p. 579-606, by courtesy of Academic Press Inc., Orlando","DOI":"10.1016\/S0049-237X(08)70203-9."},{"key":"9643_CR8","unstructured":"Dedekind, R.: Essays on the Theory of Numbers: I. Continuity and Irrational Numbers. II. The Nature and Meaning of Numbers. Dover Publications, New York (1963)"},{"key":"9643_CR9","doi-asserted-by":"crossref","unstructured":"D\u017eamonja, M., Koutsoukou-Argyraki, A., Paulson, L.C.: Formalising ordinal partition relations using Isabelle\/HOL. arXiv:2011.13218 (2020)","DOI":"10.1080\/10586458.2021.1980464"},{"issue":"8","key":"9643_CR10","doi-asserted-by":"publisher","first-page":"532","DOI":"10.1002\/andp.19083310806","volume":"331","author":"A Einstein","year":"1908","unstructured":"Einstein, A., Laub, J.: \u00dcber die elektromagnetischen Grundgleichungen f\u00fcr bewegte K\u00f6rper. Ann. Phys. 331(8), 532\u2013540 (1908). https:\/\/doi.org\/10.1002\/andp.19083310806","journal-title":"Ann. Phys."},{"key":"9643_CR11","doi-asserted-by":"publisher","unstructured":"Goldblatt, R.: First-Order Spacetime Geometry. In: Fenstad, J.E., Frolov, I.T., Hilpinen, R. (eds.) Studies in logic and the foundations of mathematics, logic, methodology and philosophy of science VIII, vol. 126, pp. 303\u2013316. Elsevier, Amsterdam (1989). https:\/\/doi.org\/10.1016\/S0049-237X(08)70051-X","DOI":"10.1016\/S0049-237X(08)70051-X"},{"key":"9643_CR12","volume-title":"Orthogonality and Spacetime Geometry","author":"R Goldblatt","year":"2012","unstructured":"Goldblatt, R.: Orthogonality and Spacetime Geometry. Springer, New York (2012)"},{"key":"9643_CR13","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF: A Mechanised Logic of Computation","author":"M Gordon","year":"1979","unstructured":"Gordon, M., Milner, R., Wadsworth, C.: Edinburgh LCF: A Mechanised Logic of Computation. Lecture Notes in Computer Science. Springer, Berlin (1979)"},{"key":"9643_CR14","doi-asserted-by":"publisher","unstructured":"Gourgoulhon, \u00c9.: Special Relativity in General Frames: From Particles to Astrophysics. Graduate Texts in Physics. Springer, Berlin (2013). https:\/\/doi.org\/10.1007\/978-3-642-37276-6","DOI":"10.1007\/978-3-642-37276-6"},{"issue":"2","key":"9643_CR15","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevA.81.022109","volume":"81","author":"P Goyal","year":"2010","unstructured":"Goyal, P., Knuth, K.H., Skilling, J.: Origin of complex quantum amplitudes and Feynman\u2019s rules. Phys. Rev. A 81(2), 022109 (2010). https:\/\/doi.org\/10.1103\/PhysRevA.81.022109","journal-title":"Phys. Rev. A"},{"key":"9643_CR16","doi-asserted-by":"crossref","unstructured":"Grabowski, A.: Tarski\u2019s geometry modelled in Mizar computerized proof assistant. In: 2016 Federated Conference on Computer Science and Information Systems (FedCSIS), pp. 373\u2013381 (2016)","DOI":"10.15439\/2016F290"},{"issue":"1","key":"9643_CR17","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/s00454-005-1211-1","volume":"36","author":"TC Hales","year":"2006","unstructured":"Hales, T.C., Ferguson, S.P.: A formulation of the Kepler conjecture. Discrete Comput. Geom. 36(1), 21\u201369 (2006). https:\/\/doi.org\/10.1007\/s00454-005-1211-1","journal-title":"Discrete Comput. Geom."},{"key":"9643_CR18","unstructured":"Hales, T., Adams, M., Bauer, G., Dang, D.T., Harrison, J., Hoang, T.L., Kaliszyk, C., Magron, V., McLaughlin, S., Nguyen, T.T., Nguyen, T.Q., Nipkow, T., Obua, S., Pleso, J., Rute, J., Solovyev, A., Ta, A.H.T., Tran, T.N., Trieu, D.T., Urban, J., Vu, K.K., Zumkeller, R.: A formal proof of the Kepler conjecture. arXiv:1501.02155 (2015)"},{"key":"9643_CR19","doi-asserted-by":"publisher","unstructured":"Harrison, J.: Without loss of generality. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics, pp. 43\u201359. Springer, Berlin (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_3","DOI":"10.1007\/978-3-642-03359-9_3"},{"key":"9643_CR20","volume-title":"The Thirteen Books of Euclid\u2019s Elements","author":"TL Heath","year":"1956","unstructured":"Heath, T.L.: The Thirteen Books of Euclid\u2019s Elements. Courier Corporation, North Chelmsford (1956)"},{"key":"9643_CR21","volume-title":"The Foundations of Geometry","author":"D Hilbert","year":"1950","unstructured":"Hilbert, D.: The Foundations of Geometry. The Open Court Publishing Company, Chicago (1950)"},{"key":"9643_CR22","doi-asserted-by":"publisher","unstructured":"Knuth, K.H.: Understanding the Electron. In: Durham, I.T., Rickles, D. (eds.) Information and Interaction: Eddington, Wheeler, and the Limits of Knowledge, The Frontiers Collection, pp. 181\u2013207. Springer International Publishing, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-43760-6_10","DOI":"10.1007\/978-3-319-43760-6_10"},{"issue":"11","key":"9643_CR23","doi-asserted-by":"publisher","DOI":"10.1063\/1.4899081","volume":"55","author":"KH Knuth","year":"2014","unstructured":"Knuth, K.H., Bahreyni, N.: A potential foundation for emergent space-time. J. Math. Phys. 55(11), 112501 (2014). https:\/\/doi.org\/10.1063\/1.4899081","journal-title":"J. Math. Phys."},{"key":"9643_CR24","doi-asserted-by":"publisher","unstructured":"Kun\u010dar, O., Popescu, A.: Comprehending Isabelle\/HOL\u2019s Consistency. In: Yang, H. (ed.) Programming Languages and Systems. Lecture Notes in Computer Science, pp. 724\u2013749. Springer, Berlin (2017). https:\/\/doi.org\/10.1007\/978-3-662-54434-1_27","DOI":"10.1007\/978-3-662-54434-1_27"},{"key":"9643_CR25","doi-asserted-by":"publisher","unstructured":"Lagarias, J.C.: The Kepler Conjecture and Its Proof. In: Lagarias, J.C. (ed.) The Kepler Conjecture: The Hales\u2013Ferguson Proof, pp. 3\u201326. Springer, New York, NY (2011). https:\/\/doi.org\/10.1007\/978-1-4614-1129-1_1","DOI":"10.1007\/978-1-4614-1129-1_1"},{"key":"9643_CR26","doi-asserted-by":"publisher","unstructured":"Magaud, N., Narboux, J., Schreck, P.: Formalizing Projective Plane Geometry in Coq. In: Sturm, T., Zengler, C. (eds.) Automated Deduction in Geometry. Lecture Notes in Computer Science, pp. 141\u2013162. Springer, Berlin (2011). https:\/\/doi.org\/10.1007\/978-3-642-21046-4_7","DOI":"10.1007\/978-3-642-21046-4_7"},{"key":"9643_CR27","unstructured":"Makarios, T.J.M.: A mechanical verification of the independence of Tarski\u2019s Euclidean axiom. Master\u2019s thesis, Victoria University of Wellington (2012)"},{"key":"9643_CR28","doi-asserted-by":"publisher","unstructured":"Meikle, L.I., Fleuriot, J.D.: Formalizing Hilbert\u2019s Grundlagen in Isabelle\/Isar. In: Basin, D., Wolff, B. (eds.) Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science, pp. 319\u2013334. Springer, Berlin (2003). https:\/\/doi.org\/10.1007\/10930755_21","DOI":"10.1007\/10930755_21"},{"key":"9643_CR29","unstructured":"Minkowski, H.: Die Grundgleichungen f\u00fcr die elektromagnetischen Vorg\u00e4nge in bewegten K\u00f6rpern, pp. 53\u2013111. Nachrichten von der Gesellschaft der Wissenschaften zu G\u00f6ttingen, Mathematisch-Physikalische Klasse pp (1908)"},{"issue":"1","key":"9643_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1086\/289289","volume":"53","author":"B Mundy","year":"1986","unstructured":"Mundy, B.: Optical axiomatization of Minkowski space-time geometry. Philos. Sci. 53(1), 1\u201330 (1986)","journal-title":"Philos. Sci."},{"issue":"1","key":"9643_CR31","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1093\/oxfordjournals.bjps\/37.1.25","volume":"37","author":"B Mundy","year":"1986","unstructured":"Mundy, B.: The physical content of Minkowski geometry. Br. J. Philos. Sci. 37(1), 25\u201354 (1986). https:\/\/doi.org\/10.1093\/oxfordjournals.bjps\/37.1.25","journal-title":"Br. J. Philos. Sci."},{"key":"9643_CR32","doi-asserted-by":"publisher","unstructured":"Narboux, J.: Mechanical Theorem Proving in Tarski\u2019s Geometry. In: Botana, F., Recio, T. (eds.) Automated Deduction in Geometry. Lecture Notes in Computer Science, pp. 139\u2013156. Springer, Berlin (2007). https:\/\/doi.org\/10.1007\/978-3-540-77356-6_9","DOI":"10.1007\/978-3-540-77356-6_9"},{"key":"9643_CR33","doi-asserted-by":"crossref","unstructured":"Narboux, J., Janicic, P., Fleuriot, J.: Computer-Assisted Theorem Proving in Synthetic Geometry, pp. 21\u201360. Chapman and Hall, Baco Raton (2018)","DOI":"10.1201\/9781315121116-2"},{"key":"9643_CR34","unstructured":"Nipkow, T.: Programming and proving in Isabelle\/HOL. https:\/\/isabelle.in.tum.de\/doc\/prog-prove.pdf"},{"key":"9643_CR35","unstructured":"Palmer, J., Fleuriot, J.D.: Mechanising an Independent Axiom System for Minkowski Space-time. In: Proceedings of the 12th international conference on automated deduction in geometry, pp. 64\u201379 (2018)"},{"key":"9643_CR36","doi-asserted-by":"publisher","unstructured":"Paulson, L., Blanchette, J.: Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers. In: International Workshop on the Implementation of Logics (IWIL-2010) (2010). https:\/\/doi.org\/10.29007\/tnfd","DOI":"10.29007\/tnfd"},{"key":"9643_CR37","doi-asserted-by":"crossref","unstructured":"Paulson, L.C., Nipkow, T., Wenzel, M.: From LCF to Isabelle\/HOL. arXiv:1907.02836 (2019)","DOI":"10.1007\/s00165-019-00492-1"},{"key":"9643_CR38","volume-title":"Geometry of Time and Space","author":"AA Robb","year":"1936","unstructured":"Robb, A.A.: Geometry of Time and Space. Cambridge University Press, Cambridge (1936)"},{"key":"9643_CR39","doi-asserted-by":"publisher","unstructured":"Schmoetten, R., Palmer, J., Fleuriot, J.: Formalising Geometric Axioms for Minkowski Spacetime and Without-Loss-of-Generality Theorems. In: P.\u00a0Jani\u010di\u0107, Z.\u00a0Kov\u00e1cs (eds.) Proceedings of the 13th International Conference on Automated Deduction in Geometry, Hagenberg, Austria\/virtual, September 15\u201317, 2021, Electronic Proceedings in Theoretical Computer Science, vol. 352, pp. 116\u2013128. Open Publishing Association (2021). https:\/\/doi.org\/10.4204\/EPTCS.352.13","DOI":"10.4204\/EPTCS.352.13"},{"key":"9643_CR40","unstructured":"Schmoetten, R., Palmer, J., Fleuriot, J.D.: Schutz\u2019 independent axioms for Minkowski spacetime. Archive of Formal Proofs (2021). https:\/\/isa-afp.org\/entries\/Schutz_Spacetime.html"},{"issue":"6","key":"9643_CR41","doi-asserted-by":"publisher","first-page":"1049","DOI":"10.1103\/PhysRev.28.1049","volume":"28","author":"E Schr\u00f6dinger","year":"1926","unstructured":"Schr\u00f6dinger, E.: An undulatory theory of the mechanics of atoms and molecules. Phys. Rev. 28(6), 1049\u20131070 (1926). https:\/\/doi.org\/10.1103\/PhysRev.28.1049","journal-title":"Phys. Rev."},{"key":"9643_CR42","doi-asserted-by":"crossref","unstructured":"Schutz, J.W.: Foundations of Special Relativity: Kinematic Axioms for Minkowski Space-Time. Lecture Notes in Mathematics, vol. 361. Springer, Berlin (1973)","DOI":"10.1007\/BFb0066796"},{"issue":"2","key":"9643_CR43","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1063\/1.524877","volume":"22","author":"JW Schutz","year":"1981","unstructured":"Schutz, J.W.: An axiomatic system for Minkowski space-time. J. Math. Phys. 22(2), 293\u2013302 (1981). https:\/\/doi.org\/10.1063\/1.524877","journal-title":"J. Math. Phys."},{"key":"9643_CR44","volume-title":"Independent Axioms for Minkowski Space-Time","author":"JW Schutz","year":"1997","unstructured":"Schutz, J.W.: Independent Axioms for Minkowski Space-Time. CRC Press, Baco Raton (1997)"},{"issue":"1","key":"9643_CR45","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1016\/0304-3975(93)90095-B","volume":"121","author":"DS Scott","year":"1993","unstructured":"Scott, D.S.: A type-theoretical alternative to ISWIM. CUCH. OWHY. Theor. Comput. Sci. 121(1), 411\u2013440 (1993). https:\/\/doi.org\/10.1016\/0304-3975(93)90095-B","journal-title":"CUCH. OWHY. Theor. Comput. Sci."},{"key":"9643_CR46","unstructured":"Scott, P.: Mechanising Hilbert\u2019s Foundations of Geometry in Isabelle. Master\u2019s thesis, School of Informatics, The University of Edinburgh (2008)"},{"key":"9643_CR47","unstructured":"Scott, P.: Ordered geometry in Hilbert\u2019s Grundlagen der Geometrie. PhD Thesis, The University of Edinburgh, School of Informatics (2015)"},{"key":"9643_CR48","doi-asserted-by":"crossref","unstructured":"Scott, P., Fleuriot, J.: An Investigation of Hilbert\u2019s Implicit Reasoning through Proof Discovery in Idle-Time. In: Schreck, P., Narboux, J., Richter-Gebert, J. (eds.) Automated Deduction in Geometry. Lecture Notes in Computer Science, pp. 182\u2013200. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-25070-5_11"},{"issue":"4","key":"9643_CR49","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/s10817-013-9292-7","volume":"52","author":"M Stannett","year":"2014","unstructured":"Stannett, M., N\u00e9meti, I.: Using Isabelle\/HOL to verify first-order relativity theory. J. Autom. Reason. 52(4), 361\u2013378 (2014). https:\/\/doi.org\/10.1007\/s10817-013-9292-7","journal-title":"J. Autom. Reason."},{"key":"9643_CR50","unstructured":"Streater, R.F., Wightman, A.S.: PCT, Spin and Statistics, and All That., corr. 3rd print. of the 1978 ed. edn. Princeton Landmarks in Physics. Princeton University Press, Princeton, NJ (2000)"},{"issue":"20","key":"9643_CR51","doi-asserted-by":"publisher","first-page":"651","DOI":"10.2307\/2024318","volume":"65","author":"P Suppes","year":"1968","unstructured":"Suppes, P.: The desirability of formalization in science. J. Philos. 65(20), 651\u2013664 (1968). https:\/\/doi.org\/10.2307\/2024318","journal-title":"J. Philos."},{"key":"9643_CR52","doi-asserted-by":"crossref","unstructured":"Szekeres, G.: Kinematic geometry; an axiomatic system for Minkowski space\u2013time: M. L. Urquhart in Memoriam. J. Austral. Math. Soc. 8(2), 134\u2013160 (1968)","DOI":"10.1017\/S1446788700005188"},{"key":"9643_CR53","unstructured":"\u2019t Hooft, G.: Introduction to General Relativity. https:\/\/webspace.science.uu.nl\/~hooft101\/lectures\/genrel_2013.pdf (2012)"},{"key":"9643_CR54","doi-asserted-by":"publisher","unstructured":"Tarski, A.: What is Elementary Geometry? In: Henkin, L., Suppes, P., Tarski, A. (eds.) Studies in Logic and the Foundations of Mathematics, The Axiomatic Method, vol. 27, pp. 16\u201329. Elsevier, Amsterdam (1959). https:\/\/doi.org\/10.1016\/S0049-237X(09)70017-5","DOI":"10.1016\/S0049-237X(09)70017-5"},{"issue":"3","key":"9643_CR55","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1090\/S0002-9947-1904-1500678-X","volume":"5","author":"O Veblen","year":"1904","unstructured":"Veblen, O.: A system of axioms for geometry. Trans. Am. Math. Soc. 5(3), 343\u2013384 (1904)","journal-title":"Trans. Am. Math. Soc."},{"key":"9643_CR56","doi-asserted-by":"publisher","unstructured":"Walker, A.G.: Axioms for Cosmology. In: Henkin, L., Suppes, P., Tarski, A. (eds.) Studies in Logic and the Foundations of Mathematics, The Axiomatic Method, vol. 27, pp. 308\u2013321. Elsevier, Amsterdam (1959). https:\/\/doi.org\/10.1016\/S0049-237X(09)70036-9","DOI":"10.1016\/S0049-237X(09)70036-9"},{"key":"9643_CR57","doi-asserted-by":"publisher","unstructured":"Wenzel, M.: Isar\u2014A Generic Interpretative Approach to Readable Formal Proof Documents. In: Bertot, Y., Dowek, G., Th\u00e9ry, L., Hirschowitz, A., Paulin, C. (eds.) Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science, pp. 167\u2013183. Springer, Berlin (1999). https:\/\/doi.org\/10.1007\/3-540-48256-3_12","DOI":"10.1007\/3-540-48256-3_12"},{"key":"9643_CR58","unstructured":"Wenzel, M.: The Isabelle\/Isar Reference Manual. https:\/\/isabelle.in.tum.de\/doc\/isar-ref.pdf"},{"key":"9643_CR59","doi-asserted-by":"publisher","unstructured":"Wenzel, M., Paulson, L.C., Nipkow, T.: The Isabelle Framework. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science, pp. 33\u201338. Springer, Berlin (2008). https:\/\/doi.org\/10.1007\/978-3-540-71067-7_7","DOI":"10.1007\/978-3-540-71067-7_7"},{"key":"9643_CR60","volume-title":"The De Bruijn factor","author":"F Wiedijk","year":"2000","unstructured":"Wiedijk, F.: The De Bruijn factor. Department of Computer Science, Nijmegen University, Tech. rep (2000)"}],"updated-by":[{"DOI":"10.1007\/s10817-022-09651-1","type":"correction","label":"Correction","source":"publisher","updated":{"date-parts":[[2023,1,13]],"date-time":"2023-01-13T00:00:00Z","timestamp":1673568000000}}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09643-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-022-09643-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09643-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,13]],"date-time":"2023-01-13T02:13:43Z","timestamp":1673576023000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-022-09643-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,1]]},"references-count":60,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2022,11]]}},"alternative-id":["9643"],"URL":"https:\/\/doi.org\/10.1007\/s10817-022-09643-1","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,10,1]]},"assertion":[{"value":"18 July 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"31 July 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 October 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 January 2023","order":4,"name":"change_date","label":"Change Date","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Correction","order":5,"name":"change_type","label":"Change Type","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"A Correction to this paper has been published:","order":6,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"https:\/\/doi.org\/10.1007\/s10817-022-09651-1","URL":"https:\/\/doi.org\/10.1007\/s10817-022-09651-1","order":7,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}}]}}