众多逻辑，单一方法论：关于形式化推理中逻辑复数主义的呼吁

本立场陈述回顾了两个多年来关于在经典高阶逻辑（Higher-Order Logic, HOL）中对非经典逻辑进行浅层嵌入的研究，这一研究线索扩展为一系列在 HOL 中进行的逻辑嵌入，并催生了 LogiKEy 逻辑复数主义知识表示与推理方法论。这篇论文在计算形而上学的基础上，为在诸如 LogiKEy 之类的统一元逻辑框架内支持对象层次逻辑复数主义提供论据。更广泛地，它倡导在现代证明助理中原则性地支持逻辑复数主义，并警戒逻辑帝国主义——即对大规模理论发展严格采用单一基础逻辑的做法——这会阻碍 LogiKEy 旨在启用的跨学科复用。