Journal Article
@Article
Artikel in Fachzeitschrift


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(s)

Author(s):

Tran, Duc-Khanh
Ringeissen, Christopher
Ranise, Silvio
Kirchner, Helene

dblp
dblp
dblp
dblp

Not MPG Author(s):

Ringeissen, Christopher
Ranise, Silvio
Kirchner, Helene

BibTeX cite key*:

tran-decproc-jsc

Title

Title*:

Combinations of Convex Theories: Modularity, Deduction Completeness and Explanation

Journal

Journal Title*:

Journal of Symbolic Computation

Journal's URL:

http://www.elsevier.com/wps/find/journaldescription.cws_home/622902/description#description

Download URL
for the article:

http://dx.doi.org/10.1016/j.jsc.2008.10.006

Language:

English

Publisher

Publisher's
Name:

Elsevier

Publisher's URL:

http://www.elsevier.com/wps/find/homepage.cws_home

Publisher's
Address:

Amsterdam, The Netherlands

ISSN:

0747-7171

Vol, No, pp, Date

Volume*:

45-

Number:

2

Publishing Date:

2009

Pages*:

261-286

Number of
VG Pages:


Page Start:

261

Page End:

286

Sequence Number:


DOI:

10.1016/j.jsc.2008.10.006

Note, Abstract, ©

Note:

Accepted for publication

(LaTeX) Abstract:

Decision procedures are key components of theorem provers and
constraint satisfaction systems. Their modular combination is of
prime interest for building efficient systems, but their effective
use is often limited by poor interface capabilities, when such
procedures only provide a simple ``sat/unsat'' answer. In this
paper, we develop a framework to design cooperation schemas between
such procedures while maintaining modularity of their
interfaces. First, we use the framework to specify and prove the
correctness of classic combination schemas by Nelson-Oppen and
Shostak. Second, we introduce the concept of deduction complete
satisfiability procedures, we show how to build them for large
classes of theories, then we provide a schema to modularly
combine them. Third, we consider the problem of modularly
constructing explanations for combinations by re-using available
proof-producing procedures for the component theories.

URL for the Abstract:


Categories,
Keywords:


HyperLinks / References / URLs:


Copyright Message:


Personal Comments:


Download
Access Level:

Public

Correlation

MPG Unit:

Max-Planck-Institut für Informatik



MPG Subunit:

Automation of Logic

Appearance:

MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort


BibTeX Entry:

@ARTICLE{tran-decproc-jsc,
AUTHOR = {Tran, Duc-Khanh and Ringeissen, Christopher and Ranise, Silvio and Kirchner, Helene},
TITLE = {Combinations of Convex Theories: Modularity, Deduction Completeness and Explanation},
JOURNAL = {Journal of Symbolic Computation},
PUBLISHER = {Elsevier},
YEAR = {2009},
NUMBER = {2},
VOLUME = {45-},
PAGES = {261--286},
ADDRESS = {Amsterdam, The Netherlands},
ISBN = {0747-7171},
DOI = {10.1016/j.jsc.2008.10.006},
NOTE = {Accepted for publication},
}


Entry last modified by Anja Becker, 03/25/2010
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/27/2009 05:08:14 PM
Revision
1.
0.


Editor
Anja Becker
Viorica Sofronie-Stokkermans


Edit Date
25.03.2010 13:50:06
03/27/2009 05:08:14 PM


Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section