swMATH ID: 
1822

Software Authors: 
Stärk, Robert F.

Description: 
The theoretical foundations of LPTP (a logic program theorem prover). This article contains the theoretical foundations of LPTP, a logic program theorem prover that has been implemented in Prolog by the author. LPTP is an interactive theorem prover in which one can prove correctness properties of pure Prolog programs that contain negation and builtin predicates like is/2 and call/\(n+ 1\). The largest example 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 firstorder theory that contains induction principles corresponding to the definition of the predicates in the program plus appropriate axioms for builtin predicates. The inductive extension allows to express modes and types of predicates. These can then be used to prove termination and correctness properties of programs. The main result of this article is that the inductive extension is an adequate axiomatization of the operational semantics of pure Prolog with builtin predicates. 
Homepage: 
https://www.sciencedirect.com/science/article/pii/S0743106697100139

Keywords: 
logic program;
pure Prolog

Related Software: 
AsmL;
ML;
XSB;
SATO;
HeerHugo;
Chaff;
NuSMV;
SICStus;
CiaoPP;
Ciao;
YAPProlog;
ASMKeY

Cited in: 
6 Documents
