Configuration is a complex task generally involving
varying measures of constraint satisfaction, optimization,
and the management of soft constraints. Although many successful
systems have been developed, these are often difficult
to maintain and to generalize in rapidly changing domains.
In this paper, we consider building intelligent knowledge-based
systems with maintainability well to the fore in our requirements
for such systems. We introduce two case studies: the initial
proof of concept, which was in the domain of computer configuration,
and a further field-tested study, the configuration of
compressors. Central to our approach is the use of the
proof planning technique, and the clean separation of different
kinds of knowledge: factual, heuristic, and strategic.
The Use of Proof Planning for Co-operative Theorem Proving
