Elisa: A New System for AI-Assisted Logico-Mathematical Scientific Discovery Incorporating Novel Techniques in Infinite Model Finding.

Contemporary artificial intelligence (AI) started in 1956, on the strength of a passionate resurgence in the desire to understand the principles of human reasoning, not only in order to provide a secure, rigorous foundation on which scientific theories stand, but to mechanize such reasoning---to build computational agents capable of human-level reasoning, including, ideally, those that can produce their own discoveries, and verify them according to scientific principles. The first such agents included Logic Theorist, Program I, and Program II. In parallel efforts, continuing a debate much older than AI itself, many contended (and some still do) that no such mechanization is achievable: that human reasoning and discovery are capabilities that fall outside of what is computational. That sophisticated (and even naive) computational agents have much to offer in scientific endeavors, however, is incontestable, and as progress is made in understanding the nature of human reasoning, more sophisticated agents can be built to assist in the practice of scientific discovery. In this dissertation, we present such a system: ELISA, an intelligent assistant for scientific discovery. The system, a suite of advanced reasoning tools integrated in a highly visual workspace, provides an interactive environment for a human reasoner to explore, hypothesize, and reason over scientific and mathematical domains. In this first realization of the ELISA architecture, particular attention is paid to complete or partial mechanization of particular aspects of the process of scientific discovery, specifically concept and conjecture generation, argumentation, and verification. As a full-blown and general implementation of the ambitious architecture described herein would require an order of magnitude more effort than would fit in one dissertation, the introduced implementation is restricted to logico-mathematical scientific domains---domains which can be represented in a formal logical system. This restriction allows for existing powerful automated reasoning systems to be leveraged and incorporated into the ELISA system. After setting the historical context, the presentation of ELISA begins with the architecture, inspired by a high-level theory of the process of scientific discovery. Next, the first implementation of the ELISA architecture, called ELISA1 and realized as an interactive visual workspace for discovery, is described. Finally, we zero in on a particular functionality of the ELISA 1 system, where a new technique in automated model finding is introduced. This technique hurdles a certain deficiency of existing model-finding technologies: that such systems are capable only of producing finite models. Our approach springboards from such existing work and expands the range of models that can be found to include some well-behaved, infinite domains.