The study of algorithms involves two important aspects, correctness and complexity. This project addresses these two aspects from a machine independent viewpoint by using formulas of mathematical logic. Logic formulas can provide descriptions of solutions to problems which can then be analyzed for their correctness and complexity. Of particular interest is to develop a feasible set of logical formulas for P, the class of problems which are tractable, i.e., whose solutions require only a polynomial number of machine steps, and in addition, to provide a system for reasoning about the properties of these logical formulas. Finding a comprehensive description of such a set of formulas would exhibit a machine independent definition of P and have a significant impact on our understanding of the algorithms for this important complexity class. If successful, this system could provide a method by which one could demonstrate that a given formula is the correct solution to certain problem. As an alternative to program correctness, this may provide a deeper understanding of algorithmic correctness.
