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 Library locked




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

Abstract, Links, ©

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},
ADDRESS = {Saarbr{\"u}cken},
ISBN = {978-3-642-37650-4},
}


Entry last modified by Viorica Sofronie-Stokkermans, 03/26/2014
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
[Library]
Created
03/07/2011 04:30:18 PM
Revisions
8.
7.
6.
5.
4.
Editor(s)
Viorica Sofronie-Stokkermans
Uwe Waldmann
Uwe Brahm
Viorica Sofronie-Stokkermans
Viorica Sofronie-Stokkermans
Edit Dates
01/23/2014 02:23:56 PM
11.03.2013 16:30:25
11-03-2013 04:22:39 PM
03/06/2013 12:40:39 PM
03/06/2013 12:38:20 PM
Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section