Politeness for the theory of algebraic datatypes

DOI10.1007/978-3-030-51074-9_14OpenAlexW3043890163MaRDI QIDQ2096449

Jane Lange, Pascal Fontaine, Ying Sheng, Christophe Ringeissen, Yoni Zohar, Clark Barrett

Publication date: 9 November 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-51074-9_14

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

Combining stable infiniteness and (strong) politeness ⋮ Politeness and stable infiniteness: stronger together ⋮ Polite combination of algebraic datatypes

Cites Work

• Unnamed Item
• Unnamed Item
• Many-sorted equivalence of shiny and strongly polite theories
• Combining nonstably infinite theories
• Variant-based decidable satisfiability in initial algebras with predicates
• Datatypes with shared selectors
• Theory combination: beyond equality sharing
• Politeness and combination methods for theories with bridging functions
• A decision procedure for (co)datatypes in SMT solvers
• Canonization for disjoint unions of theories
• Rewrite-Based Satisfiability Procedures for Recursive Data Structures
• Combinations of Theories for Decidable Fragments of First-Order Logic
• Simplification by Cooperating Decision Procedures
• A Practical Decision Procedure for Arithmetic with Function Symbols
• Variant-Based Satisfiability in Initial Algebras
• Polite Theories Revisited
• Locality Results for Certain Extensions of Theories with Bridging Functions
• New results on rewrite-based satisfiability procedures
• Coming to terms with quantified reasoning
• Logics in Artificial Intelligence
• Frontiers of Combining Systems
• Combined Satisfiability Modulo Parametric Theories
• Formal Methods at the Crossroads. From Panacea to Foundational Support