Amalgamating Knowledge Bases, II: Algorithms, Data Structures, and Query Processing

Integrating knowledge from multiple sources is an important aspect of automated reasoning systems. In the rst part of this series of papers, we presented a uniform declarative framework, based on annotated logics, for amalgamating multiple knowledge bases when these knowledge bases (possibly) contain inconsistencies, uncertainties, and non-monotonic modes of negation. We showed that annotated logics may be used, with some modications, tomediate between dierent knowledge bases. The multiple knowledge bases are amalgamated by embedding the individual knowledge bases into a lattice. In this paper, we brie y describe an SLD-resolution based proof procedure that is sound and complete w.r.t. our declarative semantics. We will then develop an OLDT-resolution based query processing procedure, MULTI OLDT, that satises two important properties: (1) ecient reuse of previous computations is achieved by maintaining a table { we describe the structure of this table and show that table operations can be eciently executed, and (2) approximate, interruptable query answering is achieved, i.e. it is possible to obtain an \intermediate, approximate " answer from the QPP by interrupting it at any point in time during its execution. The design of the MULTI OLDT procedure will include: (1) development of data structures for tabling (substitution, truth value) pairs, and (2) the development of algorithms to incrementally and eciently update the table.