主张在统一框架中支持多种逻辑，避免单一逻辑垄断。
Many Logics, One Methodology: A Plea for Logical Pluralism in Formalised Reasoning (preprint)
- 以LogiKEy为统一框架，实现多种非经典逻辑的浅嵌入
- 强调逻辑多元主义可促进跨学科知识复用
- 反对证明助手中的逻辑帝国主义，提倡灵活兼容
本文回顾了过去二十年在高阶逻辑（HOL）中浅嵌入非经典逻辑的研究进展，该方向发展出一系列逻辑到HOL的嵌入方法，并催生了支持逻辑多元主义的知识表示与推理框架LogiKEy。本文进一步在计算本体论基础上，倡导在统一元逻辑框架内于对象逻辑层面支持逻辑多元主义。更广泛地，主张现代证明助手应具备对逻辑多元主义的原则性支持，警惕‘逻辑帝国主义’——即为大规模理论构建强行采用单一基础逻辑——这种做法会阻碍跨学科知识的复用，而正是LogiKEy所致力于实现的目标。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。