06月12日(Tue) 15:30〜20:00 E会場(-山口県教育会館／第四研修室(72))
| 演題番号 | 1E3-OS-4-7 |
|---|---|
| 題目 | 高速充足可能性判定器を用いた命題論理の結論発見器の実装 |
| 著者 | 村松 匠(山梨大学大学院医学工学総合教育部コンピュータ・メディア工学専攻) 鈴木 健士郎(山梨大学大学院医学工学総合教育部コンピュータ・メディア工学専攻) 鍋島 英知(山梨大学大学院医学工学総合研究部) 岩沼 宏治(山梨大学大学院医学工学総合研究部コンピュータ・メディア工学専攻担当) |
| 時間 | 06月12日(Tue) 17:50〜18:10 |
| 概要 | 本稿では, 命題論理の高速充足可能性判定器(SATソルバー)を利用した結論発見手法を提案する．結論発見とは，特定の語彙に属する論理的帰結を発見する問題である．語彙が言語全体ならば主節発見，空集合ならば反駁発見に相当する．我々は，近年性能向上が著しい高速SATソルバーを利用した反駁定理に基づく結論列挙手法を提案し，SAT技術を利用した各種の効率化手法を示す． |
| 論文 | PDFファイル |