In this paper, the theory of McCarthy’s extensional arrays enriched with a maxdiff operation (this operation returns the biggest index where two given arrays differ) is proposed. It is known from the literature that a diff operation is required for the theory of arrays in order to enjoy the Craig interpolation property at the quantifier-free level. However, the diff operation introduced in the literature is merely instrumental to this purpose and has only a purely formal meaning (it is obtained from the Skolemization of the extensionality axiom). Our maxdiff operation significantly increases the level of expressivity; however, obtaining interpolation results for the resulting theory becomes a surprisingly hard task. We obtain such results via a thorough semantic analysis of the models of the theory and of their amalgamation properties. The results are modular with respect to the index theory and it is shown how to convert them into concrete interpolation algorithms via a hierarchical approach.

Interpolation and Amalgamation for Arrays with MaxDiff / S. Ghilardi, A. Gianola, D. Kapur (LECTURE NOTES IN ARTIFICIAL INTELLIGENCE). - In: Foundations of Software Science and Computation Structures / [a cura di] S. Kiefer, C. Tasson. - [s.l] : Springer, 2021. - ISBN 9783030719944. - pp. 268-288 (( convegno 24th International Conference, FOSSACS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021 tenutosi a Luxembourg City nel 2021.

Interpolation and Amalgamation for Arrays with MaxDiff

S. Ghilardi
;
2021

Abstract

In this paper, the theory of McCarthy’s extensional arrays enriched with a maxdiff operation (this operation returns the biggest index where two given arrays differ) is proposed. It is known from the literature that a diff operation is required for the theory of arrays in order to enjoy the Craig interpolation property at the quantifier-free level. However, the diff operation introduced in the literature is merely instrumental to this purpose and has only a purely formal meaning (it is obtained from the Skolemization of the extensionality axiom). Our maxdiff operation significantly increases the level of expressivity; however, obtaining interpolation results for the resulting theory becomes a surprisingly hard task. We obtain such results via a thorough semantic analysis of the models of the theory and of their amalgamation properties. The results are modular with respect to the index theory and it is shown how to convert them into concrete interpolation algorithms via a hierarchical approach.
Interpolation;Arrays; Amalgamation; SMT
Settore MAT/01 - Logica Matematica
Book Part (author)
File in questo prodotto:
File Dimensione Formato  
main.pdf

accesso riservato

Tipologia: Post-print, accepted manuscript ecc. (versione accettata dall'editore)
Dimensione 435.99 kB
Formato Adobe PDF
435.99 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
Ghilardi2021_Chapter_InterpolationAndAmalgamationFo.pdf

accesso riservato

Tipologia: Publisher's version/PDF
Dimensione 464.07 kB
Formato Adobe PDF
464.07 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
Pubblicazioni consigliate

Caricamento pubblicazioni consigliate

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/2434/830692
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 1
social impact