Part, Chapter of a Book @InBook, Buchkapitel Beitrag im Sammelband

 Show entries of: this year (2019) | last year (2018) | two years ago (2017) | Notes URL
 Action: login to update Options: Library locked Goto entry point

 Author, Editor
 Author(s): Sofronie-Stokkermans, Viorica dblp
 Editor(s): Voronkov, Andrei Weidenbach, Christoph dblp dblp Not MPII Editor(s): Voronkov, Andrei
 BibTeX cite key*: Sofronie-wlphg11

 Title, Booktitle
 Title*: On combinations of local theory extensions Booktitle*: Programming Logics, Essays in Memory of Harald Ganzinger Chapter: Series: Lecture Notes in Computer Science Language: English

 Publisher
 Name*: Springer URL: http://www.springer-ny.com/ Address*: Berlin Publication Type:

 Vol, No, pp., Year
 Volume: 7797 Number: - Edition: Pages*: 392-413 Month: VG Wort Pages: ISBN: 978-3-642-37650-4 Year*: 2013

 Note: LaTeX Abstract: Many problems in mathematics and computer science can be reduced to proving the satisfiability of conjunctions of literals in a background theory which is often the extension of a base theory with additional functions or a combination of theories. It is therefore important to have efficient procedures for checking satisfiability of conjunctions of ground literals in extensions and combinations of theories. For a special type of theory extensions, namely {\em local extensions}, hierarchic reasoning, in which a theorem prover for the base theory can be used as a black box'', is possible. Many theories used in computer science or mathematics are local extensions of a base theory. However, often it is necessary to consider complex extensions of a theory, with various types of functions. In this paper we identify situations in which a combination of local extensions of a base theory is guaranteed to be again a local extension of the base theory. We thus obtain criteria both for recognizing wider classes of local theory extensions, and for modular reasoning in combinations of theories over non-disjoint signatures. URL Abstract: Tags, Keywords: Copyright Message: HyperLinks / References / URLs: Personal Comments: noch nicht ersch. 15.03.2012/ab? Download Access Level: Public

 Correlation
 MPG Unit: Max-Planck-Institut für Informatik MPG Subunit: Automation of Logic Audience: popular Appearance: MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort
BibTeX Entry:
@INBOOK{Sofronie-wlphg11,
AUTHOR = {Sofronie-Stokkermans, Viorica},
EDITOR = {Voronkov, Andrei and Weidenbach, Christoph},
TITLE = {On combinations of local theory extensions},
BOOKTITLE = {Programming Logics, Essays in Memory of Harald Ganzinger},
PUBLISHER = {Springer},
YEAR = {2013},
NUMBER = {-},
VOLUME = {7797},
PAGES = {392--413},
SERIES = {Lecture Notes in Computer Science},