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

University Of Illinois At Urbana-Champaign, Urbana IL

Investigators

Abstract

Proposal 0546663 "CAREER: Scaling Up First-Order Logical reasoning with Graphical Structure" PI: Eyal Amir University of Illinois at Urbana-Champaign The 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.