Here is a set of worksheets with solutions to
gradually learn LPTP, the Logic Program Theorem Prover.
It assumes that the reader has a working installation of LPTP
and has read chapter 1 of user.pdf.
An overview of LPTP is described in Interactive-Proofs-for-Logic-Programs.pdf,
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
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.