Combining Decision Procedures by (Model-)Equality Propagation
DOI10.1016/J.ENTCS.2009.05.048zbMATH Open1347.68309OpenAlexW1994641146MaRDI QIDQ5179357FDOQ5179357
Authors: Diego Caminha B. de Oliveira, David Déharbe, Pascal Fontaine 
Publication date: 19 March 2015
Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.entcs.2009.05.048
Recommendations
- Combining decision procedures by (model-)equality propagation
- Combining decision algorithms for matching in the union of disjoint equational theories
- scientific article; zbMATH DE number 3898849
- Unification in the union of disjoint equational theories: Combining decision procedures
- Logics in Artificial Intelligence
- Integration and propagation of a multi-criteria decision making model in constraint programming
- Deciding equivalence-based properties using constraint solving
- Combining Proof-Producing Decision Procedures
- Decision procedures and model building in equational clause logic
Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- Title not available (Why is that?)
- Isabelle/HOL. A proof assistant for higher-order logic
- Simplification by Cooperating Decision Procedures
- Title not available (Why is that?)
- The existence of refinement mappings
- The B-Book
- Splitting on Demand in SAT Modulo Theories
- Computer Aided Verification
- Fast Decision Procedures Based on Congruence Closure
- Verification of clock synchronization algorithms: experiments on a combination of deductive tools
- Refactoring towards a layered architecture
- An efficient Nelson-Oppen decision procedure for difference constraints over rationals
- Model-based theory combination
- Deciding Combinations of Theories
- Title not available (Why is that?)
- Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis
- Frontiers of Combining Systems
- Formal methods in computer-aided design. 1st international conference, FMCAD '96, Palo Alto, CA, USA, November 6--8, 1996. Proceedings
Cited In (6)
- Title not available (Why is that?)
- Combined Satisfiability Modulo Parametric Theories
- Combining decision procedures by (model-)equality propagation
- Formal Methods for Hardware Verification
- A general setting for flexibly combining and augmenting decision procedures
- Theories, solvers and static analysis by abstract interpretation
Uses Software
This page was built for publication: Combining Decision Procedures by (Model-)Equality Propagation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5179357)
