| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2010-03-08 11:40 共通記号を持つ背景理論の決定手続きの結合法とその効率化について ○岩沼宏治（山梨大）  SS2009-67 |
|
| 抄録 | （和） | Nelson-Oppen 法は複数の背景理論の決定手続きを結合する代表的な手法であり，近年盛んに研究されているSMT(Satisfiability Modulo Theories)の中核技術の一つであるが，その完全性を保障するためには幾つかの前提条件を満たすことが必要である．その理論的限界の一つを拡張するために，Zarbaは共通記号を持つ背景理論とその決定手続きを取り扱うためにC-tableauxを提案している．本論文\ではこれらの計算体系について概説し，計算の効率化の可能性について考察を行う． |
| （英） | The Nelson-Oppen method is a well-known general framework for combining decision procedures into a single decision procedure, which plays a central role in SMT (Satisfiability Modulo Theories) technologies. The method is restricted to the combination of stably infinite theories over disjoint signatures. Recently, Zarba proposed C-tableaux which combines decision procedures for universal theories which share at most finitely many constants. In this paper, we survey these combination methods and perform a preliminarily study to improve the efficency of these calculi by introducing various methods which were invented in automated tableau-based theorem proving. | |
| キーワード | （和） | Nelson-Oppen法 / C-tableaux / SMT / 背景理論 / 決定手続き / 定理証明 / / |
| （英） | Nelson-Oppen combination method / C-tableaux / SMT / underlying theory / decision method / theorem proving / / | |
| 文献情報 | 信学技報, vol. 109, no. 456, SS2009-67, pp. 115-120, 2010年3月. | |
| 資料番号 | SS2009-67 | |
| 発行日 | 2010-03-01 (SS) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | SS2009-67 |
|
| 研究会情報 | |
| 研究会 | SS |
| 開催期間 | 2010-03-08 - 2010-03-08 |
| 開催地（和） | 鹿児島大学 郡元キャンパス |
| 開催地（英） | Kagoshima Univ. |
| テーマ（和） | 一般 |
| テーマ（英） | general |
| 講演論文情報の詳細 | |
| 申込み研究会 | SS |
| 会議コード | 2010-03-SS |
| 本文の言語 | 日本語 |
| タイトル（和） | 共通記号を持つ背景理論の決定手続きの結合法とその効率化について |
| サブタイトル（和） | |
| タイトル（英） | On a Combination Method of Decision Procedures for Theories Sharing Common Symbols |
| サブタイトル（英） | |
| キーワード(1)（和/英） | Nelson-Oppen法 / Nelson-Oppen combination method |
| キーワード(2)（和/英） | C-tableaux / C-tableaux |
| キーワード(3)（和/英） | SMT / SMT |
| キーワード(4)（和/英） | 背景理論 / underlying theory |
| キーワード(5)（和/英） | 決定手続き / decision method |
| キーワード(6)（和/英） | 定理証明 / theorem proving |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 岩沼 宏治 / Koji Iwanuma / イワヌマ コウジ |
| 第1著者 所属（和/英） | 山梨大学 (略称： 山梨大) University of Yamanashi (略称： Univ. of Yamanashi) |
| 講演者 | 第1著者 |
| 発表日時 | 2010-03-08 11:40:00 |
| 発表時間 | 30分 |
| 申込先研究会 | SS |
| 資料番号 | SS2009-67 |
| 巻番号（vol） | vol.109 |
| 号番号（no） | no.456 |
| ページ範囲 | pp.115-120 |
| ページ数 | 6 |
| 発行日 | 2010-03-01 (SS) |
[研究会発表申込システムのトップページに戻る]