Anzeige
Erschienen in:
2005 | OriginalPaper | Buchkapitel
Combining Lists with Non-stably Infinite Theories
verfasst von : Pascal Fontaine, Silvio Ranise, Calogero G. Zarba
Erschienen in: Logic for Programming, Artificial Intelligence, and Reasoning
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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 ifT
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.