文献

J-GLOBAL ID：201602292201647039   整理番号：16A1365740

帰納的述語定義を含む分離論理における循環証明による半自動証明

著者 (2件)： 仲田壮佑 (名古屋大 大学院情報科学研究科) ,  中澤巧爾 (名古屋大 大学院情報科学研究科)
資料名： 日本ソフトウェア科学会大会講演論文集(CD-ROM)  (日本ソフトウエア科学会大会講演論文集(CD-ROM))
巻： 33rd  ページ： ROMBUNNO.PPL4-2  発行年： 2016年 
JST資料番号： X0080B  ISSN： 1348-0901  資料種別： 会議録 (C)
記事区分： 短報  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 帰納的述語定義を含む分離論理によるプログラムの自動検証に向けて,論理式の半自動証明器を実装した。より具体的には,Brotherstonらの提案した循環証明体系における証明探索を行なう。循環証明体系による証明では,特定の条件のもとで証明木に循環を許し,帰納的に定義された述語を含む論理式の証明を行う。証明探索の際には帰納的述語を定義に従って展開する必要があるが,素朴な方法では適用可能な推論規則の数が爆発的に増加する。展開する述語の選び方と適用する推論規則の順番を制限し,探索の枝刈りを行った。以上のアイディアに基づき,証明探索を行う自動証明器を実装した。本研究で実装した証明器を用いて,様々な帰納的述語定義を含む論理式の自動証明を行った。また,証明可能なときには,証明器に証明木を出力させ,証明探索によって発見された証明を可視化した。(著者抄録)

シソーラス用語： *プログラム検証 ,  論理関数 ,  論理演算 ,  *述語論理 ,  帰納的関数 ,  帰納推論 ,  証明 ,  自動化 ,  可視化
準シソーラス用語： 論理式 ,  帰納的推理 ,  述語 ,  分離論理 ,  定理自動証明

分類 (2件)： 計算理論  (JB02000A) ,  論理代数  (JB03000H)

タイトルに関連する用語 (5件)： 述語 ,  定義 ,  分離論理 ,  循環 ,  証明