Home >

news Help

Publication Information


Title
Japanese:定理証明支援系のためのライブラリ検索システム作成に向けて 
English: 
Author
Japanese: 瀧本哲史, 森口草介, 渡部卓雄.  
English: Satoshi Takimoto, Sosuke Moriguchi, Takuo Watanabe.  
Language Japanese 
Journal/Book name
Japanese: 
English: 
Volume, Number, Page        
Published date Mar. 5, 2025 
Publisher
Japanese: 
English: 
Conference name
Japanese:日本ソフトウェア科学会第27回プログラミングおよびプログラミング言語ワークショップ(PPL 2025) 
English: 
Conference site
Japanese:愛知県蒲郡市 
English: 
Abstract 定理証明支援系を用いる際，プログラミング言語と同様に，既存のライブラリの結果を再利用することで，証明にかかる手間を大きく削減することができる． 再利用を促進するためには，既存のライブラリを横断的かつ網羅的に検索するシステムがあることが望ましい．しかし，RocqやAgda向けのものは構文的にマッチを行うのみで，簡約といった意味論的な側面は考慮しないなど，定理証明支援系向けの検索システムはまだ検索手法が貧弱であると考える． 本発表では，定理証明支援系ではどのような，またどれほど強力な検索が求められているかや，それをどう実現するかなどについて，現段階での研究結果と今後の展望について説明する．

©2007 Institute of Science Tokyo All rights reserved.