一种关于高效命题推理极限的新方法：基础，算法和近似

项目名称： 一种关于高效命题推理极限的新方法：基础，算法和近似

项目编号： No.61373002

项目类型： 面上项目

立项/批准年度： 2013

项目学科： 自动化技术、计算机技术

项目作者： Iddo Tzameret

作者单位： 清华大学

项目金额： 66万元

中文摘要： 命题推理，更确切地说，阐明命题公式的不可满足性，是计算机科学、软硬件验证、自动推理以及人工智能领域最重要的问题之一。实际上，充分理解命题推理的复杂性对于计算机科学的各个相关领域都是十分重要的。 本项目旨在增进我们对高效推理极限的理解，并试图挖掘其与高效计算间的新关系。我们希望通过引入命题证明、近似理论、反驳算法、代数复杂性及纯代数的新关联，去建立估算不同推理框架效率的新方法，并加深我们对高效计算和高效证明之间关联的理解。我们特别关注如何在各种证明系统(即推理框架)下,给出命题推理长度下界的证明。 我们计划采用的下列方法： ? 代数方法; ? 基于不可近似性结论; ? 基于随机实例的反驳算法; ? 近似推理的方法。 本项目是一项基础性研究，组员由计算机基础科学、计算复杂性、逻辑学、组合学和人工智能领域的资深专家组成。

中文关键词： 计算理论；计算机复杂性；计算机科学逻辑；可满足性；

英文摘要： Propositional reasoning, and specifically the task of demonstrating unsatisfiability of propositional formulas is among the most important problems in computer science as well as in hardware and software validation, automated reasoning and artificial inte

英文关键词： Theory of Computation；Computational Complexity；Logic in Computer Science；Satisfiability；