An operational semantics of the Prolog programming language is introduced. Meta-IV is used to specify the semantics. One purpose of the work is to provide a specification of an implementation of a Prolog interpreter. Another one is an application of this specification to a formal description of program optimization techniques based on the principle of partial evaluation.Transformations which account for pruning, forward data structure propagation and opening (which also provides backward data structure propagation) are formally introduced and proved to preserve meaning of programs. The so defined transformations provide means to inference data structures in an applicative language. The theoretical investigation is then shortly related to research in rule-based systems and logic.An efficient well-integrated partial evaluation system is available in Qlog --- a Lisp programming environment for Prolog.