From integrated reasoning specialists to “plug-and-play≓ reasoning components

Abstract

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.

We wish to thank Fausto Giunchiglia for very helpful discussions. We are also grateful to Alan Bundy and Alessandro Coglio for comments on an early draft of this paper. The authors are supported in part by Conferenza dei Rettori delle Università Italiane (CRUI) in collaboration with Deutscher Akademischer Austaunschdienst (DAAD) under the Vigoni Programme.