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.
From integrated reasoning specialists to “plug-And-Play” reasoning components / Armando, A.; Ranise, S.. - 1476:(1998), pp. 42-54. (Intervento presentato al convegno 4th International Conference on Artificial Intelligence and Symbolic Computation, AISC 1998 tenutosi a usa nel 1998) [10.1007/bfb0055901].
From integrated reasoning specialists to “plug-And-Play” reasoning components
Ranise S.
1998-01-01
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione