Politeness for the theory of algebraic datatypes

DOI10.1007/978-3-030-51074-9_14MaRDI QIDQ2096449zbMATH OpenOpenAlexFDO

Authors Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, 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)

Recommendations

• Polite combination of algebraic datatypes
• Polite theories revisited
• Combined Satisfiability Modulo Parametric Theories
• Politeness and stable infiniteness: stronger together
• Politeness and combination methods for theories with bridging functions

Cites work

• A decision procedure for (co)datatypes in SMT solvers
• A mathematical introduction to logic.
• A Practical Decision Procedure for Arithmetic with Function Symbols
• An abstract decision procedure for a theory of inductive data types.
• Canonization for disjoint unions of theories
• Combinations of Theories for Decidable Fragments of First-Order Logic
• Combined Satisfiability Modulo Parametric Theories
• Combining decision procedures.
• Combining nonstably infinite theories
• Coming to terms with quantified reasoning
• Datatypes with shared selectors
• Frontiers of Combining Systems
• Locality Results for Certain Extensions of Theories with Bridging Functions
• Logics in Artificial Intelligence
• Many-sorted equivalence of shiny and strongly polite theories
• New results on rewrite-based satisfiability procedures
• Polite theories revisited
• Politeness and combination methods for theories with bridging functions
• Rewrite-based satisfiability procedures for recursive data structures
• Simplification by Cooperating Decision Procedures
• Theory combination: beyond equality sharing
• Variant-based decidable satisfiability in initial algebras with predicates
• Variant-Based Satisfiability in Initial Algebras

Cited in

(5)

• Politeness and stable infiniteness: stronger together
• Polite combination of algebraic datatypes
• Politeness and combination methods for theories with bridging functions
• Combining stable infiniteness and (strong) politeness
• Verifying SQL queries using theories of tables and relations

This page was built for publication: Politeness for the theory of algebraic datatypes

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