証明支援系の図式によるインターフェイス (<特集> インタラクティブソフトウェア)
スポンサーリンク
概要
- 論文の詳細を見る
我々は図式による証明支援系のインターフェイスを設計している.本稿ではその概念設計について説明する.圏論などの代数では証明をわかりやすくするため可換図がよく用いられる.この仕組みを形式的証明にも用いようと我々は考えた.そこで形式的証明には論理式を用い,ユーザへの表示には図式を用いる証明支援系を設計した.このようなインターフェイスを持つ証明支援システムは著者の知る限りなかった.証明支援系は命題の入力と証明の実行という二つの機能を持つが,我々はその両方とも図式上の操作として実現しようと考えた.
- 日本ソフトウェア科学会の論文
- 1997-05-15
著者
-
木下 佳樹
産業技術総合研究所
-
木下 佳樹
(独)産業技術総合研究所 組込みシステム技術連携研究体
-
高橋 孝一
産業技術総合研究所
-
中田 秀基
電子技術総合研究所
-
高橋 孝一
電子技術総合研究所
-
中田 秀基
電総研
-
木下 佳樹
電子技術総合研究所
-
木下 佳樹
独立行政法人産業技術総合研究所情報処理研究部門情報科学連携研究体
-
高橋 孝一
産業技術総合研究所システム検証研究センター
-
木下 佳樹
産業技術総合研究所システム検証研究センター
関連論文
- 第1回 記述とは(記述の科学)
- 第2回 視点と形式的体系(記述の科学)
- 複数拠点にまたがるe-Scienceアプリケーション環境構築を目的としたソフトウェア導入・管理機構(並列・分散システム,システム開発論文)
- 第3回 記述の構成と利用(記述の科学)
- 形式モデルに基づくディペンダビリティのアセスメントプロセスの設計
- 複数ドメイン環境でQoSを保証するクラウドのための資源管理フレームワーク(クラウド、グリッド・P2P)
- ネットワーク帯域予約を用いた分散アプリケーション実行環境の構築(クラウド、グリッド・P2P)
- 臨床情報学のための野外科学的方法--技術移転の方法論に向けて
- モデル検査によるシステム検証(「信頼性・保全性・安全性の事例:情報処理・ソフトウェア編」〜信頼性ハンドブック出版から10年を経て〜)
- 並列ごみ集めの抽象モデル検査の形式的証明
- BDDを用いた同期アルゴリズムの探索
- モデル検査系を用いたプログラム発見(「定理証明, 推論関係の新技術」)
- 正則表現を用いた並列ごみ集めの抽象モデル検査
- Javaによるソフトウェア分散共有メモリシステムの構築
- Java向けソフトウェア分散共有メモリの実現
- 2000-HPC-81-13 Network Enabled Server System の設計
- 2000-HPC-81-11 Jiniを用いたComputing Portal Systemの開発
- グローバルコンピューティングのスケジューリングのための性能評価システム(並列処理)
- グローバルコンピューティングのためのスケジューリングフレームワーク(並列処理)
- クライアント・サーバ型のグローバルコンピューティングシステムの比較 : Ninf, NetSolve, CORBA, Ninf-on-Globusの性能評価
- グローバルコンピューティングシステムNinfを用いた数値流体解析コンポーネントnetCFD
- Javaによる大域的並列計算環境Ninflet (並列処理)
- グローバルコンピューティングシステムのシミュレーションによる評価 (並列処理)
- Ninfによる遠隔計算資源アクセスシステムの構築とグローバルコンピューティングシステムの性能評価
- グローバルコンピューティングシミュレータの概要
- 広域計算システムNinfにおけるユーザ認証
- Ninfシステムにおけるジョブスケジューラの実装と予備的評価
- 複数クライアントによるLAN/WANでのNinfの性能(並列処理)
- Ninfによる広域分散並列計算(並列処理)
- 高性能広域計算システムNinfのスケジューリングに関する予備的考察
- Ninfによる広域分散並列計算
- ネットワーク数値情報システムNinf : マルチクライアント環境での性能
- ネットワーク数値情報ライブラリ : Ninfを用いた数値計算環境システムの開発 : NinfCalcの試作
- 分散メモリ計算機用Ninf APIの実現に向けて
- ネットワーク数値情報ライブラリNinf : システム実装と評価
- Parallel STLによる並列プログラミング
- ネットワーク数値ライブラリNinfにおけるメタサーバアーキテクチャ
- 2.Googleのクラウド技術(クラウドの事例紹介,クラウドコンピューティング)
- 既存VMMへの適用が容易でゲスト透過なポストコピー型仮想マシン再配置機構
- 高速マイグレーションを利用した仮想マシン配置最適化システムの検討
- 高速フラッシュメモリに適したキーバリューストアの予備的評価
- 性能を保証する分散実行環境のためのオンラインコアロケーション手法
- クラウドコンピューティングの性能評価
- クラウドコンピューティングの性能評価
- 高速フラッシュメモリ向けMapReduceフレームワークの実現に向けて
- ファイアウォールに対応したGlobusによる広域クラスタシステムの構築とその評価
- 2000-HPC-81-12 Firewellに対応したGlobusによる広域クラスタシステムの構築と性能評価
- GlobusにおけるResource Managerの試作 : グローバルコンピューティング環境の構築に向けて
- 証明支援系の図式によるインターフェイス ( インタラクティブソフトウェア)
- Stepwise Synthesis of Partial Specifications preserving Strong $(\Omega_1,\Omega_2)$-Equivalence(Concurrency Theory and Applications '96)
- 仮想計算機パッキングへの最適化手法の適用(2010年並列/分散/協調処理に関する『金沢』サマー・ワークショップSWoPP2010)
- 仮想計算機メモリの遅延再配置による高速ライブマイグレーション
- Mealyオートマトンのスーパバイザ制御の余代数による解析(コンカレントシステム,離散事象システム及び一般)
- Ninfによる遠隔計算資源アクセスシステムの構築とグローバルコンピューティングシステムの性能評価
- Ninfによる遠隔計算資源アクセスシステムの構築とグローバルコンピューティングシステムの性能評価
- 部分観測Mealyオートマトンのスーパバイザ制御の余代数による解析 (コンカレント工学)
- 大規模資源の管理・制御に関する技術の実証実験 : 新世代ネットワークプラットフォームの実現に向けて(ネットワーク品質,トラヒック計測,サービス品質,一般)
- 並列計算機PIE64における Committed-choice型言語Flengの負荷分散手法
- Committed-Choice型言語Flengにおける静的負荷分割のPIE64上での実装および評価
- ゴールの融合によるCommitted-Choice型言語Flengの最適化
- PIE64におけるCommitted-Choice型言語flengの動的粒度制御のためのコンパイル手法
- flengの動的粒度制御のための静的解析手法
- データフロー解析に基づくCommitted-Choice型言語Flengの静的負荷分割
- データフロー解闘斤に基づくCommitted Choice型言語のスヶジューリング
- 高並列推論エンジンPIE64研究経過報告 : ソフトウェア
- Committed-Choice型言語へのオブジェクトの導入
- グローバルコンピューティングシミュレータの概要
- BDDを用いた2方向CTL論理式充足可能性決定手続きの実装(サイバー増大ページ論文概要,サイバー増大号)
- 束縛関係に基づく認証プロトコルの検証(セキュアコンピューティング)
- 標数2のある体上の代数方程式の求解
- ネットワーク計算用行列工房 : Matrix Workshopによる性能評価システム
- 2. フォーマルメソッドのフィールドワーク(Part II:産業界への応用,フォーマルメソッドの新潮流)
- 動的ネットワークパスプロビジョニングの相互運用技術 : G-lambdaシステムとGLIF Feniusの連携(ネットワーク管理/制御/設計)
- テスト付きクリーニ代数の準代数構造
- B-3 連を用いたwhileプログラムの意味論(プログラムの理論,B.ソフトウェア)
- 合成ベンチマークによるMapReduce処理系SSSの性能評価
- 合成ベンチマークによるMapReduceのI/O性能評価手法
- クヌース・ベンディクスの代りに米田 : モノイドの場合
- ファイブレーションに基づく論理プログラムの意味論
- プログラミング言語ML
- 林 晋 著, "数理論理学", コンピュータ数学シリーズ3, コロナ社, A5判, 177p., \2,060, 1989
- 多種資源を対象とするオンラインコアロケーション手法の提案
- グラフ探索アルゴリズムの形式的検証とモデル検査への応用について (プログラム変換と記号・数式処理)
- Condor VM ユニバースを利用した HPC Cloud の試作
- Javaのクラスローダ制約の定式化
- クラウドを利用した電力可視化システムの構築
- クラウドを利用した電力可視化システムの構築
- 部分観測Mealyオートマトンのスーパバイザ制御の余代数による解析(一般,コンカレントシステム及び一般)
- システム検証における数理的手法の紹介 : 組込みシステムへの適用事例(組込みシステム特集号)
- 産業技術総合研究所関西センターだより(26)機能安全とソフトウェア認証
- ソフトウェアの複雑さ (特集 複雑系モデルと情報処理--21世紀の科学)
- 特集「システム検証の科学技術」の編集にあたって(システム検証の科学技術)
- 作譜科学の現状と将来--心配のないソフトウェア開発に向けて
- 特集「続・システム検証の科学技術」の編集にあたって(サイバー増大号)
- 特集「システム検証の科学技術」の編集にあたって
- 産総研システム検証研究センター紹介
- 帰納と再帰 : 表示的意味論の第一歩
- Do the right things
- 制御システムセキュリティのためのセキュリティバリアデバイスの提案
- 制御システムセキュリティのためのセキュリティバリアデバイスの提案