ITR: Inference in AI, Verification, and Theory: A Unified Approach

University Of Washington, Seattle WA

Investigators

Abstract

The problem of developing efficient automated systems of logical inference is a key step toward the dream of creating verifiable, reliable, and secure hardware and software systems. This research is aimed at developing a well-founded, unified theory of practical logical inference, that combines complementary ideas and powerful approaches for propositional inference developed in AI, formal verification, and theoretical computer science. This unified theory will focus on (ii) combining the different representations used in the various approaches to propositional inference, such as Boolean decision diagrams and conjunctive normal form, in order to take advantage of the diverse algorithmic techniques associated with each; (ii) developing new and improved inference algorithms using the combined representation; (iii) precisely characterizing the power of various heuristic inference techniques, such as clause learning and randomized search; and (iv) developing a rigorous understanding of how problem structure indicates the potential effectiveness of particular inference strategies. The research will involve theoretical work using methods of proof complexity as well as experimental work on logical encodings of both real-world verification problems and AI planning problems. The ultimate goal research is to significantly expand the size and complexity of software and hardware systems that are amenable to formal analysis.