文献

J-GLOBAL ID：201802282022549367   整理番号：18A0204816

極大完備化に基づく等式定理の自動証明

著者 (2件)： 萩原崇央 (新潟大 大学院自然科学研究科) ,  青戸等人 (新潟大 大学院自然科学研究科)
資料名： 日本ソフトウェア科学会大会講演論文集(CD-ROM)  (日本ソフトウエア科学会大会講演論文集(CD-ROM))
巻： 34th  ページ： ROMBUNNO.PPL2-1  発行年： 2017年 
JST資料番号： X0080B  ISSN： 1348-0901  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 項書き換えシステムの代表的な自動証明法として,クヌース・ベンディクス完備化がある。失敗無し完備化(Bachmairら,1989)はクヌース・ベンディクス完備化を利用した等式の定理自動証明法である。一方,完備化の新しい手法として,極大完備化(Klein&広川,2011)が提案されている。極大完備化は,パラメータとして簡約順序を必要としない,SMTソルバを活用した完備化手法である。本報告では,極大完備化を失敗無し極大完備化へと拡張する。具体的には,等式判定手続きへの変更,変数のスコーレム定数への置き換え,向き付け不能な等式による書き換え手続きの追加,柔軟な危険対生成手続きの導入を行い,極大完備化に基づく等式定理の自動証明システムを実現した。また,実装したシステムによる定理証明実験の結果を報告する。(著者抄録)

シソーラス用語： 項書換え系 ,  *等式論理 ,  証明 ,  性質 ,  関数型言語 ,  命題論理 ,  可能性 ,  *定理証明
準シソーラス用語： 一階述語論理 ,  完備性 ,  極大完備化 ,  項書換えシステム ,  自動定理証明 ,  充足可能性

分類 (1件)： その他の情報工学基礎理論  (JB06000C)

タイトルに関連する用語 (2件)： 定理 ,  証明