Using Specialists to Accelerate General Reasoning

Abstract

Theorem provers are prone to combinatorial explosions, especially when the reasoning chains needed to establish a desired result are lengthy. To alleviate this problem, special purpose inference methods have been developed that exploit properties of certain domains to shorten chains of reasoning with types, temporal relations, colors, numeric relations, and sets, to name a few. The problem investigated here is how to use these efficient, but limited methods in a more general environment. Although much research has been done on this problem, most of the resulting systems either restrict what they can represent and reason with, limit the types of special mechanisms that can be used, or are difficult to extend with other specialists. We develop a uniform interface to specialists which allows them to assist a resolution-based theorem prover in function evaluation, literal evaluation, and generalized resolving and factoring. The specialists incorporated into this system include a temporal reasoner, a type hierarchy, a number specialist, a set specialist, and a simple color specialist. Each new specialist was found to make possible fast proofs of questions previously beyond the scope of the theorem prover. Examples from the fully operational hybrid system are included.