Combining Theories: The Ackerman and Guarded Fragments

Areces, C. and Fontaine, P.. Combining Theories: The Ackerman and Guarded Fragments. In Tinelli, C. and Sofronie-Stokkermans, V., editors, Proceedings of Frontiers of Combining Systems, 8th International Symposium, (FroCoS 2011), Lecture Notes in Computer Science, pp. 40–54, Springer, Saarbruecken, Germany, October 2011.

Download: [pdf] 

Abstract:

Combination of decision procedures is at the heart of Satisfiability Modulo Theories (SMT) solvers. It provides ways to compose decision procedures for expressive languages which mix symbols from various decidable theories. Typical combinations include (linear) arithmetic, uninterpreted symbols, arrays operators, etc. In [7] we showed that any first-order theory from the Bernays-Schonfinkel-Ramsey fragment, the two variable fragment, or the monadic fragment can be combined with virtually any other decidable theory. Here, we complete the picture by considering the Ackermann fragment, and several guarded fragments. All theories in these fragments can be combined with other decidable (combinations of) theories, with only minor restrictions. In particular, it is not required for these other theories to be stably-infinite.

BibTeX: (download)

@INCOLLECTION{arec:comb11,
  author = {Areces, C. and Fontaine, P.},
  title = {Combining Theories: The Ackerman and Guarded Fragments},
  booktitle = {Proceedings of Frontiers of Combining Systems, 8th International
	Symposium, (FroCoS 2011)},
  publisher = {Springer},
  year = {2011},
  editor = {Tinelli, C. and Sofronie-Stokkermans, V.},
  volume = {6989},
  series = {Lecture Notes in Computer Science},
  pages = {40-54},
  address = {Saarbruecken, Germany},
  month = {October},
  abstract = {Combination of decision procedures is at the heart of Satisfiability
	Modulo Theories (SMT) solvers. It provides ways to compose decision
	procedures for expressive languages which mix symbols from various
	decidable theories. Typical combinations include (linear) arithmetic,
	uninterpreted symbols, arrays operators, etc. In [7] we showed that
	any first-order theory from the Bernays-Schonfinkel-Ramsey fragment,
	the two variable fragment, or the monadic fragment can be combined
	with virtually any other decidable theory. Here, we complete the
	picture by considering the Ackermann fragment, and several guarded
	fragments. All theories in these fragments can be combined with other
	decidable (combinations of) theories, with only minor restrictions.
	In particular, it is not required for these other theories to be
	stably-infinite.},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  ee = {http://dx.doi.org/10.1007/978-3-642-24364-6_4}
}

Generated by bib2html.pl (written by Patrick Riley) on Sun Oct 02, 2016 17:05:49