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.

开发有效的自动化系统的问题是朝着梦想创建可验证，可靠和安全的硬件和软件系统的关键步骤。这项研究在开发一种有充分的实践性推理的良好，统一的统一理论方面结合了互补的思想和有力的攻击，用于在AI，正式化和理论计算机科学中开发的命题推理，这些统一理论将重点介绍（ii）在（II）将各种阶级的不同方法与诸如临时性临床的不同方法相结合，例如临床，例如，临床构成了疾病，例如，临床构成了临时性的疾病。算法技术与每种技术相关；（ii）使用组合表示形式开发新的和改进的推论；（iii）精确地阐明各种启发式推理技术的力量，例如子句学习和随机搜索；（iv）对问题结构如何表明特定推理策略的电位有效性发展，这项研究将涉及使用证明复杂性方法以及对Bothreal-World-World验证问题和AI计划问题的逻辑编码的实验性工作的理论工作。《城市目标研究》是显着扩大适合易毛分析的软件和硬件系统的大小和复杂性。