Scaling Up First-Order Logical Reasoning using Graphical Structure

Principal Investigator

  • Eyal Amir, University of Illinois at Urbana-Champaign

    Students

  • Deepak Ramachandran, University of Illinois at Urbana-Champaign
  • Igor Gammer, University of Illinois at Urbana-Champaign

    This work is supported by award NSF IIS 05-46663 (CAREER Award) titled CAREER: Scaling Up First-Order Logical Reasoning with Graphical Structure.

    Research Objectives

    The ability to represent and reason about objects and relations between them is central to many approaches and applications in Artificial Intelligence (AI), including common-sense query answering, natural-language processing, planning, and diagnosis problem solving. In recent years the number of objects and relations that applications need to consider has increased dramatically, and current real-world applications require reasoning mechanisms that can scale to thousands and more objects and relations. Traditional approaches to logical reasoning that focus on propositional theories are impractical for such real-world domain because propositional representations of the associated theories have explosive sizes, rendering inference useless. On the other hand, current inference in First-Order Logic (FOL) is impractical here as well because it focuses on mathematical theories that are much smaller and lack the structure of real-world common-sense domain theories.

    This project focuses on scaling up inference over FOL with graph-based structures that are available in real-world domains. In this research we focus first on inference in FOL, and then apply the insights we gain from general FOL to inference with first-order structure on more specialized scenarios (most times avoiding general FOL inference while still using the same structure). The key idea in this approach is a methodology for inference in FOL that can ignore most interactions between objects, functions, and predicates, and be fast and correct. In this methodology, a given theory is first partitioned into a tree of subtheories, according to different measures of efficiency that depend on the target inference algorithm.

    Our research starts with creating a theory of such structures in FOL knowledge bases, anticipating future use of the graph structures by inference algorithms. We then consider two paradigms for inference: one in which we use the structure to create compact propositional encodings of the original theory, and one in which inference is carried out directly in FOL guided by the graph structure. In a complementary effort, we plan to develop algorithms that partition a given theory automatically according to different optimization criteria that match the target inference algorithm.

    See also the Partitioning and Reasoning project web page.

    PAPERS

    D. Ramachandran and E. Amir, Compact Propositional Encodings of First-Order Theories, in 20th National Conference on Artificial Intelligence (AAAI'05), 2005 (PS,PDF). [new]
    Eyal Amir Last updated on January 23, 2005.