Combination of disjoint theories: beyond decidability - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2012

Combination of disjoint theories: beyond decidability

Résumé

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.
Fichier non déposé

Dates et versions

hal-00747271 , version 1 (30-10-2012)

Identifiants

Citer

Pascal Fontaine, Stephan Merz, Christoph Weidenbach. Combination of disjoint theories: beyond decidability. IJCAR - 6th International Joint Conference on Automated Reasoning - 2012, Jun 2012, Manchester, United Kingdom. pp.256-270, ⟨10.1007/978-3-642-31365-3_21⟩. ⟨hal-00747271⟩
124 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More