定理証明支援系のためのライブラリ検索システム作成に向けて

瀧本哲史; 森口草介; 渡部卓雄

論文・著書情報

タイトル

和文:	定理証明支援系のためのライブラリ検索システム作成に向けて
英文:

著者

和文:	瀧本哲史, 森口草介, 渡部卓雄.
英文:	Satoshi Takimoto, Sosuke Moriguchi, Takuo Watanabe.

言語

Japanese

掲載誌/書名

和文:
英文:

巻, 号, ページ

出版年月

2025年3月5日

出版者

和文:
英文:

会議名称

和文:	日本ソフトウェア科学会第27回プログラミングおよびプログラミング言語ワークショップ(PPL 2025)
英文:

開催地

和文:	愛知県蒲郡市
英文:

アブストラクト

定理証明支援系を用いる際，プログラミング言語と同様に，既存のライブラリの結果を再利用することで，証明にかかる手間を大きく削減することができる．再利用を促進するためには，既存のライブラリを横断的かつ網羅的に検索するシステムがあることが望ましい．しかし，RocqやAgda向けのものは構文的にマッチを行うのみで，簡約といった意味論的な側面は考慮しないなど，定理証明支援系向けの検索システムはまだ検索手法が貧弱であると考える．本発表では，定理証明支援系ではどのような，またどれほど強力な検索が求められているかや，それをどう実現するかなどについて，現段階での研究結果と今後の展望について説明する．

Home

各種検索

サポート

T2R2について

関連リンク

論文・著書情報