WEKO3
アイテム
Formal Proof of Higman's Lemma on Isabelle/HOL
https://ipsj.ixsq.nii.ac.jp/records/83520
https://ipsj.ixsq.nii.ac.jp/records/8352084351002-e61d-40ed-8702-99b17f70c2fc
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-TPRO0503012.pdf (27.2 kB)
|
Copyright (c) 2012 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | Trans(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 2012-08-20 | |||||||
| タイトル | ||||||||
| タイトル | Formal Proof of Higman's Lemma on Isabelle/HOL | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | Formal Proof of Higman's Lemma on Isabelle/HOL | |||||||
| 言語 | ||||||||
| 言語 | eng | |||||||
| キーワード | ||||||||
| 主題Scheme | Other | |||||||
| 主題 | [発表概要] | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||||
| 資源タイプ | journal article | |||||||
| 著者所属 | ||||||||
| Japan Advanced Institute of Science and Technology | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Japan Advanced Institute of Science and Technology | ||||||||
| 著者名 |
Mizuhito, Ogawa
× Mizuhito, Ogawa
|
|||||||
| 著者名(英) |
Mizuhito, Ogawa
× Mizuhito, Ogawa
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | This paper reports a formal proof of Higman's lemma on Isabelle/HOL, including its brief history of its proofs, both informal and formal ones. Among them, we focus on a formal proof based on open induction. A technical problem in a formal proof of Higman's lemma is how to manage various orderings. They share the axioms of orderings in many different contexts, with additional axioms, e.g., total ordering, well-founded ordering, and well-quasi-ordering. Isabelle provides two methods: (old) axclass and (latest) locale. We discuss on the limitaton on axclass and how to overcome it by locale. | |||||||
| 論文抄録(英) | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | This paper reports a formal proof of Higman's lemma on Isabelle/HOL, including its brief history of its proofs, both informal and formal ones. Among them, we focus on a formal proof based on open induction. A technical problem in a formal proof of Higman's lemma is how to manage various orderings. They share the axioms of orderings in many different contexts, with additional axioms, e.g., total ordering, well-founded ordering, and well-quasi-ordering. Isabelle provides two methods: (old) axclass and (latest) locale. We discuss on the limitaton on axclass and how to overcome it by locale. | |||||||
| 書誌レコードID | ||||||||
| 収録物識別子タイプ | NCID | |||||||
| 収録物識別子 | AA11464814 | |||||||
| 書誌情報 |
情報処理学会論文誌プログラミング（PRO） 巻 5, 号 3, p. 66-66, 発行日 2012-08-20 |
|||||||
| ISSN | ||||||||
| 収録物識別子タイプ | ISSN | |||||||
| 収録物識別子 | 1882-7802 | |||||||
| 出版者 | ||||||||
| 言語 | ja | |||||||
| 出版者 | 情報処理学会 | |||||||
