Properties of Programs and the First-Order Predicate Calculus

Abstract

This paper is concerned with the relationship of the termination problem for programs and abstract programs to the validity of certain formulas in the first-order predicate calculus. By exploiting this relationship, subclasses of abstract programs for which the termination problem is decidable can be isolated. Moreover, known proof procedures for the first-order predicate calculus (e.g. resolution) can be applied to prove the termination of both programs and abstract programs. The correctness and equivalence problems of abstract programs are shown to be reducible to the termination problem.