I am looking for an electronic resource (book, article, site) on Prolog that clearly lays out the logical / mathematical foundations, explicating exactly what is meant by unification, the matching algorithm, the back-tracing algorithm, SLDNF resolution, cut, ... all in a clear and consistent package. It is fine (even preferred) that this resource presumes familiarity with first order logic. It doesn't need to go into applications as I have acquired another book on this.
The book I'm reading makes the unfortunate decision to leave out the math and instead define these terms and processes only vaguely, which leaves many other details defined only vaguely as well.
I found this that would correspond to what you are looking for http://pages.di.unipi.it/borger/Papers/LogicPgg/prolog.pdf
(A mathematical definition of full Prolog, by Börger and Rosenzweig)