Interpolation in local theory extensions

Sofronie-Stokkermans, Viorica

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 公開

表示: 全項目非表示: 全項目

基本情報

表示: 非表示:

アイテムのパーマリンク: https://hdl.handle.net/11858/00-001M-0000-000F-24CD-F 版のパーマリンク: https://hdl.handle.net/11858/00-001M-0000-002D-7BE2-1

資料種別: 会議論文

ファイル

表示: ファイル

非表示: ファイル

:

sofronie-ijcar-06.pdf (全文テキスト（全般）), 193KB

ファイルのパーマリンク:
-

ファイル名:
sofronie-ijcar-06.pdf

説明:
-

OA-Status:

閲覧制限:
非公開

MIMEタイプ / チェックサム:
application/pdf

技術的なメタデータ:

著作権日付:
-

著作権情報:
-

CCライセンス:
-

作成者

表示:

非表示:

作成者:
Sofronie-Stokkermans, Viorica¹, 著者

所属:
1Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545

内容説明

表示:

非表示:

キーワード: -

要旨: 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.

資料詳細

表示:

非表示:

言語: eng - English

日付: 修正: 2007-03-12出版: 2006

出版の状態: 出版

ページ: -

出版情報: -

目次: -

査読: -

識別子（DOI, ISBNなど）: eDoc: 521705
その他: Local-ID: C125716C0050FB51-CBB53CEA861FCCE0C125729C0035814B-Sofronie-ijcar-06

学位: -

訴訟

表示:

Project information

表示:

出版物 1

表示:

非表示:

出版物名: Proceedings of IJCAR 2006

種別: 会議論文集

著者・編者:
Furbach, Ulrich, 編集者
Shankar, Natarajan, 編集者

所属:
-

出版社, 出版地: New York : Springer

ページ: - 巻号: - 通巻号: - 開始・終了ページ: 235 - 250 識別子（ISBN, ISSN, DOIなど）: -

出版物 2

表示:

非表示:

出版物名: Lecture Notes in Artificial Intelligence

種別: 連載記事

著者・編者:

所属:

出版社, 出版地: -

ページ: - 巻号: 4130 通巻号: - 開始・終了ページ: - 識別子（ISBN, ISSN, DOIなど）: -

アイテム詳細

基本情報

ファイル

関連URL

作成者

内容説明

資料詳細

関連イベント

訴訟

Project information

出版物 1

出版物 2