Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
  Combinations of Convex Theories: Modularity, Deduction Completeness and Explanation

Tran, D.-K., Ringeissen, C., Ranise, S., & Kirchner, H. (2010). Combinations of Convex Theories: Modularity, Deduction Completeness and Explanation. Journal of Symbolic Computation, 45(2), 261-268. doi:doi:10.1016/j.jsc.2008.10.006.

Item is

Externe Referenzen

einblenden:

Urheber

einblenden:
ausblenden:
 Urheber:
Tran, Duc-Khanh1, Autor           
Ringeissen, Christopher2, Autor
Ranise, Silvio2, Autor
Kirchner, Helene2, Autor
Affiliations:
1Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              
2External Organizations, ou_persistent22              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: 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.

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 2009-03-272009-06-182010
 Publikationsstatus: Erschienen
 Seiten: -
 Ort, Verlag, Ausgabe: -
 Inhaltsverzeichnis: -
 Art der Begutachtung: Expertenbegutachtung
 Identifikatoren: eDoc: 521085
Anderer: Local-ID: C125716C0050FB51-7E5292801CABC2A8C12575860058A53F-tran-decproc-jsc
DOI: doi:10.1016/j.jsc.2008.10.006
 Art des Abschluß: -

Veranstaltung

einblenden:

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

einblenden:
ausblenden:
Titel: Journal of Symbolic Computation
Genre der Quelle: Zeitschrift
 Urheber:
Affiliations:
Ort, Verlag, Ausgabe: Amsterdam : Elsevier
Seiten: - Band / Heft: 45 (2) Artikelnummer: - Start- / Endseite: 261 - 268 Identifikator: ISSN: 0747-7171
CoNE: https://pure.mpg.de/cone/journals/resource/954922649120