Automated theorem proving in the ProTem programming language

The ProTem programming language has been designed around a formal mathematical basis to allow a programmer to define exactly what a computer program means. A ProTem program is expressed in the language of first order logic, and uses several theories, such as bunch theory, number theory, list theory and others.;This thesis addresses the problem of proving refinements correct in the ProTem programming language. One envisions a ProTem programming environment where each step of the programming process (from specification to program) is checked by an automated theorem prover, to determine that each refinement is correct.;The desired action of a computer program is expressed in a first order logic sentence called the specification. A specification will not usually be in the notation of a computer language (i.e. one cannot compile a specification in most cases) so the specification must be transformed into a programming language. Specification refinement allows a programmer to move from the specification to programming notation in steps. As long as each refinement step is a theorem in first order logic, then the refinement is correct. When the refinement is complete, and each refinement is correct, then the resulting computer program has been determined correct with respect to the specification.