ダウンロード数: 41
このアイテムのファイル:
ファイル | 記述 | サイズ | フォーマット | |
---|---|---|---|---|
2170-09.pdf | 6.48 MB | Adobe PDF | 見る/開く |
タイトル: | Expressing Dung's Extensions as FO-Formulas to Enumerate Them with an SMT Solver (Model theoretic aspects of the notion of independence and dimension) |
著者: | Okamoto, Keishi Kido, Hiroyuki Takai, Toshinori |
著者名の別形: | 岡本, 圭史 木藤, 浩之 高井, 利憲 |
発行日: | Sep-2020 |
出版者: | 京都大学数理解析研究所 |
誌名: | 数理解析研究所講究録 |
巻: | 2170 |
開始ページ: | 64 |
終了ページ: | 72 |
抄録: | It is useful to express constraints for Dung's extensions as FO-formulas so that we can enumerate extensions with an SMT solver. We can extract an extension with a naive SMT solver if we naively express constraints for extensions as FO-formulas. But the definitions of some extensions require maximality /minimality conditions that can not be expressed as FO-formulas. On the other hand, a naive expression is readable but sometimes hard to solve with an SMT solver. Moreover, we need to improve a naive SMT solver to enumerate extensions since an enumeration is an iteration of an extraction. In this paper, we propose a method to enumerate Dung's extensions by solving a Partial Maximal Satisfiable Subsets Enumeration problem, which is an extension of a Maximal Satisfiable Subsets Enumeration problem[l]. In particular, we express hard constraints and soft constraints, which are required for a Partial Maximal Satisfiable Subsets Enumeration problem, with FO-formulas. |
URI: | http://hdl.handle.net/2433/261565 |
出現コレクション: | 2170 モデル理論における独立概念と次元の研究 |
このリポジトリに保管されているアイテムはすべて著作権により保護されています。