I don't have much to add other than that the Warren Abstract Machine seems to be particularly popular as an abstract model for implementing Prolog. If you haven't looked into it yet, this may be a good start for you.

http://wambook.sourceforge.net/wambook.pdf