Automated Theorem Proving for Prolog Verification

TL;DR

This work adapts automated theorem proving to Prolog verification by translating Staerk's LPTP inductive theory $IND(P)$ into first-order formulas in the TPTP framework and applying off-the-shelf ATPs such as $E$ and Vampire. It encodes Prolog semantics through per-predicate viewpoints $(R^s,R^f,R^t)$, a groundness constraint $gr/1$, and induction schemas, enabling automatic proofs of termination and partial correctness. The authors detail a complete compilation pipeline from a Prolog program to a single $FOF$ theory, demonstrate it on roughly 400 properties from the LPTP library, and report rapid refutations on standard hardware, with the compiler and benchmark publicly available. This work demonstrates that automated provers can effectively automate key aspects of Prolog program verification, offering a scalable complement to interactive proof approaches.

Abstract

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.