| 演題番号 | 3J1-OS7-7 |
|---|---|
| 題目 | Nelson-Oppen法を組み込んだSMTソルバの設計 |
| 著者 | 福田 寿志(山梨大学大学院医学工学総合教育部コンピュータ・メディア工学専攻) 岩沼 宏治(山梨大学大学院医学工学総合研究部コンピュータ・メディア工学専攻担当) 山本 泰生(山梨大学大学院医学工学総合研究部) |
| 時間 | 06月03日(Fri) 11:05〜11:25 |
| 概要 | SMTは，決定可能な一階論理の部分体系で記述された背景理論を命題SAT技法で効果的に処理するための推論技術である．実用問題で必要となる背景理論は複数の一階論理から構成されているが，Nelson-Oppen法はそれら複数理論の個々の決定手続きを組み合わせて用いるための理論である．本稿ではこのNelson-Oppen法を実装したSMTソルバを試作し，簡単な性能評価実験を行ったので，その報告を行う． |
| 論文 | PDFファイル |