等式論理系における制約解消による証明支援環境構築の試み
スポンサーリンク
概要
- 論文の詳細を見る
等式論理を基盤とする仕様記述言語では, 仕様は項書換え系による操作的意味を持つため簡約手続きによる実行が可能であり, この実行機構を通して仕様の検証が行なわれる。私達は形式的記述(仕様および検証記述)に自然言語等による説明を加えた拡張されたHTML: Forsdonnet (Formal specification document on network)の文章を対象とし, 形式的記述間の制約の記述と, 簡約手続き, 帰納的証明等の実行機能による制約解消を繰り返すことで, ユーザが対話的に仕様の検証を行う環境を構築した。以下でその説明を行う。
- 一般社団法人情報処理学会の論文
- 1997-09-24
著者
-
石黒 正揮
株式会社三菱総合研究所
-
井上 直
情報処理振興事業協会
-
井上 直
情報処理振興事業協会(ipa)
-
中川 中
(株)SRAソフトウエアエ学研究所
-
中川 中
情報処理振興事業協会(IPA)技術センター
-
石黒 正揮
三菱総合研究所
関連論文
- ウインターワークショップ2010・イン・倉敷開催報告
- インターネット上の脅威分析を支援する空間および時間的な特徴量に基づく分析手法(侵入検出・検知,情報システムを支えるコンピュータセキュリティ技術の再考)
- ウインターワークショップ2010・イン・倉敷開催報告
- ウインターワークショップ2010・イン・倉敷開催報告
- 項書換え系に基づく定理証明支援環境の構築
- 代数仕様言語CafeOBJのパラメータ化機構
- 実行可能な形式仕様言語CafeOBJ(4) : CafeOBJによるZ仕様のアニメーションの枠組み
- 実行可能な形式仕様言語cafeOBJ(3) : CafeOBJによるオブジェクト指向システムの仕様記述ライブラリの記述
- 実行可能な形式仕様言語CafeOBJ(2) : Cafeシステムの核アーキテクチャ
- 実行可能な形式仕様言語CafeOBJ(1) : CafeOBJの宣言的意味論
- ダイナミックCT造影像の経時変化に基づく肝腫瘍自動診断手法
- 画素密度分布のエントロピー最小化に基づく肝CT画像のセグメンテーション手法
- 肝CT画像の陰影経時変化パターンに基づく腫瘍良悪性判別手法の検討
- CafeOBJによるプロセス記述ライブラリの作成
- 肝CT造影像の経時変化に基づく類似画像検索システムの開発(レジストレーション・イメージマッチング)(関連学会との共催によるバイオメディカルイメージング連合フォーラム)
- セグメント特徴量に対する機械学習を用いた肝癌画像判別手法
- 等式論理系における制約解消による証明支援環境構築の試み
- LLPシステムによる観測データの統計解析手法の検討
- 等式論理系における制約解消による証明記述の枠組み
- 不正侵入の痕跡と判別分析によるリモートアタックの検出法
- 不正侵入の痕跡と判別分析によるリモートアタックの検出法
- 必須アクセス制御方式を用いた侵入検出システム保護機能(21世紀のコンピュータセキュリティ技術)
- 2000-CSEC-10-26 侵入検出システムにおけるセキュリティ機能の検討
- ISEC2000-48 侵入検出システムにおけるセキュリティ機能の検討
- ウィンターワークショップ2011・イン・修善寺開催報告
- 代数的仕様記述言語CafeOBJ