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

点击翻译按钮获取中文摘要

The problem of developing efficient automated systems of logicalinference is a key step toward the dream of creating verifiable,reliable, and secure hardware and software systems. This research isaimed at developing a well-founded, unified theory of practicallogical inference, that combines complementary ideas and powerfulapproaches for propositional inference developed in AI, formalverification, and theoretical computer science.This unified theory will focus on (ii) combining the differentrepresentations used in the various approaches to propositionalinference, such as Boolean decision diagrams and conjunctive normalform, in order to take advantage of the diverse algorithmic techniquesassociated with each; (ii) developing new and improved inferencealgorithms using the combined representation; (iii) preciselycharacterizing the power of various heuristic inference techniques,such as clause learning and randomized search; and (iv) developing arigorous understanding of how problem structure indicates thepotential effectiveness of particular inference strategies.The research will involve theoretical work using methods of proofcomplexity as well as experimental work on logical encodings of bothreal-world verification problems and AI planning problems. Theultimate goal research is to significantly expand the size andcomplexity of software and hardware systems that are amenable toformal analysis.