We present a Maehara-style construction of Craig interpolants for the three-valued propositional logic of here and there (HT), also known as Gödel's $G_3$. The method adapts a recent interpolation technique that operates on classically encoded logic programs to a variation of a sequent calculus for HT by Mints. The approach is characterized by two stages: First, a preliminary interpolant is constructed, a formula that is an interpolant in some sense, but not yet the desired HT formula. In the second stage, an actual HT interpolant is obtained from this preliminary interpolant. With the classical encoding, the preliminary interpolant is a classical Craig interpolant for classical encodings of the two input HT formulas. In the presented adaptation, the sequent system operates directly on HT formulas, and the preliminary interpolant is in a nonclassical logic that generalizes HT by an additional logic operator.

翻译：本文针对三值命题逻辑"此时此地"（HT，亦称哥德尔$G_3$逻辑）提出了一种前原风格的克雷格插值构造方法。该方法将近期一种基于经典编码逻辑程序的插值技术，适配至Mints提出的HT矢列演算变体。该方法的特征在于两个阶段：首先构造预备插值式——这是一种在某种意义上的插值公式，但尚未成为目标HT公式；第二阶段则从此预备插值式中导出真正的HT插值式。在经典编码框架下，预备插值式是两个输入HT公式经典编码的经典克雷格插值式。而在本文提出的适配方案中，矢列系统直接对HT公式进行演算，所得预备插值式属于一种通过附加逻辑算子扩展HT的非经典逻辑。