Formal verification of logic programs: Foundations and implementation

Abstract

We present the theoretical foundations of LPTP, a logic program theorem prover implemented in Prolog by the author. LPTP is an interactive theorem prover in which one can prove termination and correctness properties of pure Prolog programs that contain negation and built-in predicates like is/2 and call/n. The largest program that has been verified using LPTP is 635 lines long including its specification. The full formal correctness proof is 13128 lines long (133 pages). The formal theory underlying LPTP is the inductive extension of pure Prolog programs. This is a first-order theory that contains induction principles corresponding to the definition of the predicates in the program plus appropriate axioms for built-in predicates.