LPTP 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 built-in 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 first-order theory that contains induction principles corresponding to the definition of the predicates in the program plus appropriate axioms for built-in 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 built-in predicates. Homepage: https://www.sciencedirect.com/science/article/pii/S0743106697100139 Keywords: logic program; pure Prolog Related Software: AsmL; ML; XSB; HeerHugo; Chaff; SATO; NuSMV; SICStus; CiaoPP; Ciao; YAP-Prolog; ASMKeY Cited in: 6 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year The theoretical foundations of LPTP (a logic program theorem prover). Zbl 0911.68030Stärk, Robert F. 1998 all top 5 Cited by 7 Authors 2 Fruja, Nicu G. 2 Stärk, Robert F. 1 Bagnara, Roberto 1 Drabent, Włodzimierz 1 Gori, Roberta 1 Hill, Patricia M. 1 Zaffanella, Enea all top 5 Cited in 6 Serials 1 Theoretical Computer Science 1 Science of Computer Programming 1 The Journal of Logic Programming 1 Information and Computation 1 Computer Languages, Systems & Structures 1 ACM Transactions on Computational Logic Cited in 1 Field 6 Computer science (68-XX) Citations by Year