Reference: Amir, E. & McIlraith, S. A. Partition-Based Logical Reasoning. Knowledge Systems Laboratory, February, 2000.
Abstract: We investigate the problem of reasoning with partitions of related logical axioms. We are motivated by the problem of how to reason effectively with multiple knowledge bases that have overlap in content. In this paper, we address the more general problem of how to exploit structure inherent in a set of logical axioms to improve the efficiency of reasoning. To this end, we provide algorithms for reasoning with partitions of axioms in propositional and first-order logic. Craig's interpolation theorem serves as a key to proving completeness of these algorithms. We analyze the computational benefit of our algorithms and identify those parameters of a partitioning that influence the efficiency of computation. These parameters are the number of symbols shared by a pair of partitions, the size of each partition, and the topology of the overall partitioning. Finally, we provide a greedy algorithm that automatically decomposes a given theory into partitions, trying to optimize the efficiency of reasoning by controlling these parameters.
Notes: This paper (without the proofs) also appears in the Proceedings of the Seventh International Conference on Principles of Knowledge Representation and Reasoning (KR2000), Breckenridge, USA. April, 2000.
Full paper available as ps.