RI: Small: Universal Automated Reasoning by Knowledge Compilation

推动这个项目的一个长期目标是开发一个通用计算引擎，以支持智能系统的不同应用程序(例如，规划和诊断)的推理。该项目建立在一种方法的基础上，该方法将知识库编译成易于处理的形式的分类，这是对否定范式(NNF)施加各种条件(如可分解性和确定性)的结果。通常难以处理的某些查询在编译后的NNF表单上变得容易处理。要实现像规划或诊断这样的任务，所有人需要做的就是将他们的知识库编译成NNF的最简洁的子集，该子集为任务所需的查询提供多时间支持。该项目将特别侧重于使用自上而下和自下而上的编译技术对NNF编译施加各种条件的算法，以支持更大的一组易于处理的形式。这将导致开发和评估比传统的SAT解算器更强大的推理机，并得到一套更全面的知识库查询和转换的支持。它还将导致将编译方法扩展到更大类别的人工智能应用程序。

A long term goal motivating this project is the development of a universal computational engine to support reasoning across different applications of intelligent systems (e.g., planning and diagnosis). The project is founded on an approach that compiles knowledge bases into a taxonomy of tractable forms, which result from imposing various conditions, such as decomposability and determinism, on Negation Normal Form (NNF). Certain queries, which are generally intractable, become tractable on the compiled NNF forms. To implement a task like planning or diagnosis, all one needs to do is compile their knowledge base to the most succinct subset of NNF that provides polytime support for the queries required by the task. The project will focus in particular on algorithms for imposing various conditions on NNF compilations, using both top-down and bottom-up compilation techniques, to support a larger set of tractable forms. This will lead to developing and evaluating a more powerful inference engine than traditional SAT solvers, supported by a more comprehensive set of queries and transformations on knowledge bases. It will also lead to extending the compilation approach to a larger class of AI applications.