EFFICIENT ACCESS TO KNOWLEDGE VIA FORWARD CHAINING TACTICS

Abstract

The goal of this work is to explore efficient ways to use knowledge in interactive development of formal arguments. The challenge in automatically applying knowledge from a large knowledge base is in defining useful and tractable approximations to the deductive closure of the knowledge base. For an approximation to be useful, it must be deep in some directions. For it to be tractable, it must not be deep in all directions. Further, it must be easy to control this directedness. Thus, we need to make selective inferences from a large knowledge base that are sensitive both to its internal structure and to the query under consideration. To do this, most interactive systems employ a combination of heuristics and explicit user commands. The interaction of these two is intricate: to efficiently give hints to a heuristic prover requires developing a model of reasoning that is both efficiently implementable and easy to understand and use, i.e., fast, having a concise command language and predictable results. Rule-based specifications of approximations is the starting point for the contribution of this thesis in solving the problem described above. In this thesis, we analyze the use of rule-based forward chaining inference procedures and develop several extensions to the basic approach. We propose a new language for forward chaining tactics that can be used to specify goal-directed inference from large knowledge bases. This provides a modular approach to programming the heuristics for theorem proving. The tactic language has clean theoretical properties that make it appropriate for automated analysis and optimization. From the software engineering perspective, this thesis contains an assessment of the new software engineering approach of the theorem prover Ontic: specifying high performance theorem provers in a bottom-up logic programming framework. This perspective provides a much needed link between the Ontic project and other established research paradigms. The analysis tools developed for evaluating the forward chaining approach to obvious reasoning should have broad applications in evaluating other semi-automated approaches and systems. We also develop a language for declarative specification of control for forward chaining reasoning that is analogous to the role of LCF tacticals for specifying control in refinement-style reasoning, as embodied in Nuprl. We arrived at promising conclusions about the potential for combining these two styles of tactic programming in such problems as the integration of decision procedures and rewriting into interactive theorem provers.