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

职业：用图形结构扩展一阶逻辑推理

• 批准号: 0546663
• 负责人: Eyal Amir
• 金额: --
• 依托单位: University of Illinois at Urbana-Champaign
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2005
• 资助国家: 美国
• 起止时间: 2005-12-15 至 2010-11-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0546663&HistoricalAwards=false
• 关键词: CAREER; Scaling; Up; First; Order

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.

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