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.