Combining Decision Procedures by (Model-)Equality Propagation

DOI10.1016/J.ENTCS.2009.05.048MaRDI QIDQ5179357zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

automatic theorem provingSMT solverscombination of decision procedures

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Specification and verification (program logics, model checking, etc.) (68Q60)

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

Cites work

• scientific article; zbMATH DE number 605806 (Why is no real title available?)
• scientific article; zbMATH DE number 1140674 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• An efficient Nelson-Oppen decision procedure for difference constraints over rationals
• Computer Aided Verification
• Deciding Combinations of Theories
• Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis
• Fast Decision Procedures Based on Congruence Closure
• Formal methods in computer-aided design. 1st international conference, FMCAD '96, Palo Alto, CA, USA, November 6--8, 1996. Proceedings
• Frontiers of Combining Systems
• Isabelle/HOL. A proof assistant for higher-order logic
• Model-based theory combination
• Refactoring towards a layered architecture
• Simplification by Cooperating Decision Procedures
• Splitting on Demand in SAT Modulo Theories
• The B-Book
• The existence of refinement mappings
• Verification of clock synchronization algorithms: experiments on a combination of deductive tools

Cited in

(6)

• scientific article; zbMATH DE number 2090084 (Why is no real title available?)
• 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

Describes a project that uses

Uses Software

• HOL Light
• HOL
• z3
• Isabelle/HOL
• ML
• Coq

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)