Polite theories revisited

Dejan Jovanović; Clark Barrett

doi:10.1007/978-3-642-16242-8-29

Polite theories revisited

Dejan Jovanović, Clark Barrett

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English (US)
Title of host publication	Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Proceedings
Editors	Christian G. Fermuller
Pages	402-416
Number of pages	15
DOIs	https://doi.org/10.1007/978-3-642-16242-8-29
State	Published - 2010
Event	17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-17 - Yogyakarta, Indonesia Duration: Oct 10 2010 → Oct 15 2010

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	6397 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-17
Country/Territory	Indonesia
City	Yogyakarta
Period	10/10/10 → 10/15/10

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

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

Cite this

Jovanović, D., & Barrett, C. (2010). Polite theories revisited. In C. G. Fermuller (Ed.), Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Proceedings (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. ed. / Christian G. Fermuller. 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 proceeding › Conference contribution

Jovanović, D & Barrett, C 2010, Polite theories revisited. in CG Fermuller (ed.), Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Proceedings. 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 Fermuller CG, editor, Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Proceedings. 2010. p. 402-416. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-16242-8-29

@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{\'c} and Clark Barrett",

year = "2010",

doi = "10.1007/978-3-642-16242-8-29",

language = "English (US)",

isbn = "364216241X",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "402--416",

editor = "Fermuller, {Christian G.}",

booktitle = "Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Proceedings",

note = "17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-17 ; Conference date: 10-10-2010 Through 15-10-2010",

}

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

AN - SCOPUS:78449265426

SN - 364216241X

SN - 9783642162411

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

A2 - Fermuller, Christian G.

T2 - 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-17

Y2 - 10 October 2010 through 15 October 2010

ER -

Polite theories revisited

Abstract

Publication series

Other

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this