Craig插值法用于Here和There逻辑及其Mintssequent系统的变种
Craig-Lyndon Interpolation for the Logic of Here and There with a Variation of Mints' Sequent System
AI总结：
本文提出了一种基于Mintssequent系统的HT逻辑Craig插值法，通过两阶段构造非经典逻辑中的插值项，以解决HT逻辑的插值问题。
摘要：
我们提出了一个Maehara风格的构造方法，用于为Here和There（HT）三值命题逻辑（也称为Gödel的G₃）构造Craig插值项。该方法将一种最近用于经典编码逻辑程序的插值技术适应到Mints为HT设计的sequent算法规则变种上。该方法分为两个阶段：首先构造一个初步插值项，这是一个在某种意义上是插值项的公式，但尚未成为所需的HT公式。在第二阶段，通过此初步插值项获得实际的HT插值项。在经典编码下，初步插值项是经典编码下两个输入HT公式的经典Craig插值项。在所提出的适应中，sequent系统直接作用于HT公式，而初步插值项则处于一种扩展了HT的非经典逻辑中，通过增加一个额外的逻辑运算符来一般化HT。
英文摘要：
We present a variation of Maehara's method to construct Craig-Lyndon interpolants for the three-valued propositional logic of here and there (HT), also known as Gödel's $G_3$, a superintuitionistic logic of importance in logic programming. Our method adapts a recent interpolation technique that operates on classically encoded logic programs to a variation of Mints' sequent system for HT. 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-Lyndon 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
