An overview of LPTP (Logic Program Theorem Prover) is described in Interactive-Proofs-for-Logic-Programs.pdf. The LaTeX source files are present in this repository.
The LPTP proof format is an extension of first order natural deduction. If needed, natural deduction is explained for instance in the following book:
Logic in computer science - modelling and reasoning about systems
Huth & Ryan – Cambridge University Press - 2000
This repository also contains a set of worksheets with solutions to gradually learn LPTP. It assumes that the reader has a working installation of LPTP and has read chapter 1 of user.pdf.
The *.tex are TeX files (not LaTeX files). They can be compiled into PDF files with the usual tools. Check that the first line of these files is \input ../tex/proofmacros.tex. The file tex/proofmacros.tex is included in the repository. LPTP rewrites that line to the absolute path of its own installation every time it regenerates a .tex, which might work.