LPTP (Logic Program Theorem Prover) is an interactive natural-deduction-based theorem prover for pure Prolog programs with negation as failure, unification with the occurs check, and a restricted but extensible set of built-in predicates. With LPTP, one can formally prove termination and partial correctness of such Prolog programs. LPTP was designed in the mid-1990's by Robert F. Staerk. It is written in ISO-Prolog and comes with an Emacs user-interface. From a theoretical point of view, in his publications about LPTP, Staerk associates a set of first-order axioms IND(P) to the considered Prolog program P. IND(P) contains the Clark's equality theory for P, definitions of success, failure and termination for each user-defined logic procedure in P, axioms relating these three points of view, and an axiom schema for proving inductive properties. LPTP is thus a dedicated proof editor where these axioms are hard-wired. We propose to translate these axioms as first-order formulas (FOFs), and apply automated theorem provers to check the property of interest. Using FOF as an intermediary language, we experiment the use of automated theorem provers for Prolog program verification. We evaluate the approach over a benchmark of about 400 properties of Prolog programs from the library available with LPTP. Both the compiler which generates a set of FOF files from a given input Prolog program together with its properties and the benchmark are publicly available.

翻译：LPTP（逻辑程序定理证明器）是一种基于自然演绎的交互式定理证明器，适用于具有失败即否定、带出现检查的统一化以及一组受限但可扩展的内置谓词的纯Prolog程序。利用LPTP，可以对此类Prolog程序的终止性和部分正确性进行形式化证明。LPTP由Robert F. Staerk于1990年代中期设计，采用ISO-Prolog编写并配备Emacs用户界面。从理论视角看，Staerk在其关于LPTP的文献中为所考察的Prolog程序P关联了一组一阶公理IND(P)。IND(P)包含：P的Clark等式理论、P中每个用户定义逻辑过程关于成功/失败/终止性的定义、关联这三个视角的公理，以及用于证明归纳性质的公理模式。因此LPTP是一个将这些公理硬编码的专用证明编辑器。我们提出将这些公理转换为一阶公式，并应用自动定理证明器来验证目标性质。以一阶公式作为中间语言，我们尝试将自动定理证明器应用于Prolog程序验证。我们在LPTP附带的程序库中选取约400个Prolog程序性质构成基准测试集进行评估。用于从给定Prolog程序及其性质生成一阶公式文件集的编译器及基准测试集均已公开。