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

开发高效的逻辑推理自动化系统是实现创建可验证、可靠和安全的硬件和软件系统梦想的关键一步。 本研究旨在发展一个有充分根据的、统一的实用逻辑推理理论，该理论结合了人工智能、形式验证和理论计算机科学中发展的互补思想和有力的命题推理方法。这个统一的理论将侧重于（ii）结合各种命题推理方法中使用的不同表示，如布尔决策图和合取范式，为了利用与每一个相关联的不同算法技术;（ii）使用组合表示开发新的和改进的推理算法;（iii）精确地表征各种启发式推理技术的能力，例如子句学习和随机搜索;和（四）发展对问题结构如何表明特定推理策略的潜在有效性的深刻理解。这项研究将涉及使用证明复杂性的方法的理论工作，以及对现实世界的验证问题和人工智能规划问题进行逻辑编码的实验工作。 研究的最终目标是显着扩大规模和复杂性的软件和硬件系统，服从形式化分析。

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.