摘要：We investigate the application of automated deduction techniques to retrieve software components based on their formal specifications. The application profile has major impacts on the problem solving process and requires an open system architecture in which different deductive engines work in combination because the proof problems are too difficult for a single monolithic system. We describe our system architecture, a pipeline of filters of increasing deductive strength, and concentrate on the final filter, in which theorem provers are applied. Here, we use the Ilf-system as a control and integration shell to combine different provers. We support two different combination styles, competition and cooperation. Experiments confirm our approach. With moderate timeouts we already achieve an overall recall of approximately 80%.
