Here is a set of worksheets with solutions to gradually learn LPTP, the Logic Program Theorem Prover.

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. 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