Strategies for combining decision procedures

DOI10.1016/j.tcs.2005.11.025zbMath1088.68161OpenAlexW2069422398MaRDI QIDQ2368951

Sylvain Conchon, Sava Krstić

Publication date: 28 April 2006

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2005.11.025

zbMATH Keywords

decision proceduresinference systemsNelson-Oppen combinationShostak's algorithm

Mathematics Subject Classification ID

Related Items (1)

Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates

Uses Software

• ELAN
• Maude
• CVC
• Zapato

Cites Work

• Abstract congruence closure
• Deciding Combinations of Theories
• Fast Decision Procedures Based on Congruence Closure
• Simplification by Cooperating Decision Procedures
• Computer Aided Verification
• Automated Deduction – CADE-19
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Strategies for combining decision procedures