Kuroda's translation embeds classical first-order logic into intuitionistic logic, through the insertion of double negations. Recently, Brown and Rizkallah extended this translation to higher-order logic. In this paper, we adapt it for theories encoded in higher-order logic in the lambdaPi-calculus modulo theory, a logical framework that extends lambda-calculus with dependent types and user-defined rewrite rules. We develop a tool that implements Kuroda's translation for proofs written in Dedukti, a proof language based on the lambdaPi-calculus modulo theory.

翻译：Kuroda 翻译通过插入双重否定，将经典一阶逻辑嵌入直觉主义逻辑。最近，Brown 和 Rizkallah 将这一翻译推广至高阶逻辑。本文针对在 λΠ-演算模理论（一种通过依赖类型和用户自定义重写规则扩展 λ-演算的逻辑框架）中编码的高阶逻辑理论，对该翻译方法进行了适配。我们开发了一个工具，用于实现针对基于 λΠ-演算模理论的证明语言 Dedukti 所编写证明的 Kuroda 翻译。