conference paper
Polite Combination in Parametric Array Theories
Thiemann, René
•
Weidenbach, Christoph
September 15, 2025
Frontiers of Combining Systems - 15th International Symposium, FroCoS 2025, Proceedings
Parametric array theories are extensions of the quantifier-free theory of arrays with relations that hold componentwise. We observe that decision procedures for the satisfiability of these theories rely on a kind of finite witnessability property. We use this insight to show the politeness of these theories with respect to the index and element sorts. Our results clarify the politeness of the theory of sets with the cardinality operator, which was left open in the literature.
Loading...
Name
10.1007_978-3-032-04167-8_9.pdf
Type
Main Document
Version
Published version
Access type
openaccess
License Condition
CC BY
Size
519.56 KB
Format
Adobe PDF
Checksum (MD5)
22498e83d3dcd73b8d39937a599b106e