In program verification one has often to reason about lists over elements of a given nature. Thus, it becomes important to be able to combine the theory of lists with a generic theory T modeling the elements. This combination can be achieved using the Nelson-Oppen method only if T is stably infinite. The goal of this paper is to relax the stable-infiniteness requirement. More specifically, we provide a new method that is able to combine the theory of lists with any theory T of the elements, regardless of whether T is stably infinite or not. The crux of our combination method is to guess an arrangement over a set of variables that is larger than the one considered by Nelson and Oppen. Furthermore, our results entail that it is also possible to combine T with the more general theory of lists with a length function. © Springer-Verlag Berlin Heidelberg 2005.

Combining lists with non-stably infinite theories / Fontaine, P.; Ranise, S.; Zarba, C. G.. - 3452:(2005), pp. 51-66. (Intervento presentato al convegno 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2004 tenutosi a Montevideo, ury nel 2005) [10.1007/978-3-540-32275-7_4].

### Combining lists with non-stably infinite theories

#### Abstract

In program verification one has often to reason about lists over elements of a given nature. Thus, it becomes important to be able to combine the theory of lists with a generic theory T modeling the elements. This combination can be achieved using the Nelson-Oppen method only if T is stably infinite. The goal of this paper is to relax the stable-infiniteness requirement. More specifically, we provide a new method that is able to combine the theory of lists with any theory T of the elements, regardless of whether T is stably infinite or not. The crux of our combination method is to guess an arrangement over a set of variables that is larger than the one considered by Nelson and Oppen. Furthermore, our results entail that it is also possible to combine T with the more general theory of lists with a length function. © Springer-Verlag Berlin Heidelberg 2005.
##### Scheda breve Scheda completa Scheda completa (DC)
2005
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Germany
Springer Verlag
978-3-540-25236-8
978-3-540-32275-7
Fontaine, P.; Ranise, S.; Zarba, C. G.
Combining lists with non-stably infinite theories / Fontaine, P.; Ranise, S.; Zarba, C. G.. - 3452:(2005), pp. 51-66. (Intervento presentato al convegno 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2004 tenutosi a Montevideo, ury nel 2005) [10.1007/978-3-540-32275-7_4].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: `https://hdl.handle.net/11572/333176`
##### Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

• ND
• 8
• ND