CAREER: Scaling Up First-Order Logical Reasoning with Graphical Structure

提案0546663“职业：用图形结构扩展一阶逻辑推理”PI: Eyal amir伊利诺伊大学香槟分校自动推理世界的能力是人工智能（AI）的核心。近年来，应用程序必须考虑的对象和关系的数量急剧增加，当前的实际应用程序需要可以扩展到数千甚至数百万个对象和关系的推理机制。本研究的重点是使用现实世界中可用的基于图的结构将逻辑推理扩展到许多对象。关键思想是一种在一阶逻辑（FOL）中进行快速和正确推理的方法，该方法可以忽略对象、函数和谓词之间的大多数交互。该方法通过将输入FOL理论划分为子理论树，识别（看似重要的）可忽略的相互作用，并创建原始理论的紧凑命题编码来工作。它使用新的编码进行推理，或者直接使用树来指导FOL中的推理。该项目通过可能的应用，包括对象检测和对自然语言文本的复杂查询，具有广泛影响的潜力。该项目将通过让学生参与研究并将研究整合到本科和研究生课程中，从而将研究和教育活动结合起来。

Proposal 0546663"CAREER: Scaling Up First-Order Logical reasoning with Graphical Structure"PI: Eyal AmirUniversity of Illinois at Urbana-ChampaignThe ability to reason automatically about the world is central to Artificial Intelligence (AI). In recent years the number of objects and relations that applications must consider has increased dramatically, and current real-world applications require reasoning mechanisms that can scale to thousands and millions of objects and relations. This research focuses on scaling up logical inference to many objects using graph-based structures that are available in real-world domains. The key idea is a methodology for fast and correct inference in first-order logic (FOL) that can ignore most interactions between objects, functions, and predicates. The method works by partitioning the input FOL theory into a tree of sub-theories, identifying (seemingly essential) ignorable interactions, and creating a compact propositional encoding of the original theory. It reasons with that new encoding or uses the tree to guide reasoning in FOL directly.This project has the potential for wide Broader Impact through possible applications including object detection and complex queries on natural language texts. This project will integrate research and educational activities by involving students in the research and by integrating the research into both undergraduate and graduate classes.