様相節変換に基づくボトムアップ型様相論理証明法
スポンサーリンク
概要
- 論文の詳細を見る
様相論理の高速な定理証明器の実現方法として,証明すべき様相論理式をモデル生成型定理証明器MGTPの入力節に変換する様相節変換方式を提案する.本方式は,様相論理の標準的な証明法である様相タブロー法の書換え規則の部分計算に基づいている.本方式の特徴は,書換え規則の適用を遅延するように変換することによって,証明に無関係な分枝の生成を抑制する点にある.本稿では,まず,生成される分枝数を削減するために,閉条件のテストを前件の照合に変換する方式を述べる.さらにゴール情報を利用し,トップダウン推論を模擬するように変換することによって,高速化を図る.様相節変換のコストが入力論理式長に関して線形であることを示し,計算機実験によって本方式の有用性を示す.
- 一般社団法人情報処理学会の論文
- 1995-04-15
著者
-
赤埴 淳一
日本電信電話株式会社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,メタデータ,ライフログ活用技術,オフィスインフォメーションシステム,ライフインテリジェンス,一般)