AF: Small: Dynamic Reasoning

University Of Massachusetts Amherst, Amherst MA

Investigators

Abstract

Descriptive Complexity measures the richness of a language needed to describe a given property. The languages are variants of first-order logic describing finite structures. All major complexity classes have been shown to have natural descriptive characterizations, providing a deep and profound relationship between the traditional computational complexity of a problem and the descriptive complexity of the problem. Thus complexity can be understood entirely from a logical point of view. Important new understandings about complexity have arisen from the descriptive point of view. In particular, the trade-off between parallel time and amount of hardware, a fundamental issue in computation, has been characterized as the trade-off between formula size and number of variables. There are four broader impacts from the above work. (1) This project will extend knowledge concerning the complexity of problems as well as providing new methods to automatically check the correctness of programs. This work will lead to tools useful for teaching logic and complexity. (2) The project will improve the understanding of the fundamental nature of computation. (3) Results from this project will be widely distributed and will be presented at conferences, published in journals, and taught in seminars. (4) The PI will also train graduate students to do research in this combination of pure and applied theory. In this project, the PI will continue to extend the understanding of computational complexity using descriptive complexity. The PI will also expand the recent use of modern SAT solvers to automatically prove that programs meet their correctness conditions or find runs on which they do not. The intellectual merit of this project is that it will extend the understanding of computational complexity and it will improve the ability and understanding of how to automatically reason about the correctness of programs. The research in this project has several specific thrusts: (1) The PI will extend the methodology for automatically generating correctness conditions for programs in simple languages which are automatically checkable, (2) The PI will extend the current understanding of dynamic complexity, especially for reachability properties, (3) The PI will develop a theory of dynamic reasoning, identifying when it is possible to reason about program states in an essentially propositional way and when it is not, (4) The PI will study the dichotomy phenomon from a descriptive point of view. In particular, starting with binary Constraint Satisfaction Problems, the PI will explain where dichotomies lie and in particular why natural computational problems tend to be complete for a small number of important complexity classes.