Polite combination of algebraic datatypes

DOI10.1007/S10817-022-09625-3MaRDI QIDQ2090130zbMATH OpenOpenAlexFDO

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

Publication date 24 October 2022

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2004.04854

zbMATH Keywords

algebraic datatypesautomated reasoningpolite combinationsatisfiability modulo theoriestheory combination

Mathematics Subject Classification ID

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

Recommendations

• Politeness for the theory of algebraic datatypes
• Polite theories revisited
• Politeness and stable infiniteness: stronger together
• Politeness and combination methods for theories with bridging functions
• A polite non-disjoint combination method: theories with bridging functions revisited

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
• Combination of convex theories: modularity, deduction completeness, and explanation
• Combinations of Theories for Decidable Fragments of First-Order Logic
• Combined Satisfiability Modulo Parametric Theories
• Combining nonstably infinite theories
• Coming to terms with quantified reasoning
• Cooperation of background reasoners in theory reasoning by residue sharing
• Datatypes with shared selectors
• Formal methods at the crossroads. From Panacea to foundational support. 10th anniversary colloquium of UNU/IIST, the International Institute for Software Technology of The United Nations University, Lisbon, Portugal, March 18--20, 2002. Revised papers
• Frontiers of Combining Systems
• scientific article; zbMATH DE number 2086596 (Why is no real title available?)
• 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
• Politeness and stable infiniteness: stronger together
• Politeness for the theory of algebraic datatypes
• 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

(8)

• Politeness and stable infiniteness: stronger together
• Politeness for the theory of algebraic datatypes
• Combining Finite Combination Properties: Finite Models and Busy Beavers
• Number theory combination: natural density and SMT
• Polite combination in parametric array theories
• Shininess, strong politeness, and unicorns
• Combining combination properties. I: Nelson-Oppen and politeness
• Modular derivation of decision procedures for extensions of the algebraic theory of arrays

Describes a project that uses

Uses Software

• CVC4

This page was built for publication: Polite combination of algebraic datatypes

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