Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
 
 
DownloadE-Mail
 Lokale TagsFreigabegeschichteDetailsÜbersicht
  Interpolation in local theory extensions

Sofronie-Stokkermans, V. (2006). Interpolation in local theory extensions. In U. Furbach, & N. Shankar (Eds.), Proceedings of IJCAR 2006 (pp. 235-250). New York: Springer.

Item is

 

einblenden: alle ausblenden: alle

Basisdaten

einblenden: ausblenden:
Datensatz-Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-24CD-F Versions-Permalink: https://hdl.handle.net/11858/00-001M-0000-002D-7BE2-1
Genre: Konferenzbeitrag

Dateien

einblenden: Dateien
ausblenden: Dateien
:
sofronie-ijcar-06.pdf (beliebiger Volltext), 193KB
 
Datei-Permalink:
-
Name:
sofronie-ijcar-06.pdf
Beschreibung:
-
OA-Status:
Sichtbarkeit:
Privat
MIME-Typ / Prüfsumme:
application/pdf
Technische Metadaten:
Copyright Datum:
-
Copyright Info:
-
Lizenz:
-

Externe Referenzen

einblenden:

Urheber

einblenden:
ausblenden:
 Urheber:
Sofronie-Stokkermans, Viorica1, Autor           
Affiliations:
1Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: Many problems in mathematics and computer science (e.g. in verification, or when reasoning in and about distributed databases) can be reduced to proving the satisfiability of conjunctions of (ground) literals modulo a background theory. This theory can, for instance, be the extension of a base theory with additional functions or a combination of theories. It is therefore very important to find efficient methods for checking the unsatisfiability of ground formulae in such complex theories. However, it is often equally important to find local causes for inconsistency. Such information is usually provided by interpolants. In this paper we study interpolation in local extensions of a base theory ${\cal T}_0$. In such extensions efficient hierarchical reasoning -- in which a prover for the base theory is used as a black box -- is possible. We identify situations in which it is possible to obtain interpolants in a hierarchical manner, by using a prover and a procedure for generating interpolants in ${\cal T}_0$ as `black-boxes' in order to generate interpolants in the extension. We provide several examples of such theories, and discuss their applications in verification or knowledge representation.

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 2007-03-122006
 Publikationsstatus: Erschienen
 Seiten: -
 Ort, Verlag, Ausgabe: -
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: eDoc: 521705
Anderer: Local-ID: C125716C0050FB51-CBB53CEA861FCCE0C125729C0035814B-Sofronie-ijcar-06
 Art des Abschluß: -

Veranstaltung

einblenden:
ausblenden:
Titel: Untitled Event
Veranstaltungsort: Seattle, USA
Start-/Enddatum: 2006-08-17 - 2006-08-21

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

einblenden:
ausblenden:
Titel: Proceedings of IJCAR 2006
Genre der Quelle: Konferenzband
 Urheber:
Furbach, Ulrich, Herausgeber
Shankar, Natarajan, Herausgeber
Affiliations:
-
Ort, Verlag, Ausgabe: New York : Springer
Seiten: - Band / Heft: - Artikelnummer: - Start- / Endseite: 235 - 250 Identifikator: -

Quelle 2

einblenden:
ausblenden:
Titel: Lecture Notes in Artificial Intelligence
Genre der Quelle: Reihe
 Urheber:
Affiliations:
Ort, Verlag, Ausgabe: -
Seiten: - Band / Heft: 4130 Artikelnummer: - Start- / Endseite: - Identifikator: -