This dissertation is based on a PASCAL hyperresolution program, written by the author. Features of the program are described; the 'most general unifier' (mgu) is defined algorithmically; a semi-formal denotational semantics for PASCAL is introduced, leading to a correctness proof for the implementation of te mgu; and the dissertation ends with an exposition of Tseitin's lower bound for ground resolution (118 pages).