Mizarによる数論アルゴリズムの形式化と検証(一般,情報セキュリティ,ライフログ活用技術,ライフインテリジェンス,オフィス情報システム,一般)
スポンサーリンク
概要
- 論文の詳細を見る
本稿では数論アルゴリズムからユークリッドの互除法と拡張ユークリッドの互除法を取り上げ,プルーフチェッカMizarを用いて形式化を行う.本研究での目的は数論を扱うツールの実装を支援することである.本研究で形式化を行ったアルゴリズムは数論システムであるNZMATHのソースコードに基づいている.
- 2011-11-07
著者
-
師玉 康成
信州大学工学部情報工学科
-
岡崎 裕之
信州大学工学部
-
師玉 康成
信州大学工学部
-
師玉 康成
信州大
-
師玉 康成
信州大学 工学部
-
師玉 康成
信州大学
-
岡崎 裕之
信州大学大学院工学系研究科情報工学専攻
-
青木 祥希
信州大学
-
岡崎 裕之
信州大学
関連論文
- コンカレントエンジニアリングを目指したロボット設計製作教育
- 工学教育としてのロボットコンテストの意義
- 拡張ペトリネットを用いた情報収集の為の分散アルゴリズムの設計
- (22)学社融合によるロボット教室の試み : 親子のロボット工作教室(第6セッション 個性化・活性化(I))
- 広選択度広帯域マイクロストリップラインフィルタによるCATV上り拡張アンプに関する研究(ネットワークプロセッサ,通信のための信号処理,及び一般)
- 広選択度広帯域マイクロストリップラインフィルタによるCATV上り拡張アンプに関する研究(ネットワークプロセッサ,通信のための信号処理,及び一般)
- 広選択度広帯域マイクロストリップラインフィルタによるCATV上り拡張アンプに関する研究(ネットワークプロセッサ,通信のための信号処理,及び一般)
- N-5 プログラミングレポート自動評価における事前処理(教育支援システム(1),N.教育・人文科学)
- 中心多様体と弱非線形系H^∞制御
- 拡張ペトリネットを用いた情報収集の為の分散アルゴリズムの設計
- Moodle用数理演習モジュールを用いたWeb上での数理教育手法(ユビキタス・モバイル学習環境/一般)
- 形式化数学言語システムMizarを用いたCMS/Moodleの数理演習モジュール開発(e-learning/一般)
- 拡張ペトリネットとJava/PNMLによる並列システムの構成手法(コンカレントシステム,離散事象システム,ハイブリッドシステム,及び一般)
- 7-213 信州大学インターネット大学院・大学の現状(オーガナイズドセッション「バーチャルユニバーシティ」)
- IEEE802.11g 無線 LAN を用いた山間地拠点間接続の長距離化(ネットワークプロセッサ, 通信のための信号処理, 符号理論, 一般)
- IEEE802.11g 無線 LAN を用いた山間地拠点間接続の長距離化(ネットワークプロセッサ, 通信のための信号処理, 符号理論, 一般)
- IEEE802.11g無線LANを用いた山間地拠点間接続の長距離化(ネットワークプロセッサ, 通信のための信号処理, 符号理論, 一般)
- IEEE802.11g無線LANを用いた山間地拠点間接続の長距離化
- IEEE802.11g無線LANを用いた山間地拠点間接続の長距離化
- IEEE802.11g無線LANを用いた山間地拠点間接続の長距離化
- 自己組織化マップを用いたニューラルネットワークによる高分子物性予測(OS4b 逆問題解析手法の開発と最新応用)
- 追従制御問題の一解法と, マニピュレータ制御への応用
- あるファジィ集合族のコンパクト性
- ある階層型ニューラルネットワーク集合のコンパクト性
- 制御量制約のある非線形追従制御の一解法
- ファジィ集合族のコンパクト性について
- 3-リンク系の非線形追従制御問題の一解法
- 非線形追従制御の一解法
- 前件部変数をファジィ数とした推論法に関する一考察(NW管理)
- (204)情報セキュリティマネジメント向けe-learning教育用コンテンツの作成 : 高校生に対する情報社会に参画する態度の育成(セッション58 コンピュータ援用教育I)
- (73)信州大学インターネット大学院におけるCAIサーバの高信頼性化(セッション21 e-ラーニング(インターネット・マルチメディア利用教育を含む)I)
- (72)個別の学習進捗に対応したe-Learning教材表示制御システム(セッション21 e-ラーニング(インターネット・マルチメディア利用教育を含む)I)
- 拡張ペトリネットによる並列システム設計とエンジンプログラムの試作(コンカレント工学理論と応用一般)
- 信州大学インターネット大学院
- [特別講演]信州大学インターネット大学院におけるサーバ運用の高信頼化について(リッチメディア,信頼性・セキュリティ,一般)
- 信州大学インターネット大学院におけるマルチメディア教材の利用と履修状況について
- (25)設計製作教育における3次元モデルに関する考察(第7セッション 教育システム(実験・設計製図等)(II))
- (24)ものづくり教育における個人製作とグループ製作(第7セッション 教育システム(実験・設計製図等)(II))
- 2P1-A03 高所レスキューを題材としたロボット製作
- ロボット製作を通したグループ学習の分析
- Team-Teachingによるロボット製作の実践
- 四輪独立駆動型全方向移動ロボットの運動学と走行特性
- 信州大学インターネット大学院におけるマルチメディア教材の利用と履修状況について
- 活性炭の透過電子顕微鏡像からのファジィテンプレートによる境界抽出法
- 長距離無線LANと広域CATV通信網接続による山岳医療情報ネットワークの構築
- ニューラルネットワークを用いた局地海上風の予測への試み
- ニューラルネットワークを用いた局所的な気象予測法について
- 遺伝的アルゴリズムを用いたファジイ推論の最適化の収束性
- ファジィ推論の遺伝的アルゴリズムを用いた最適化
- 非線形フィードバックと不動点問題
- ファジー集合論を用いた画像処理
- ファジィ集合族のコンパクト性とファジィ最適制御の存在
- ロボットマニピュレ-タのロバストコントロ-ラの一構成法
- 有界なパラメータを含む最適制御問題のためのこう配法
- 合成リカッチ変換によるある非線形最適制御問題の数値計算法とマニピュレータ制御問題への応用
- (71)ストリーミングメディアに連動させるe-Learning向け電子出版物の遠隔制御(第19セッション インターネット・マルチメティアの利用(I))
- 合成リカッチ変換による非線形最適制御問題の数値計算法 : 終端時刻未知問題
- 積分多様体と弱非線形制御系
- 積分多様体を解にもつ弱非線形レギュレータ問題の解析
- 制御量制約と終端拘束をもつ非線形最適制御問題の数値計算法
- ステートフェンス図 : リアクティブシステム設計のための一図式表現
- リアクティブシステム設計のためのグラフィカルな一表現法
- ステ-トフェンス図とバ-チャルオブジェクトを用いたシ-ケンス制御システムのソフトウエア開発手法
- ある階層型ニューラルネットワーク集合のコンパクト性とニューラルネットワークによるある最適制御の存在
- データ通信に用いるCATV網上り回線の雑音低減について(画像符号化・通信・ストリーム技術および一般)
- データ通信に用いるCATV網上り回線の雑音低減について
- データ通信に用いるCATV網上り回線の雑音低減について
- データ通信に用いるCATV網上り回線の雑音低減について
- M-062 無線端末位置推定法Gomashioの改良(ユビキタス・モバイルコンピューティング,一般論文)
- 信州大学インターネット大学院--e-ラーニング教材と学生について (特集 e-ラーニングの活用)
- 拡張ペトリネットとXMLをベースとしたファイルサーバの設計と実装
- 拡張ペトリネットとXMLをベースとしたファイルサーバの設計と実装
- CATVの上り回線の広帯域化に関する研究
- C-22 拡張ネットモデルによるNFSサーバプロセスの設計と動作の検証(ネットワークシステム,C.アーキテクチャ・ハードウェア)
- A-12-1 色付き論理ペトリネットを用いたNFSサーバプロセスのコンカレント設計
- 拡張ネットモデルによるNFSプロセスのモデル化とXMLを用いた実装
- (72)信州大学インターネット大学院の概要と今後の展望(第19セッション インターネット・マルチメティアの利用(I))
- 信州大学インターネット大学院の経緯と現状
- 弱非線形差分方程式の解を含む低次元多様体とレギュレータ問題
- 信州大学インターネット大学院計画について
- 信州大学バーチャル大学院計画について
- 弱非線形系H∞制御における中心多様体と状態フィードバック解
- Mamdani推論法の最適化問題への応用 (情報数理に関連する応用函数解析の研究)
- 時間に依存するファジィ集合族を用いた最適制御に関する一考察 (函数解析学の応用としての情報数理の研究)
- NBV空間のファジィ集合族のコンパクト性とファジィ制御への応用
- プルーフチェッカーを用いた論理演算器の設計検証
- 拡張ペトリネットを用いたNFSプロセスのモデル化と実装
- 拡張ネットモデルを用いたファイルサーバ設計による信頼性向上の一方策
- 拡張ネットモデルを用いたファイルサーバ設計による信頼性向上の一方策
- 1Z-5 ネットモデルと用いた自立分散型ファイルシステムのコンカレント設計
- Rechnungsmethod fur optimale Steuerungsprobleme mit Endzwang mittels Festpunkttheorems
- Mizarによる数論アルゴリズムの形式化と検証(一般,情報セキュリティ,ライフログ活用技術,ライフインテリジェンス,オフィス情報システム,一般)
- Mizarによる数論アルゴリズムの形式化と検証(一般,情報セキュリティ,ライフログ活用技術,ライフインテリジェンス,オフィス情報システム,一般)
- Center of Sums法による非ファジィ化計算の連続性とその応用(インタフェース技術と学習支援システム/一般)
- Mizar による数論アルゴリズムの形式化と検証
- Formal definition of probability on finite and discrete sample space for proving security of cryptographic systems using Mizar
- Formalization of Definitions and Theorems Related to an Elliptic Curve Over a Finite Prime Field by Using Mizar
- Mizarによる大学数学向け高度遠隔教育用コンテンツ開発(e-Learning運用/一般)
- 長距離無線LANと広域CATV通信網接続による山岳医療情報ネットワークの構築
- AT-2-2 定理証明系Mizarの概要(AT-2.情報理論のための形式的定理照明,ソサイエティ企画)