Polite combination in parametric array theories

DOI10.1007/978-3-032-04167-8_9MaRDI QIDQ6852315zbMATH OpenFDO

Authors R. Raja, Christophe Ringeissen

Publication date 26 February 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-032-04167-8_9

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Logic in artificial intelligence (68T27) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT
• Cardinality constraints for arrays (decidability results and applications)
• Combining sets with cardinals
• Combining theories with shared set operations
• Decision Procedures for Multisets with Cardinality Constraints
• Frontiers of Combining Systems
• Higher-order quantifier elimination, counter simulations and fault-tolerant systems
• scientific article; zbMATH DE number 53151 (Why is no real title available?)
• Model-based theory combination
• NP satisfiability for arrays as powers
• On direct products of theories
• Polite combination of algebraic datatypes
• Polite theories revisited
• Reasoning about vectors using an SMT theory of sequences
• Reasoning with finite sets and cardinality constraints in SMT
• Simplification by Cooperating Decision Procedures
• Succinct ordering and aggregation constraints in algebraic array theories
• The first order properties of products of algebraic systems
• Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic

Cited in

(1)

• Modular derivation of decision procedures for extensions of the algebraic theory of arrays

This page was built for publication: Polite combination in parametric array theories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6852315)