From integrated reasoning specialists to “plug-And-Play” reasoning components

There is an increasing evidence that a new generation of reasoning systems will be obtained via the integration of different reasoning paradigms. In the verification arena, several proposals have been advanced on the integration of theorem proving with model checking. At the same time, the advantages of integrating symbolic computation with deductive capabilities has been recognized and several proposals to this end have been put forward. We propose a methodology for turning reasoning specialists integrated in state-of-the-art reasoning systems into reusable and implementation independent reasoning components to be used in a "plug-and-play" fashion. To test our ideas we have used the Boyer and Moore's linear arithmetic procedure as a case study. We report experimental results which confirm the viability of the approach.