Automated design of specialized representations

摘要

We present a general notion of specialized representation and a methodology that automates the design of such representations. These representations are combinations of data structure and procedure that efficiently perform inferences required in solving a problem. Our implementation of the methodology begins with a problem stated in a sorted first-order logic and designs a representation for the problem by combining building blocks, called representation schemes. It has a library of representation schemes. A scheme is identified for use in designing a representation by matching a description of the inferences it performs against one or more statements in a problem. Once a scheme is designed into a representation, the general problem solver need no longer consider the problem statements matched in the scheme identification process because the scheme computes the required inferences from those statements. The machinery to perform the required inferences has been moved out of the problem solving cycle and into the representation. Experience with the implementation has shown that a theorem prover reasoning about a smaller set of statements in a specialized representation is dramatically more efficient than reasoning about the original set of statements in the original representation.