文献

J-GLOBAL ID：200902294342204746   整理番号：09A0986752

異なる帰納スキームにまたがる性質の定理証明手法

著者 (2件)： 吉丸始須雄 (関西学院大 大学院理工学研究科) ,  高橋和子 (関西学院大 大学院理工学研究科)
資料名： 日本ソフトウェア科学会大会講演論文集(CD-ROM)  (日本ソフトウエア科学会大会講演論文集(CD-ROM))
巻： 26th  ページ： ROMBUNNO.1B-2  発行年： 2009年 
JST資料番号： X0080B  ISSN： 1348-0901  資料種別： 会議録 (C)
記事区分： 短報  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 本研究は,自然数と二分木という異なる帰納スキームを対応させる手法として,二進数を利用するアプローチを提案し,その対応関係について定理証明器Isabelle/HOLによる証明を行うものである。定理証明では一般に,帰納的推論による証明が行われる。そのため,自然数と二分木の対応関係について議論するには,まずそれらの帰納スキームを対応させることが必要となる。ここでは,二分木構造を用いた具体的な事例として理想的電子現金方式に着目し,その条件のひとつである分割利用可能性についての検証を試みた。これは,一度発行された電子現金を,利用合計金額が額面の金額になるまで何度でも使うことができる,という性質である。この性質が,自然数と二分木の対応関係について記述したモデルの上で成り立っていることを証明することにより,二分木構造の電子現金と自然数としての金額が対応していることを示した。(著者抄録)

シソーラス用語： *定理証明 ,  整数 ,  二分木 ,  *帰納推論 ,  分割法 ,  財 ,  数学モデル
準シソーラス用語： 自然数 ,  電子現金

分類 (2件)： 計算理論  (JB02000A) ,  人工知能  (JE08000Z)

タイトルに関連する用語 (5件)： 帰納 ,  スキーム ,  性質 ,  定理証明 ,  手法