pith. sign in

arxiv: 2605.27246 · v1 · pith:6W27LMICnew · submitted 2026-05-26 · 💻 cs.LO · cs.AI· math.LO

Many Logics, One Methodology: A Plea for Logical Pluralism in Formalised Reasoning (preprint)

Christoph Benzm\"uller , Daniel Kirchner , Luca Pasetto This is my paper

Pith reviewed 2026-06-29 14:38 UTC · model grok-4.3

classification 💻 cs.LO cs.AImath.LO
keywords logical pluralismshallow embeddingshigher-order logicformal reasoningproof assistantscomputational metaphysicsknowledge representation
0
0 comments X

The pith

Logical pluralism at the object level inside one meta-framework enables reuse across disciplines that single-logic approaches block.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper reviews twenty years of embedding non-classical logics into classical higher-order logic and presents this work as evidence that a pluralistic stance at the object-logic level, housed inside a single meta-framework, supports wider reuse of formal developments. It contrasts this stance with logical imperialism, the practice of committing an entire large theory to one foundational logic, and claims the latter creates barriers to interdisciplinary application. The argument is anchored in the authors' LogiKEy methodology and in computational metaphysics. A reader would care because the choice affects how readily formal methods can cross from pure logic into metaphysics, computer science, and related fields without repeated reformulation.

Core claim

After two decades of shallow embeddings, a unifying meta-logical framework such as LogiKEy makes it feasible and advantageous to employ many different object logics side by side rather than locking large-scale formalizations into one logic; this pluralism at the object level, the paper states, directly enables the interdisciplinary reuse that logical imperialism impedes.

What carries the argument

Shallow embeddings of non-classical logics into classical higher-order logic, used as a unifying meta-framework that hosts multiple object logics without forcing commitment to any single one.

If this is right

  • Formal developments in metaphysics and other disciplines can share components without translation into a single mandated logic.
  • Proof assistants gain value by natively supporting multiple object logics rather than enforcing one foundational choice.
  • Interdisciplinary projects avoid the repeated reformulation costs imposed when every theory must conform to one logic.
  • Computational metaphysics proceeds more flexibly by selecting the object logic suited to each subproblem inside the same meta-framework.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same embedding technique could be applied inside other meta-logics besides classical HOL if those meta-logics prove equally expressive.
  • Designers of future proof assistants might treat support for multiple object logics as a baseline requirement rather than an optional extension.
  • Empirical trials in domains such as legal reasoning or ethical modeling could quantify the reuse gains the paper describes.

Load-bearing premise

The accumulated practical results from two decades of shallow embeddings already supply enough evidence to justify recommending logical pluralism for proof assistants in general.

What would settle it

A concrete large-scale formalization project carried out once under a single fixed logic and once under the pluralistic LogiKEy approach, with measured reuse across domains, would show whether the claimed advantage materializes or fails to appear.

Figures

Figures reproduced from arXiv: 2605.27246 by Christoph Benzm\"uller, Daniel Kirchner, Luca Pasetto.

