Polite Theories Revisited

by Dejan Jovanović, Clark Barrett
Abstract:
The classic method of Nelson and Oppen for combining decision procedures requires the theories to be stably-infinite. Unfortunately, some important theories do not fall into this category (e.g. the theory of bit-vectors). To remedy this problem, previous work introduced the notion of polite theories. Polite theories can be combined with any other theory using an extension of the Nelson-Oppen approach. In this paper we revisit the notion of polite theories, fixing a subtle flaw in the original definition. We give a new combination theorem which specifies the degree to which politeness is preserved when combining polite theories. We also give conditions under which politeness is preserved when instantiating theories by identifying two sorts. These results lead to a more general variant of the theorem for combining multiple polite theories.
Reference:
Polite Theories Revisited (Dejan Jovanović, Clark Barrett), In Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR ’10) (Christian G. Fermüller, Andrei Voronkov, eds.), Springer, volume 6397, 2010. (Yogyakarta, Indonesia)
Bibtex Entry:
@inproceedings{JB10-LPAR,
  url       = "http://www.cs.stanford.edu/~barrett/pubs/JB10-LPAR.pdf",
  author    = "Dejan Jovanović and Clark Barrett",
  title     = "Polite Theories Revisited",
  booktitle = "Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR '10)",
  series    = "Lecture Notes in Computer Science",
  volume    = 6397,
  publisher = "Springer",
  editor    = {Christian G. Ferm"{u}ller and Andrei Voronkov},
  pages     = "402--416",
  month     = oct,
  year      = 2010,
  isbn      = "3-642-16241-X, 978-3-642-16241-1",
  issn      = "0302-9743",
  note      = "Yogyakarta, Indonesia",
  category  = "Conference Publications",
  abstract  = "The classic method of Nelson and Oppen for combining decision procedures requires the theories to be stably-infinite. Unfortunately, some important theories do not fall into this category (e.g. the theory of bit-vectors). To remedy this problem, previous work introduced the notion of polite theories. Polite theories can be combined with any other theory using an extension of the Nelson-Oppen approach. In this paper we revisit the notion of polite theories, fixing a subtle flaw in the original definition. We give a new combination theorem which specifies the degree to which politeness is preserved when combining polite theories. We also give conditions under which politeness is preserved when instantiating theories by identifying two sorts. These results lead to a more general variant of the theorem for combining multiple polite theories."
}

Fork me on GitHub