Within software’s life cycle, program testing is very important, since quality of specification demand, design and application must be proven. All definitions related to program testing are based on the same tendency and that is to give answer to the question: does the program behave in the requested way? One of oldest and best-known methods used in constructive testing of smaller programs is the symbolic program execution. One of ways to prove whether given program is written correctly is to execute it symbolically. Ramified program may be translated into declarative shape, i.e. into a clause sequence, and this translation may be automated. Method comprises of transformation part and resolution part.This work gives the description of the general frame for the investigation of the problem regarding program correctness, using the method of resolution invalidation.. It is shown how the rules of program logic can be used in the automatic resolution procedure. The examples of the realization on the LP prolog language are given (without limitation to Horn's clauses and without final failure).. The process of Pascal program execution in the LP system demonstrator is shown.