Modular Construction of Very Large Knowledge Bases

摘要

In this report, we describe work done at Kestrel under the DARPA High Performance Knowledge Bases program. The goal of the program is to develop methods for structuring large knowledge-bases and reasoning efficiently in them. The report contains four sections. In the first, we describe our work on the crisis management challenge problems. In the second, we describe our Designware system for semi-automated program synthesis. In the third, we present a detailed description of parametrized specifications, an important tool for combining theory refinements. In the fourth, we describe limits, interpretation, and slicing, all important tools for constructing, deconstructing, and relating theories.