Polite theories revisited

Dejan Jovanović, Clark Barrett

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationLogic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Proceedings
Pages402-416
Number of pages15
Volume6397 LNCS
DOIs
StatePublished - 2010
Event17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-17 - Yogyakarta, Indonesia
Duration: Oct 10 2010Oct 15 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6397 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-17
CountryIndonesia
CityYogyakarta
Period10/10/1010/15/10

Fingerprint

Defects
Decision Procedures
Theorem
Sort

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Jovanović, D., & Barrett, C. (2010). Polite theories revisited. In Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Proceedings (Vol. 6397 LNCS, pp. 402-416). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6397 LNCS). https://doi.org/10.1007/978-3-642-16242-8-29

Polite theories revisited. / Jovanović, Dejan; Barrett, Clark.

Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Proceedings. Vol. 6397 LNCS 2010. p. 402-416 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6397 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Jovanović, D & Barrett, C 2010, Polite theories revisited. in Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Proceedings. vol. 6397 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6397 LNCS, pp. 402-416, 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-17, Yogyakarta, Indonesia, 10/10/10. https://doi.org/10.1007/978-3-642-16242-8-29
Jovanović D, Barrett C. Polite theories revisited. In Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Proceedings. Vol. 6397 LNCS. 2010. p. 402-416. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-16242-8-29
Jovanović, Dejan ; Barrett, Clark. / Polite theories revisited. Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Proceedings. Vol. 6397 LNCS 2010. pp. 402-416 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{8950052bbee04be999558272f83572ee,
title = "Polite theories revisited",
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.",
author = "Dejan Jovanović and Clark Barrett",
year = "2010",
doi = "10.1007/978-3-642-16242-8-29",
language = "English (US)",
isbn = "364216241X",
volume = "6397 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "402--416",
booktitle = "Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Proceedings",

}

TY - GEN

T1 - Polite theories revisited

AU - Jovanović, Dejan

AU - Barrett, Clark

PY - 2010

Y1 - 2010

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=78449265426&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=78449265426&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-16242-8-29

DO - 10.1007/978-3-642-16242-8-29

M3 - Conference contribution

SN - 364216241X

SN - 9783642162411

VL - 6397 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 402

EP - 416

BT - Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Proceedings

ER -