Combination of disjoint theories: beyond decidability

Abstract : Combination of theories underlies the design of satisfiability modulo theories (SMT) solvers. The Nelson-Oppen framework can be used to build a decision procedure for the combination of two disjoint decidable stably infinite theories. We here study combinations involving an arbitrary first-order theory. Decidability is lost, but refutational completeness is preserved. We consider two cases and provide complete (semi-)algorithms for them. First, we show that it is possible under minor technical conditions to combine a decidable (not necessarily stably infinite) theory and a disjoint finitely axiomatized theory, obtaining a refutationally complete procedure. Second, we provide a refutationally complete procedure for the union of two disjoint finitely axiomatized theories, that uses the assumed procedures for the underlying theories without modifying them.
Type de document :
Communication dans un congrès
Bernhard Gramlich and Dale Miller and Uli Sattler. IJCAR - 6th International Joint Conference on Automated Reasoning - 2012, Jun 2012, Manchester, United Kingdom. Springer, 7364, pp.256-270, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-31365-3_21〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00747271
Contributeur : Pascal Fontaine <>
Soumis le : mardi 30 octobre 2012 - 21:57:15
Dernière modification le : jeudi 20 septembre 2018 - 07:54:02

Lien texte intégral

Identifiants

Collections

Citation

Pascal Fontaine, Stephan Merz, Christoph Weidenbach. Combination of disjoint theories: beyond decidability. Bernhard Gramlich and Dale Miller and Uli Sattler. IJCAR - 6th International Joint Conference on Automated Reasoning - 2012, Jun 2012, Manchester, United Kingdom. Springer, 7364, pp.256-270, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-31365-3_21〉. 〈hal-00747271〉

Partager

Métriques

Consultations de la notice

206