Figure 1
Figure 1. Figure 1: The logic-pluralistic knowledge representation and reasoning methodology LogiKEy instantiated for the application direction proposed in this paper. sketched here, where mathematical theories must interface with other disciplines that do not share—or actively reject—the foundational assumptions underlying those libraries. The remainder of this paper is organised as follows. Section 2 introduces the LogiKEy … view at source ↗
Figure 2
Figure 2. Figure 2: Shallow embedding of higher-order modal logic (HOML) in the classical higher￾order logic (HOL) of Isabelle/HOL utilizing the LogiKEy methodology. Reader’s guide: ι is the type of (possibly non-actual) individuals, µ the type of worlds, and o the HOL Booleans; the abbreviations σ := µ → o and τ := ι → σ collect world-relativised propositions and world-relativised (individual) properties, respectively (occur… view at source ↗
Figure 3
Figure 3. Figure 3: Set filter and ultrafilter formalised for our modal logic setting. The types here can be read off as follows: a modal set is a world-relativised predicate of type τ (so it picks out, at each world, a subset of individuals), and a modal set of modal sets accordingly has type τ → σ. With this typing, Subset relates two modal sets (the inclusion is required to hold at every world), whereas Element relates a m… view at source ↗
Figure 4
Figure 4. Figure 4: Modalised versions of core (schematic) postulates of Church’s Type Theory are proven as lemmata, and further modalised mathematical notions are provided as naturally embedded and analysable concepts in HOL. Two notes may help to read the figure. First, CardinalNumbers (line 26) holds of a (modal) collection u when u is the equipollence class of some witness p. Second, the successor operator S on cardinals … view at source ↗
Figure 5
Figure 5. Figure 5: Checking/verifying parts of Andrews’ textbook [1] at the layer of HOML; the development is useful also for educational purposes. (This formalisation of Andrews’ development is exploratory and partial: it is intended to illustrate the approach rather than to provide a complete treatment, which is left for an extended version of this paper.) [PITH_FULL_IMAGE:figures/full_fig_p015_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: The verification of Gödel’s original modal ontological argument [22] from [13], enriched by a preliminary study on the cardinality of positive properties under the assumption of different existing (e.g., mathematical) entities [PITH_FULL_IMAGE:figures/full_fig_p016_6.png] view at source ↗
read the original abstract

This position statement looks back on two decades of work on shallow embeddings of non-classical logics in classical higher-order logic (HOL), a line of research that expanded into a range of logic embeddings in HOL and inspired the LogiKEy logic-pluralistic knowledge representation and reasoning methodology. This paper advances the case for logical pluralism at object-logic level within a unifying meta-logical framework such as LogiKEy, grounding the argument in computational metaphysics. More broadly, it advocates principled support for logical pluralism in modern proof assistants, and cautions against logical imperialism -- the rigid adoption of a single foundational logic for large-scale theory developments -- which impedes the interdisciplinary reuse that LogiKEy is designed to enable.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 0 minor

Summary. The paper is a position statement that reviews two decades of the authors' work on shallow embeddings of non-classical logics into classical higher-order logic (HOL) and the resulting LogiKEy methodology. It argues that logical pluralism at the object-logic level, embedded within a unifying meta-logical framework, enables interdisciplinary reuse in formalised reasoning and computational metaphysics, while cautioning against logical imperialism (the rigid use of a single foundational logic) that impedes such reuse.

Significance. If the advocated methodology gains traction, it could encourage proof-assistant designers to support multiple object logics rather than enforcing a single foundation, potentially improving reuse across logic, metaphysics, and AI. The paper explicitly credits its own prior embeddings and LogiKEy as the concrete demonstration of the pluralist approach.

major comments (1)
  1. [Introduction] Introduction and the section grounding the argument in computational metaphysics: the claim that pluralism within LogiKEy 'enables the interdisciplinary reuse that logical imperialism impedes' rests entirely on the authors' own prior embeddings and methodology as both the evidence base and the recommended solution, creating a self-referential structure that does not address whether independent groups have achieved comparable reuse without LogiKEy.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the constructive review and the recommendation of minor revision. We address the single major comment below.

read point-by-point responses

  1. Referee: [Introduction] Introduction and the section grounding the argument in computational metaphysics: the claim that pluralism within LogiKEy 'enables the interdisciplinary reuse that logical imperialism impedes' rests entirely on the authors' own prior embeddings and methodology as both the evidence base and the recommended solution, creating a self-referential structure that does not address whether independent groups have achieved comparable reuse without LogiKEy.

    Authors: We agree that the paper is a position statement that draws its concrete evidence from the authors' own two decades of work on shallow embeddings and the LogiKEy methodology. This self-referential character is inherent to the genre of the paper, which explicitly presents itself as a retrospective on that research program. The central claim is therefore illustrative rather than a universal empirical assertion. To address the concern, we will revise the introduction and the computational-metaphysics section to (i) state more explicitly that the argument for object-level pluralism within a HOL meta-framework is independent of any single methodology and (ii) note that LogiKEy is offered as one demonstrated instance rather than the sole solution. We will also add a short paragraph acknowledging that broader adoption by independent groups remains an open question for future work. revision: partial

Circularity Check

0 steps flagged

No significant circularity; position paper with independent methodological argument

full rationale

The manuscript is an advocacy/position paper whose central claim is a recommendation for logical pluralism inside a meta-framework such as LogiKEy. No technical derivation, theorem, equation, or fitted parameter is advanced. The text cites the authors' prior embeddings work as historical motivation and practical illustration, but the recommendation itself does not reduce to those citations by construction, nor does any uniqueness theorem or ansatz get smuggled in to force a result. The argument remains self-contained as an interdisciplinary plea and does not meet any of the enumerated circularity patterns.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Position paper containing no new mathematical derivations, fitted parameters, or invented entities; the argument relies on narrative reference to prior work.

pith-pipeline@v0.9.1-grok · 5659 in / 969 out tokens · 29884 ms · 2026-06-29T14:38:00.720014+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

41 extracted references · 21 canonical work pages · 1 internal anchor

  1. [1]

    P. B. Andrews.An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Second. Kluwer Academic Publishers, 2002

    2002

  2. [2]

    In: Medical Image Computing and Computer Assisted Intervention – MICCAI 2025

    C. Benzmüller. “Faithful Logic Embeddings in HOL – Deep and Shallow”. In: Automated Deduction – CADE-30 – 30th International Conference on Automated Deduction, Proceedings. Ed. by C. Barrett and U. Waldmann. Vol. 15943. LNCS. Preprint: arXiv:2502.19311. Springer, 2025, pp. 280–302.doi:10.1007/978-3- 031-99984-0_16

    work page doi:10.1007/978-3- 2025

  3. [3]

    Universal (Meta-)Logical Reasoning: Recent Successes

    C. Benzmüller. “Universal (Meta-)Logical Reasoning: Recent Successes”. In:Sci- ence of Computer Programming172 (2019), pp. 48–62.doi:10.1016/j.scico. 2018.10.008. Many Logics, One Methodology 19

    work page doi:10.1016/j.scico 2019

  4. [4]

    Church’s Type Theory

    C. Benzmüller and P. Andrews. “Church’s Type Theory”. In:The Stanford En- cyclopedia of Philosophy. Ed. by E. N. Zalta and U. Nodelman. Spring 2024. Metaphysics Research Lab, Stanford University, 2024.url:https : / / plato . stanford.edu/archives/spr2024/entries/type-theory-church/

    2024

  5. [5]

    Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel’s Ontological Argument

    C. Benzmüller and D. Fuenmayor. “Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel’s Ontological Argument”. In:Bulletin of the Section of Logic49.2 (2020), pp. 127–148.doi: 10.18778/0138-0680.2020.08

    work page doi:10.18778/0138-0680.2020.08 2020

  6. [6]

    First-Order Modal Logic in HOL: Deep and Shallow Embeddings with Automated Faithfulness

    C. Benzmüller and D. Kirchner. “First-Order Modal Logic in HOL: Deep and Shallow Embeddings with Automated Faithfulness”. In: Submitted. 2026

    2026

  7. [7]

    Designing Normative Theories for Ethical and Legal Reasoning: LogiKEy Framework, Methodology, and Tool Support

    C. Benzmüller, X. Parent, and L. van der Torre. “Designing Normative Theories for Ethical and Legal Reasoning: LogiKEy Framework, Methodology, and Tool Support”. In:Artificial Intelligence287 (2020), p. 103348.doi:10 . 1016 / j . artint.2020.103348

    work page arXiv 2020

  8. [8]

    Exploring Properties of Normal Multimodal Logics in Simple Type Theory with LEO-II

    C. Benzmüller and L. C. Paulson. “Exploring Properties of Normal Multimodal Logics in Simple Type Theory with LEO-II”. In:Reasoning in Simple Type The- ory — Festschrift in Honor of Peter B. Andrews on His 70th Birthday. Ed. by C. Benzmüller, C. Brown, J. Siekmann, and R. Statman. Studies in Logic, Math- ematical Logic and Foundations. College Publication...

    2008

  9. [9]

    MultimodalandIntuitionisticLogicsinSimple Type Theory

    C.BenzmüllerandL.C.Paulson.“MultimodalandIntuitionisticLogicsinSimple Type Theory”. In:The Logic Journal of the IGPL18.6 (2010), pp. 881–892.doi: 10.1093/jigpal/jzp080

    work page doi:10.1093/jigpal/jzp080 2010

  10. [10]

    Quantified Multimodal Logics in Simple Type Theory

    C. Benzmüller and L. C. Paulson.Quantified Multimodal Logics in Simple Type Theory. Tech. rep. DFKI Bremen GmbH, Safe and Secure Cognitive Systems, Cartesium, Enrique Schmidt Str.5, D–28359 Bremen, Germany: Saarland Uni- versity, 2009.doi:10.48550/arXiv.0905.2435

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.0905.2435 2009

  11. [11]

    Quantified Multimodal Logics in Simple Type Theory

    C. Benzmüller and L. C. Paulson. “Quantified Multimodal Logics in Simple Type Theory”. In:Logica Universalis (Special Issue on Multimodal Logics)7.1 (2013), pp. 7–20.doi:10.1007/s11787-012-0052-y

    work page doi:10.1007/s11787-012-0052-y 2013

  12. [12]

    Automating Free Logic in HOL, with an Exper- imental Application in Category Theory

    C. Benzmüller and D. S. Scott. “Automating Free Logic in HOL, with an Exper- imental Application in Category Theory”. In:Journal of Automated Reasoning 64.1 (2020), pp. 53–72.doi:10.1007/s10817-018-09507-7

    work page doi:10.1007/s10817-018-09507-7 2020

  13. [13]

    Notes on Gödel’s and Scott’s Variants of the Ontological Argument

    C. Benzmüller and D. S. Scott. “Notes on Gödel’s and Scott’s Variants of the Ontological Argument”. In:Monatshefte für Mathematik208 (2025), pp. 569– 611.doi:10.1007/s00605-025-02078-x

    work page doi:10.1007/s00605-025-02078-x 2025

  14. [14]

    Notes on Gödel’s and Scott’s Variants of the Ontological Argument (Isabelle/HOL dataset)

    C. Benzmüller and D. S. Scott. “Notes on Gödel’s and Scott’s Variants of the Ontological Argument (Isabelle/HOL dataset)”. In:Archive of Formal Proofs (2025).url:https : / / www . isa - afp . org / entries / Notes _ On _ Goedels _ Ontological_Argument.html

    2025

  15. [15]

    The Higher-Order Prover LEO-II

    C. Benzmüller, N. Sultana, L. C. Paulson, and F. Theiss. “The Higher-Order Prover LEO-II”. In:Journal of Automated Reasoning55.4 (2015), pp. 389–404. doi:10.1007/s10817-015-9348-y

    work page doi:10.1007/s10817-015-9348-y 2015

  16. [16]

    LEO-II - A Coopera- tive Automatic Theorem Prover for Higher-Order Logic (System Description)

    C. Benzmüller, F. Theiss, L. C. Paulson, and A. Fietzke. “LEO-II - A Coopera- tive Automatic Theorem Prover for Higher-Order Logic (System Description)”. In:Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Pro- ceedings. Ed. by A. Armando, P. Baumgartner, and G. Dowek. Vol. 5195. LNCS. Springer, 2008, pp. 162–170.doi:10.1007/978-3-540-...

    work page doi:10.1007/978-3-540-71070-7_14 2008

  17. [17]

    Automating Gödel’s Ontological Proof of God’s Existence with Higher-order Automated Theorem Provers

    C. Benzmüller and B. Woltzenlogel Paleo. “Automating Gödel’s Ontological Proof of God’s Existence with Higher-order Automated Theorem Provers”. In: 20 Christoph Benzmüller, Daniel Kirchner, and Luca Pasetto ECAI 2014. Ed. by T. Schaub, G. Friedrich, and B. O’Sullivan. Vol. 263. Fron- tiers in Artificial Intelligence and Applications. IOS Press, 2014, pp. ...

    work page doi:10.3233/978-1-61499-419-0-93 2014

  18. [18]

    Interacting with Modal Logics in the Coq Proof Assistant

    C. Benzmüller and B. Woltzenlogel Paleo. “Interacting with Modal Logics in the Coq Proof Assistant”. In:Computer Science - Theory and Applications - 10th International Computer Science Symposium in Russia, CSR 2015, Proceedings. Ed. by L. D. Beklemishev and D. V. Musatov. Vol. 9139. LNCS. Springer, 2015, pp. 398–411.doi:10.1007/978-3-319-20297-6_25

    work page doi:10.1007/978-3-319-20297-6_25 2015

  19. [19]

    The Inconsistency in Gödel’s On- tological Argument: A Success Story for AI in Metaphysics

    C. Benzmüller and B. Woltzenlogel Paleo. “The Inconsistency in Gödel’s On- tological Argument: A Success Story for AI in Metaphysics”. In:IJCAI 2016. Ed. by S. Kambhampati. Vol. 1-3. AAAI Press, 2016, pp. 936–942

    2016

  20. [20]

    Bertot and P

    Y. Bertot and P. Casteran.Interactive Theorem Proving and Program Develop- ment. Springer, 2004

    2004

  21. [21]

    A Formulation of the Simple Theory of Types

    A. Church. “A Formulation of the Simple Theory of Types”. In:Journal of Sym- bolic Logic5.2 (1940), pp. 56–68.doi:10.2307/2266170

    work page doi:10.2307/2266170 1940

  22. [22]

    Appendix A: Notes in Kurt Gödel’s Hand

    K. Gödel. “Appendix A: Notes in Kurt Gödel’s Hand”. In:Logic and Theism. Ed. by J. Sobel. Cambridge University Press, 1970, pp. 144–145

    1970

  23. [23]

    Computer-Verified Foundations of Metaphysics and an Ontology of Natural Numbers in Isabelle/HOL

    D. Kirchner. “Computer-Verified Foundations of Metaphysics and an Ontology of Natural Numbers in Isabelle/HOL”. PhD thesis. Freie Universität Berlin, 2022. doi:10.17169/refubium-35141

    work page doi:10.17169/refubium-35141 2022

  24. [24]

    The Definition of E(xistence)! in Free Logic

    K. Lambert. “The Definition of E(xistence)! in Free Logic”. In:Abstracts: The In- ternational Congress for Logic, Methodology and Philosophy of Science. Stanford U. Press, 1960

    1960

  25. [25]

    Diagonal Arguments and Cartesian Closed Categories with Au- thor Commentary

    F. W. Lawvere. “Diagonal Arguments and Cartesian Closed Categories with Au- thor Commentary”. In:Reprints in Theory and Applications of Categories15 (2006). Reprint, with commentary, of the 1969 original (Lecture Notes in Math- ematics, vol. 92, Springer), pp. 1–13.url:http : / / www . tac . mta . ca / tac / reprints/articles/15/tr15abs.html

    2006

  26. [26]

    doi: 10.1007/978-3-030-79876-5_37

    L. de Moura and S. Ullrich. “The Lean 4 Theorem Prover and Programming Language”. In:Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Proceedings. Ed. by A. Platzer and G. Sutcliffe. LNCS. Springer, 2021, pp. 625–635.doi:10.1007/978-3-030-79876-5_37

    work page doi:10.1007/978-3-030-79876-5_37 2021

  27. [27]

    On the maximality of positive properties and modal collapse in variants of Gödel’s ontological proof of God

    C. Mühlenbeck and C. Benzmüller. “On the maximality of positive properties and modal collapse in variants of Gödel’s ontological proof of God”. In:Logic and Logical Philosophy(2026), pp. 1–21.doi:10.12775/LLP.2026.007.url: https://apcz.umk.pl/LLP/article/view/55901

    work page doi:10.12775/llp.2026.007.url: 2026

  28. [28]

    Nipkow, L

    T. Nipkow, L. C. Paulson, and M. Wenzel.Isabelle/HOL - A Proof Assistant for Higher-Order Logic. Vol. 2283. LNCS. Springer, 2002.doi:10.1007/3-540- 45949-9

    work page doi:10.1007/3-540- 2002

  29. [29]

    Partizan Games in Isabelle/HOLZF

    S. Obua. “Partizan Games in Isabelle/HOLZF”. In:Theoretical Aspects of Com- puting – ICTAC 2006. Vol. 4281. LNCS. Springer, 2006, pp. 272–286.doi:10. 1007/11921240_19

    2006

  30. [30]

    Isabelle: The Next 700 Theorem Provers

    L. C. Paulson. “Isabelle: The Next 700 Theorem Provers”. In:CoRR cs.LO/9301106 (1993).url:https://arxiv.org/abs/cs/9301106

    work page arXiv 1993

  31. [31]

    L. C. Paulson.ZFC in HOL. Archive of Formal Proofs. 2019

    2019

  32. [32]

    Logical Pluralism

    G. Russell and C. Blake-Turner. “Logical Pluralism”. In:The Stanford Encyclo- pedia of Philosophy. Ed. by E. N. Zalta and U. Nodelman. Fall 2023. Metaphysics Research Lab, Stanford University, 2023

    2023

  33. [33]

    Appendix B: Notes in Dana Scott’s Hand

    D. Scott. “Appendix B: Notes in Dana Scott’s Hand”. In:Logic and Theism. Ed. by J. Sobel. Cambridge University Press, 1972, pp. 145–146. Many Logics, One Methodology 21

    1972

  34. [34]

    Existence and description in formal logic

    D. Scott. “Existence and description in formal logic”. In:Bertrand Russell: Philosopher of the Century. Ed. by R. Schoenman. (See also: Philosophical Ap- plication of Free Logic, edited by K. Lambert. Oxford:OUP, 1991, pp. 28 - 48). George Allen & Unwin, London, 1967, pp. 181–200

    1991

  35. [35]

    Extensional Higher-Order Paramodulation in Leo- III

    A. Steen and C. Benzmüller. “Extensional Higher-Order Paramodulation in Leo- III”. In:Journal of Automated Reasoning65.6 (2021), pp. 775–807.doi:10 . 1007/s10817-021-09588-x

    2021

  36. [36]

    Solving Quantified Modal Logic Prob- lems by Translation to Classical Logics

    A. Steen, G. Sutcliffe, and C. Benzmüller. “Solving Quantified Modal Logic Prob- lems by Translation to Classical Logics”. In:Journal of Logic and Computation 35.4 (2025), pp. 1–23.doi:10.1093/logcom/exaf006

    work page doi:10.1093/logcom/exaf006 2025

  37. [37]

    The lean mathematical library

    The mathlib Community. “The lean mathematical library”. In:Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. CPP 2020. New Orleans, LA, USA: Association for Computing Machinery, 2020, pp. 367–381.doi:10.1145/3372885.3373824

    work page doi:10.1145/3372885.3373824 2020

  38. [38]

    E. N. Zalta.Abstract Objects: An Introduction to Axiomatic Metaphysics. Vol. 160. Synthese Library. Dordrecht, Boston, and Lancaster: D. Reidel Pub- lishing Company, 1983, pp. xiii + 193

    1983

  39. [39]

    E. N. Zalta.Intensional Logic and the Metaphysics of Intentionality. Bradford Books. Cambridge, MA: The MIT Press, 1988, pp. xiii + 256

    1988

  40. [40]

    Principia Logico-Metaphysica (Draft/Excerpt)

    E. N. Zalta. “Principia Logico-Metaphysica (Draft/Excerpt)”. Available at https://mally.stanford.edu/principia.pdf[accessed 24-May-2026]. 2026

    2026

  41. [41]

    Unifying and Validating Some Ideas of Kurt Gödel

    E. N. Zalta. “Unifying and Validating Some Ideas of Kurt Gödel”. Awarded contribution to the 2025 Kurt Gödel Essay Prize; available online athttps : //tinyurl.com/35t36nvz[accessed 26-May-2026]. 2025

    2025