Combination of convex theories: modularity, deduction completeness, and explanation
From MaRDI portal
Publication:1041593
DOI10.1016/j.jsc.2008.10.006zbMath1192.68190OpenAlexW1994486216MaRDI QIDQ1041593
Duc-Khanh Tran, Christophe Ringeissen, Silvio Ranise, Hélène Kirchner
Publication date: 3 December 2009
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/inria-00331479/file/RR-6688.pdf
Related Items (5)
A Rewriting Approach to the Combination of Data Structures with Bridging Theories ⋮ A superposition calculus for abductive reasoning ⋮ Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates ⋮ Politeness and combination methods for theories with bridging functions ⋮ Polite combination of algebraic datatypes
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Combining matching algorithms: The regular case
- Combining unification algorithms
- Intelligent backtracking in \(\text{CLP}(\Re)\)
- A rewriting approach to satisfiability procedures.
- Abstract congruence closure
- Unions of non-disjoint theories and combinations of satisfiability procedures
- Efficient theory combination via Boolean search
- Decision procedures for extensions of the theory of arrays
- Normalized rewriting: An alternative to rewriting modulo a set of equations
- Combining Proof-Producing Decision Procedures
- Simplify: a theorem prover for program checking
- Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures
- Deciding Combinations of Theories
- Simplification by Cooperating Decision Procedures
- Variations on the Common Subexpression Problem
- Efficiency of a Good But Not Linear Set Union Algorithm
- Shostak's congruence closure as completion
- On Shostak's decision procedure for combinations of theories
- A comprehensive combination framework
- New results on rewrite-based satisfiability procedures
- Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis
- Automatic Combinability of Rewriting-Based Satisfiability Procedures
- Theoretical Aspects of Computing – ICTAC 2005
- Term Rewriting and Applications
- Term Rewriting and Applications
- Theoretical Aspects of Computing - ICTAC 2004
- Verification, Model Checking, and Abstract Interpretation
- Tools and Algorithms for the Construction and Analysis of Systems
- Formal Methods at the Crossroads. From Panacea to Foundational Support
- Automated Deduction – CADE-19
This page was built for publication: Combination of convex theories: modularity, deduction completeness, and explanation
