Polite combination of algebraic datatypes
From MaRDI portal
Publication:2090130
DOI10.1007/s10817-022-09625-3OpenAlexW4229059058MaRDI QIDQ2090130
Pascal Fontaine, Ying Sheng, Christophe Ringeissen, Clark Barrett, Yoni Zohar, Jane Lange
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
automated reasoningsatisfiability modulo theoriestheory combinationalgebraic datatypespolite combination
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Many-sorted equivalence of shiny and strongly polite theories
- Combining nonstably infinite theories
- Combination of convex theories: modularity, deduction completeness, and explanation
- 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
- Variant-based decidable satisfiability in initial algebras with predicates
- Datatypes with shared selectors
- Cooperation of background reasoners in theory reasoning by residue sharing
- Politeness and stable infiniteness: stronger together
- Politeness for the theory of algebraic datatypes
- 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
This page was built for publication: Polite combination of algebraic datatypes
