We develop the foundations of Horn clause logic programming in a proof-theoretic style. We present a formal unification system for first order terms including a syntactic representation of environments and formalisms for the bottom-up and top down computation of answers in a unified formal setting. In passing, we propose an abstrac unification machine. We also discuss the possibility and implications of representing logic program evaluation strategies in the lambda calculus.