Politeness and combination methods for theories with bridging functions
From MaRDI portal
Publication:2303236
DOI10.1007/s10817-019-09512-4zbMath1468.68143OpenAlexW2910685485WikidataQ128586219 ScholiaQ128586219MaRDI QIDQ2303236
Pascal Fontaine, Paula Chocron, Christophe Ringeissen
Publication date: 3 March 2020
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/hal-01988452/file/bridging-nd-full.pdf
Logic in computer science (03B70) Data structures (68P05) Computational aspects of satisfiability (68R07)
Related Items (4)
Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs ⋮ Polite combination of algebraic datatypes ⋮ Politeness for the theory of algebraic datatypes ⋮ A posthumous contribution by Larry Wos: excerpts from an unpublished column
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Model-theoretic methods in combined constraint satisfiability
- Combining sets with cardinals
- Combination of convex theories: modularity, deduction completeness, and explanation
- A rewriting approach to satisfiability procedures.
- Reasoning about algebraic data types with abstractions
- Cooperation of background reasoners in theory reasoning by residue sharing
- Unions of non-disjoint theories and combinations of satisfiability procedures
- Superposition decides the first-order logic fragment over ground theories
- Decision procedures for term algebras with integer constraints
- A Rewriting Approach to the Combination of Data Structures with Bridging Theories
- Combining Satisfiability Procedures for Unions of Theories with a Shared Counting Operator
- A Gentle Non-disjoint Combination of Satisfiability Procedures
- A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited
- Combining Theories with Shared Set Operations
- Simplification by Cooperating Decision Procedures
- Reasoning About Recursively Defined Data Structures
- A Practical Decision Procedure for Arithmetic with Function Symbols
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Hierarchic Superposition with Weak Abstraction
- Polite Theories Revisited
- Combinable Extensions of Abelian Groups
- Locality Results for Certain Extensions of Theories with Bridging Functions
- Decision procedures for algebraic data types with abstractions
- New results on rewrite-based satisfiability procedures
- Connecting many-sorted theories
- Frontiers of Combining Systems
- Logic for Programming, Artificial Intelligence, and Reasoning
This page was built for publication: Politeness and combination methods for theories with bridging functions
