In the recent years, the Metis prover based on ordered paramodulation and model elimination has replaced the earlier built-in methods for general-purpose proof automation in HOL4 and Isabelle/HOL. In the annual CASC competition, the leanCoP system based on connection tableaux has however performed better than Metis. In this paper we show how the leanCoP's core algorithm can be implemented inside HOLLight. leanCoP's flagship feature, namely its minimalistic core, results in a very simple proof system. This plays a crucial role in extending the MESON proof reconstruction mechanism to connection tableaux proofs, providing an implementation of leanCoP that certifies its proofs. We discuss the differences between our direct implementation using an explicit Prolog stack, to the continuation passing implementation of MESON present in HOLLight and compare their performance on all core HOLLight goals. The resulting prover can be also used as a general purpose TPTP prover. We compare its performance against the resolution based Metis on TPTP and other interesting datasets.

翻译：近些年来,基于定购配制和模式消除的梅蒂斯证明书取代了HOL4和Isabelle/HOL中早先的通用证明自动化固有方法。在CASC年度竞赛中,基于连接表的精密CoP系统取得了优于梅蒂斯的成绩。在本文中,我们展示了如何在HOLLight中实施精干CoP的核心算法。精干CoP的旗舰特征,即其最小核心,导致形成一个非常简单的验证系统。这在将MESON证据重建机制扩展至连接表单证据方面发挥了关键作用,提供了精干CoP的落实情况,从而证明了它的证据。我们用明确的Prolog堆来讨论我们直接实施这一系统之间的差别,在HOLLight中继续推广MESON,并比较其在所有核心HOLLight目标上的性能。由此产生的证明书也可以作为一般目的TPTP证明书。我们将其执行情况与基于TPTP和其他有趣的数据集的Metis决议进行比较。