Technical Abstract for Algernon and Access-Limited Logic

We have developed Access-Limited Logic (ALL) into a useful language for representing knowledge in very large knowledge-bases. Our goal in this work is to combine the formal rigor of first-order logic with the efficiency and intuitive appeal of a network-structured knowledge-base. Our research methodology involves a synergistic balance between theoretical work and system implementation. On the formal side, we have completed a rigorous proof of soundness and Socratic Completeness for ALL which includes negation, assumptions, and proof by contradiction. We have also demonstrated the existence of a family of increasingly powerful inference methods, parameterized by the depth of assumption nesting, ranging from incomplete and tractable to complete and intractable. On the practical side, Algernon, the implementation of ALL, continues to be used by students in our graduate course on expert systems. Further, Algernon serves as the basis for QPC, a sophisticated AI program for building qualitative differential equation models of physical systems. Algernon is also in use by researchers both here at the University of Texas and at MCC. Finally, the natural language group at MCC has recently distributed to their shareholders a natural language system built using Algernon.

It has long been a guiding principle of the semantic network approach to knowledge representation that by exploiting the network structure of knowledge, one can increase the efficiency of reasoning. Intuitively, in a semantic network related concepts are located ``close together'' in the network and thus search and inference can be guided by the structure of the knowledge-base. However, formalisms for semantic networks have generally treated the semantic network notation as a variant of predicate calculus, and have regarded the access limitations inherent in a network to be an extra-logical indexing mechanisms.

Reasoning is hard. If a knowledge representation language is as expressive as first-order predicate calculus, then the problem of deciding what an agent implicitly knows (i.e. what an agent could logically deduce from its knowledge) is unsolvable [Boolos & Jeffrey, 1980]. Thus a sound and decidable knowledge representation and reasoning system must either give up expressive power, or use a weak inference system with an incomplete set of deduction rules or artificial resource limits (e.g. bounds on the number of applications of modus ponens). However, such inference systems tend to be difficult to describe semantically and tend to place unnatural limits on an agent's reasoning ability [Levesque, 1986].

Our solution to this dilemma is two fold. First, we have identified a set of inference mechanisms which can be efficiently computed in a network structured knowledge-base. The inference mechanisms in ALL are based on the idea of an access path and are guaranteed never to require searches of the entire knowledge-base. The time complexity of computing inference in ALL thus depends (polynomially) on the size of the accessible portion of the knowledge-base. Inference in ALL is thus necessarily incomplete. The second part of our approach is the development of formal results which characterize the (in)completeness of ALL. We have shown that ALL is Socratically Complete --- for any query of a proposition which is a consequence (in predicate calculus) of the knowledge-base, there exists a series of preliminary queries after which the original query will succeed. We have also shown several technical properties which partially characterize the conditions under which a query will succeed immediately.

Though ALL is Socratically Complete, complete inference in first order logic without existential quantification is known to be NP complete, so the problem of generating the series of preliminary Socratic queries must be NP complete. However, we have shown that the key factor determining the difficulty of finding such a series is the depth of assumption nesting in the series. Given any knowledge-base and any fact, if there exists a series of preliminary queries and assumptions after which a query of the fact will succeed, and the series only nests assumptions to depth n, then the series can be found in time proportional to the size of the accessible portion of the knowledge-base raised to the power n. This result is particularly significant since we expect common-sense reasoning to require large knowledge-bases, but relatively shallow assumption nesting. In future work, we plan to use context mechanisms to restrict the size of the reachable portion of the knowledge base.

An important part of our work has been the synergistic combination of theoretical work on ALL and implementation work on Algernon. Algernon has been implemented in CommonLisp (and recently in C++) and is a substantial knowledge-representation system. A large number of small and medium-sized Algernon knowledge-bases are presented in [Crawford, 1990]. It is also the implementation language for the substantial qualitative-model building system QPC [Crawford, et al, 1990], Since 1990, Algernon has been used for projects in the graduate Expert Systems class at the University of Texas at Austin. It has also been used in a central or substantial supporting role in research toward two master's theses and four doctoral dissertations at the University of Texas at Austin.

In addition, Algernon is being distributed to other industrial and university sites. When MCC was developing a general-purpose natural language front-end for knowledge bases, they assigned several teams to implement their system on top of different knowledge representation languages. The team using Algernon consisted of a single UT Linguistics graduate student. Because of her skill and experience, and because of Algernon's simplicity and clarity, she was the first to complete the task. MCC licensed Algernon from UT for distribution to its shareholders, and a number of shareholder firms have subsequently licensed Algernon. The system has also been distributed to several other sites including Stanford University, where it is contributing to our collaboration with a research group focusing on large-scale knowledge-based systems for reasoning about physical devices.