Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Conferences, Workshops, Symposiums, and Seminars
  4. Polite Combination in Parametric Array Theories
 
conference paper

Polite Combination in Parametric Array Theories

Raya, Rodrigo  
•
Ringeissen, Christophe
Thiemann, René
•
Weidenbach, Christoph
September 15, 2025
Frontiers of Combining Systems - 15th International Symposium, FroCoS 2025, Proceedings
15th International Symposium on Frontiers of Combining Systems

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.

  • Files
  • Details
  • Metrics
Loading...
Thumbnail Image
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

Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés