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

ITR：人工智能推理、验证和理论：统一方法

• 批准号: 0219468
• 负责人: Paul Beame
• 金额: $ 49万
• 依托单位: University of Washington
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2002
• 资助国家: 美国
• 起止时间: 2002-09-01 至 2006-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0219468&HistoricalAwards=false
• 关键词: ITR; Inference; AI; Verification; Theory

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.

开发高效的自动逻辑推理系统的问题是朝着创建可验证、可靠和安全的硬件和软件系统的梦想迈出的关键一步。这项研究的目的是建立一个有充分基础的、统一的实用逻辑推理理论，它结合了人工智能、形式验证和理论计算机科学中发展起来的互补的思想和强大的命题推理方法。这个统一的理论将集中在(Ii)结合各种命题推理方法中使用的不同表示，以利用与每个方法相关的不同的算法技术；(Ii)使用组合表示来开发新的和改进的推理算法；(Iii)精确地表征各种启发式推理技术的能力，例如子句学习和随机搜索；以及(Iv)加深对问题结构如何表明特定推理策略的潜在有效性的深入理解。研究将涉及使用证明复杂性方法的理论工作，以及现实世界验证问题和人工智能规划问题的逻辑编码的实验工作。研究的最终目标是显著扩展适合进行形式分析的软件和硬件系统的规模和复杂性。