THE THEORETICAL FOUNDATIONS OF LPTP (A LOGIC PROGRAM THEOREM PROVER)

This article contains the theoretical foundations of LPTP, a logic pro gram theorem prover that has been implemented in Prolog by the author. LPTP is an interactive theorem prover in which one can prove correctn ess properties of pure Prolog programs that contain negation and built -in predicates like is/2 and call/n + 1. The largest example program t hat has been verified using LPTP is 635 lines long including its speci fication. The full formal correctness proof is 13128 lines long (133 p ages). The formal theory underlying LPTP is the inductive extension of pure Prolog programs. This is a first-order theory that contains indu ction principles corresponding to the definition of the predicates in the program plus appropriate axioms for built-in predicates. The induc tive extension allows to express modes and types of predicates. These can then be used to prove termination and correctness properties of pr ograms. The main result of this article is that the inductive extensio n is an adequate axiomatization of the operational semantics of pure P rolog with built-in predicates. (C) 1998 Elsevier Science Inc. All rig hts reserved.