| Item type |
Trans(1) |
| 公開日 |
2018-12-14 |
| タイトル |
|
|
タイトル |
定理証明支援系Coqにおける不等式変形記法 |
| タイトル |
|
|
言語 |
en |
|
タイトル |
A Tactic Library for Transforming Inequalities in Coq |
| 言語 |
|
|
言語 |
jpn |
| キーワード |
|
|
主題Scheme |
Other |
|
主題 |
[通常論文] 定理証明支援系，Coq，宣言的証明，タクティックライブラリ，不等式 |
| 資源タイプ |
|
|
資源タイプ識別子 |
http://purl.org/coar/resource_type/c_6501 |
|
資源タイプ |
journal article |
| 著者所属 |
|
|
|
九州工業大学 |
| 著者所属 |
|
|
|
九州工業大学 |
| 著者所属(英) |
|
|
|
en |
|
|
Kyushu Institute of Technology |
| 著者所属(英) |
|
|
|
en |
|
|
Kyushu Institute of Technology |
| 著者名 |
村田, 康佑
江本, 健斗
|
| 著者名(英) |
Kosuke, Murata
Kento, Emoto
|
| 論文抄録 |
|
|
内容記述タイプ |
Other |
|
内容記述 |
数学定理やプログラムの性質の形式的証明では，自然数上の不等式についての証明が頻出する．しかし，定理証明支援系Coqでの不等式の形式的証明は，非形式的証明とは異なる記法で記述されるため，数学的な直観がそのまま使えないことも多い．たとえば，非形式的証明では，不等式L ≤ Rを証明するために，しばしばL = M1 ≤ M2 = M3 ≤ ・・・ ≤ Mn = Rのように項を不等号で「鎖状」につなげて示す宣言的な記法が用いられる．こうした記法は数学の教科書等でよく馴染んだ記法であり，直観的に理解・記述することが可能である．一方，Coqにはそうした宣言的な記法は標準では用意されていないため，証明の理解・記述が困難になっている．本論文では，Coq上で，自然数上の不等式変形を，非形式的証明のように「鎖状」に記述する手法を提案する．本手法の特徴は，タクティックライブラリによって「鎖状」記法が実現されることにあり，それゆえ，提案記法はライブラリをモジュールとして読み込むだけで既存記法とあわせて使うことができる．また，このタクティックライブラリを用いて，Ackermann関数の性質についての不等式の証明を試みる．その結果，標準的な数学の教科書と近い記法で形式的証明を記述できることを確認する． |
| 論文抄録(英) |
|
|
内容記述タイプ |
Other |
|
内容記述 |
Formal proofs of inequalities on natural numbers is important for formal proofs of mathematical theorems and properties of programs. However, Coq's notation of formal proofs of inequalities is different from that of informal proofs. For instance, when we write an informal proof of inequality L ≤ R, we usually use a declarative notation like a “chain” such that L = M1 ≤ M2 = M3 ≤ ・・・ ≤ Mn = R. Such notation is common in textbooks, and thus it enables us to understand proofs intuitively. On the other hand, standard Coq does not support such a declarative notation, so that we cannot understand proofs in Coq intuitively. In this paper, we propose a novel approach to enable us to write formal proofs in the “chain” notation. One of main features of our approach is that the chain notation is realized as a tactic library, so that we can use it easily by only loading it as a module, and in conjunction with the conventional notation. We also try writing formal proofs for properties of Ackermann function with our tactic library. The result shows that we can write the formal proofs like informal proofs in a textbook. |
| 書誌レコードID |
|
|
収録物識別子タイプ |
NCID |
|
収録物識別子 |
AA11464814 |
| 書誌情報 |
情報処理学会論文誌プログラミング（PRO）
巻 11,
号 4,
p. 1-12,
発行日 2018-12-14
|
| ISSN |
|
|
収録物識別子タイプ |
ISSN |
|
収録物識別子 |
1882-7802 |
| 出版者 |
|
|
言語 |
ja |
|
出版者 |
情報処理学会 |
IPSJ-TPRO1104003.pdf (1.2 MB)
