| 講演名 | 2006-12-14 単純型項書換え系における定理自動証明系HOPSYS 蒲田 明憲, 草刈 圭一朗, 西田 直樹, 酒井 正彦, 坂部 俊樹, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 本稿では,高階関数を取り扱える定理自動証明系HOPSYS (Higher-Order Proving System)を紹介する.HOPSYSでは仕様をMLやHaskellなどの関数型言語に似た構文で記述し,それを単純型項書換え系とみなして様々な検証や自動証明を行うことができる.また,利便性を高めるためWebユーザーインターフェースが用意されており,HOPSYSの機能のうち停止性証明,Knuth-Bendix完備化手続き,帰納的定理の自動証明が実行できる.本稿では特にHOPSYSで実現されている帰納的定理の自動証明についてのいくつかの証明法やリップリングと呼ばれる補題探索手法などを紹介する. |
| 抄録(英) | In this paper, we introduce the system HOPSYS (Higher-Order Proving System), an automated theorem prover that can treat higher-order functions. An input of HOPSYS is a specification written in ML/Haskell-like language. HOPSYS can verify many kinds of property and can prove theorems automatically. HOPSYS has a WUI in which we can use verifing termination property, KB completion procedure, and automatic reasoning of inductive theorems. We also introduce automatic reasoning of inductive theorems mainly, and explain some techniques for proving inductive theorems and finding lemmas by rippling. |
| キーワード(和) | 定理自動証明 / 単純型項書換え系 / 潜在帰納法 / 書換え帰納法 / リップリング |
| キーワード(英) | Automatic Thorem Proving / Simply-Typed Term Rewriting System / Inductionless Induction / Rewriting Induction / Rippling |
| 資料番号 | SS2006-57 |
| 発行日 |
| 研究会情報 | |
| 研究会 | SS |
|---|---|
| 開催期間 | 2006/12/7(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Software Science (SS) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 単純型項書換え系における定理自動証明系HOPSYS |
| サブタイトル（和） | |
| タイトル（英） | Automated Program Verification with HOPSYS |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 定理自動証明 / Automatic Thorem Proving |
| キーワード(2)（和/英） | 単純型項書換え系 / Simply-Typed Term Rewriting System |
| キーワード(3)（和/英） | 潜在帰納法 / Inductionless Induction |
| キーワード(4)（和/英） | 書換え帰納法 / Rewriting Induction |
| キーワード(5)（和/英） | リップリング / Rippling |
| 第 1 著者 氏名（和/英） | 蒲田 明憲 / Akinori KAMADA |
| 第 1 著者 所属（和/英） | 名古屋大学大学院情報科学研究科 Graduate School of Information Science, Nagoya University |
| 第 2 著者 氏名（和/英） | 草刈 圭一朗 / Keiichirou KUSAKARI |
| 第 2 著者 所属（和/英） | 名古屋大学大学院情報科学研究科 Graduate School of Information Science, Nagoya University |
| 第 3 著者 氏名（和/英） | 西田 直樹 / Naoki NISHIDA |
| 第 3 著者 所属（和/英） | 名古屋大学大学院情報科学研究科 Graduate School of Information Science, Nagoya University |
| 第 4 著者 氏名（和/英） | 酒井 正彦 / Masahiko SAKAI |
| 第 4 著者 所属（和/英） | 名古屋大学大学院情報科学研究科 Graduate School of Information Science, Nagoya University |
| 第 5 著者 氏名（和/英） | 坂部 俊樹 / Toshiki SAKABE |
| 第 5 著者 所属（和/英） | 名古屋大学大学院情報科学研究科 Graduate School of Information Science, Nagoya University |
| 発表年月日 | 2006-12-14 |
| 資料番号 | SS2006-57 |
| 巻番号（vol） | vol.106 |
| 号番号（no） | 426 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |