We present automated theorem provers for the first-order logic of here and there (HT). They are based on a native sequent calculus for the logic of HT and an axiomatic embedding of the logic of HT into intuitionistic logic. The analytic proof search in the sequent calculus is optimized by using free variables and skolemization. The embedding is used in combination with sequent, tableau and connection calculi for intuitionistic first-order logic. All provers are evaluated on a large benchmark set of first-order formulas, providing a foundation for the development of more efficient HT provers.

翻译：本文提出了针对此处与彼处一阶逻辑（HT）的自动定理证明器。这些证明器基于HT逻辑的原生矢列演算，以及HT逻辑到直觉主义逻辑的公理化嵌入方法。通过采用自由变量与斯科伦化技术，我们对矢列演算中的解析证明搜索过程进行了优化。该嵌入方法可与直觉主义一阶逻辑的矢列演算、表演算及连接演算结合使用。所有证明器均在大型一阶逻辑公式基准测试集上进行了评估，为开发更高效的HT证明器奠定了理论基础。