信念様相論理に対する様相節変換型証明器の実現
スポンサーリンク
概要
- 論文の詳細を見る
信念様相論理(KD45多重様相論理)の証明法として,論理式を一階述語論理式に変換し,可能世界間の到達可能関係を単一化によって計算する関数模擬(Functional Simulation)法が提案されている.しかし,この方法には,証明に直接寄与しない探索を行うという問題点があった.一方,様相体系Kの論理式を,証明に直接寄与しない不要な探索を抑制するように,領域限定された節集合に変換し,モデル生成型定理証明器MGTPを用いて証明する様相節変換法が提案されている.そこで本稿では,関数模擬法に基づいて可能世界間の到達可能関係を照合によって計算し,様相節変換法をKD45多重様相論理に拡張することを提案する.
- 一般社団法人情報処理学会の論文
- 1994-01-19
著者
-
赤埴 淳一
日本電信電話株式会社NTTネットワークサービスシステム研究所
-
赤埴 淳一
Nttコミュニケーション科学基礎研究所
-
長谷川 隆三
新世代コンピュータ技術開発機構
-
井上 克巳
豊橋技術科学大学情報工学系
関連論文
- Service Delivery Platformを用いたビル警報通知連携システムの開発(変革を続けるネットワークソフトウェア技術論文)
- Web-テレコム連携プログラミングのためのSDKの提案と生産性評価(変革を続けるネットワークソフトウェア技術論文)
- Web情報からのメディア特徴量分類によるメタデータ抽出手法(テーマセッション,映像ハンドリング技術とその応用)
- 将来ネットワークにおける個人IDを用いた通信方式の検討(次世代・新世代ネットワークアーキテクチャ,トラヒック計測・制御,サービス品質,ネットワーク管理,一般)
- 実世界指向情報統合に向けて
- 個人の推薦に基づく個人間情報共有モデル
- オントロジを利用した会話理解手法の提案(自然言語情報処理研究会と一部合同開催 : NL・SLP合同開催 : 音声対話1)
- オントロジを利用した会話理解手法の提案
- R&Dホットコーナー セマンティックWebの動向と近似オントロジ変換の考案
- 歩行者ナビゲーションにおける情報伝達の利用者適応の分析
- セマンティックデスクトップに基づくコンテンツ管理システムの検討 (ネットワークシステム)
- Web-テレコム連携プログラミングのためのSDKの提案と生産性評価
- Service Delivery Platform を用いたビル警報通知連携システムの開発
- B-19-4 SVMを利用したHTTPフローからのWebサイトへの書込み行為抽出方法に関する一検討(B-19.ネットワークソフトウェア,一般セッション)
- セマンティックデスクトップに基づくコンテンツ管理システムの検討(モバイル,アドホック,ユビキタス,無線,セキュリティ,マルチアクセス,アクセスネットワーク・User Network Interface,Homeネットワーク,一般)
- ICカードを用いた個人ID通信方式の検討(モバイル,アドホック,ユビキタス,無線,セキュリティ,マルチアクセス,アクセスネットワーク・User Network Interface,Homeネットワーク,一般)
- B-19-13 SDKの利用によるParlay Xアプリケーション作成時の生産性に関する一考察(B-19.ネットワークソフトウェア,一般セッション)
- B-19-3 嗜好情報解析のためのトラフィックフィルタリングに関する一検討(B-19.ネットワークソフトウェア,一般セッション)
- B-19-7 複数Webクライアントの余剰リソース活用手法(B-19.ネットワークソフトウェア,一般セッション)
- B-7-24 嗜好情報解析のためのトラフィック抽出方法に関する一検討(B-7.情報ネットワーク,一般セッション)
- BS-2-2 ノードの役割に基づく仮想ネットワークでのリソース割当ての検討(BS-2.次世代クラウド基盤の実現へ向けたネットワーク制御・管理技術,シンポジウムセッション)
- B-6-30 将来NWに向けたセキュアでパーソナルな通信の検討課題と方向性(B-6.ネットワークシステム,一般セッション)
- 実世界指向情報統合に向けて
- B-19-2 確率的Counting Bloom Filterによる頻出データ識別システムに関する一検討(B-19.ネットワークソフトウェア,一般セッション)
- B-19-1 ライフログサービスのためのネットワークフロー分析プラットフォームに関する一検討(B-19.ネットワークソフトウェア,一般セッション)
- B-19-17 ストリーム処理における動的行動情報抽出方法に関する一検討(B-19.ネットワークソフトウェア,一般セッション)
- B-19-8 HTTPフローからのブログ書込み行為の抽出方法に関する一検討(B-19.ネットワークソフトウェア,一般セッション)
- B-19-14 協調フィルタリングを用いたソーシャルグラフの作成方法に関する一考察(B-19.ネットワークソフトウェア,一般セッション)
- B-7-81 仮想ネットワークにおける動的ノード機能配備手法の検討(B-7.情報ネットワーク,一般セッション)
- B-19-9 時間情報を考慮したスケジュール情報からのユーザー行動特性抽出の検討(B-19.ネットワークソフトウェア,一般セッション)
- B-19-5 遠隔利用のためのコンテンツ情報管理に関する一検討(B-19.ネットワークソフトウェア,一般セッション)
- B-14-18 対話型WebアプリケーションWebAPI化手法(B-14.情報通信マネジメント,一般セッション)
- デジタルシティにおける情報検索のための地図インタフェース(:インターネット応用システムの構築と運用管理)
- コミュニケーション科学技術の新領域開拓活動--ディジタルシティの研究 (特集 NTTにおけるオープン・ラボ活動)
- WWW・実時間センサ情報のための統合によるデジタルシティ京都の構築
- B-19-6 スループット向上のための静的及び動的コア割り当て手法に関する一検討(B-19.ネットワークソフトウェア,一般セッション)
- B-6-55 動的なネットワーク機能配備方式の検討(B-6.ネットワークシステム,一般セッション)
- B-19-2 多段ステージスレッドプールを利用した呼処理アーキテクチャに関する一検討(B-19.ネットワークソフトウェア,一般セッション)
- L-016 複数のWebクライアントの余剰リソース活用システムの実装と評価(L分野:ネットワーク・セキュリティ,一般論文)
- B-19-5 セッション制御サーバの呼処理シーケンス並列化に関する一検討(B-19.ネットワークソフトウェア,一般セッション)
- B-19-3 Webサーバアーキテクチャの呼処理サーバへの適用に関する一検討(B-19.ネットワークソフトウェア,一般セッション)
- B-19-18 ユーザ状況推定に用いるベイジアンネットワーク構築法の提案(B-19.ネットワークソフトウェア,一般セッション)
- Web情報からのメディア特徴量分類によるメタデータ抽出手法(テーマセッション,映像ハンドリング技術とその応用)
- Web情報からのメディア特徴量分類によるメタデータ抽出手法(テーマセッション,映像ハンドリング技術とその応用)
- 実世界セマンティックWebに向けて--時空間メタデータによるWeb検索の拡張 (特集 メタデータ応用サービスおよび関連技術の動向)
- PIM上の並列定理証明系MGTP
- ブロードバンド社会におけるセマンティックウェブ技術の展望
- D-19 移動軌跡データに対する類似度検索手法(データ編成と高速化,D.データベース)
- D-18 移動軌跡データモデルと領域に基づく問合せ処理(データ編成と高速化,D.データベース)
- 歩行者ナビゲーションにおける情報伝達の利用者適応の分析
- ディジタルシティ
- 様相節変換に基づくボトムアップ型様相論理証明法
- 信念様相論理に対する様相節変換型証明器の実現
- 様相節変換に基づくMGTP上の様相論理証明器の効率的実現
- BS-4-1 将来ネットワークに向けた既存網の課題と解決手段に関する一検討(BS-4.固定・移動融合時代の全IP次世代ネットワーク技術の検討課題とその解決手法,シンポジウムセッション)
- モデル生成型定理証明器を用いたアブダクションの計算における効率化手法
- モデル生成に基づく並列アブダクション
- モデル生成に基づく並列アブダクション
- B-6-56 柔軟な運用を可能とする通信ノードハードウェア構成法の一検討(B-6.ネットワークシステム,一般セッション)
- D-9-26 企業内情報を活用した文書ファイルへのメタデータ自動付与手法の提案(D-9.ライフインテリジェンスとオフィス情報システム,一般セッション)
- B-6-67 将来ネットワークにおけるセキュアでパーソナルな通信技術の一検討(B-6.ネットワークシステム,一般セッション)
- 上昇型定理証明の探索効率を高めるノンホーン・マジックセット
- D-9-30 企業内における情報共有の実践とその活用 : 利用組織拡大による特徴的な活用状況の分析と評価(D-9.ライフインテリジェンスとオフィス情報システム,一般セッション)
- Webアプリケーションユーザの利用を妨げないWebブラウザの余剰リソース活用手法(データ工学,Web情報システム,サイバーワールド論文)
- アクション言語Αのためのオートマトン理論
- 定理証明器PTTPにおける対偶節生成の削減効果
- アクション言語Aを表現するオートマトンモデル
- アブダクションを用いた逐次的な自然言語理解モデル
- HTTPフローからのWebサイトへの情報発信型書込み行為判別手法(人・社会を支えるネットワークソフトウェア技術とその応用論文)
- ナレッジ活用のための機械学習による変遷情報の意味論的統合(「コンテキストを意識した知識の利用」及び一般)
- IaaS型パブリッククラウド管理APIの調査比較
- HTTPフローからの Web サイトへの情報発信型書込み行為判別手法
- タスクに着目した企業内情報へのメタデータ付与手法(LOD,メタデータ,ライフログ活用技術,オフィスインフォメーションシステム,ライフインテリジェンス,一般)