述語線形論理の自動証明器
スポンサーリンク
概要
- 論文の詳細を見る
線形論理(linear logic)は古典論理の中の一つの体系であるゲンツェンのLKから派生した体系と考えられる。線形論理の大きな特徴の一つはresource-conscious、すなわち数量概念を論理概念の中に含んでいることである。そして、これは古典論理の推論規則の中からweakeningとcontractionを除いた論理であると言うこともできる。
- 一般社団法人情報処理学会の論文
- 1996-03-06
著者
-
山口 文彦
慶應義塾大学大学院理工学研究科
-
三浦 泰介
慶應義塾大学大学院理工学研究科計算機科学専攻
-
中西 正和
慶應義塾大学 大学院理工学研究科
-
中西 正和
慶應義塾大学理工学部
-
中西 正和
慶應義塾大学
-
前田 敦司
筑波大学情報処理センター
-
米津 光浩
慶應義塾大学理工学研究科計算機科学科
-
前田 敦司
慶應義塾大学理工学部数理科学科
-
中西 正和
慶意義塾大学大学院理工学研究科
-
米津 光浩
慶應義塾大学大学院理工学研究科計算機科学専攻
関連論文
- 文字間統計情報に基づく口語文字列の自動抽出
- ニューラルネットワークを用いた複数楽器の音源同定処理
- 線形論理のある部分系上の帰納推論とその健全性および完全性
- PRMU2000-33 ニューラルネットワークによる6基本表情認識の規則発見
- 2000-NL-137-9 / 2000-SLP-31-4 日本語略語の自動復元
- 短期記憶を用いたシンプルリカレントネットワークによるカオス時系列の短期予測
- 区間確率密度を用いた不確かさを含む推論法 (テーマ 「オントロジー活用の実際、産業応用」および一般)
- 3G-2 キューを利用した並列計算モデル
- 3N-7 焼きなまし法を用いた対訳単語対抽出
- 3N-5 英語固有名詞のカナ表記への変換
- 1N-2 日本語文書における複合語キーワード抽出
- 4V-8 ウェーブレット信号空間における標本化関数の構成
- 音楽認識の評価方法に関する考察
- 5X-1 教育用日本語プログラミングシステムの構築
- 1N-1 数学的帰納法を用いる定理証明器の実装
- 音声と映像を用いたインタフェースの試作
- NGL法に基づいたリカレントニューラルネットワークの学習
- ニューラルネットワークによる失読症のモデル化
- 2000-MUS-36-12 リカレントニューラルネットワークを用いたコード進行の自動生成
- 短期記憶を用いたリカレントニューラルネットワークと高速な構造学習法
- Flow Graph解析を用いた並列関数型言語処理系の実装
- Logoのビジュアルモデルを用いた問題解決法のマイクロワールド
- 並列LISPシステムにおけるSpeculative Computationに関する研究
- 有理ベゼー曲線を応用した、CGアニメーションのための補間アルゴリズム
- X-Window上におけるLogoインタプリタの実現
- Xインタフェースを構築するための並列lisp処理系Momolisp
- Mach OS上における並列LispインタプリタNico Lispの実現
- 音楽自動演奏システムMIDI-98
- 明示的なα変換を用いたα単一化
- フラグメントの部分間差分を用いた例からのプログラム自動合成
- 高並列計算機EM-Xの性能モニタリングツール
- 神経グループ選択説に基づく学習システムに関する実験的考察
- 会話型FORTRAN : KEIOシステム
- 最大エントロピー法を用いた離散型共起表現の抽出
- 多義語の語義ベクトル分解
- 最大エントロピー法による対訳単語対の抽出
- 共起関係を利用した対訳コーパスからの連語の対訳表現抽出
- bigram 統計情報に基づくパージング
- d-bigram と他の統計情報との関連に関する実験
- 自然言語文評価におけるd-bigram 情報の活用方法に関する実験
- 自然言語における有繋文字列の抽出
- d-bigram 情報を用いた統語的規則の抽出
- 統計情報を用いた中国語における文単位一括変換法
- d-bigramを用いた中国語における文単位一括変換法
- d-bigramを用いた形態素解析
- d-bigramを用いた単語のクラスタリング
- d-bigramとtrigramの相関に関する実験
- d-bigramを用いた自然言語文評価に関する実験
- 強化学習における環境変化認識法
- 強化学習における環境変化認識法
- 通信手段を持つマルチエージェント系における強化学習
- 並列GCのポインタ通知数の削減による処理効率の向上
- 並列GCを備えた並列LispにおけるGCの抑制
- Lazy Reference Countを用いたLinear Lisp
- オブジェクトの世代を考慮に入れたインクリメンタルなごみ集め処理
- Snapshot型並列GCにおけるルート挿入時間の削減
- 会議システム
- オブジェクトの世代を考慮に入れた保守的ごみ集め
- ネットワーク対応オブジェクト指向Lispの処理系
- バイトコードインタプリタを用いたLispコンパイラシステム
- Lisp Serverにおけるシステムコールキャッシュ
- Micro Kernelの思想を採り入れたLisp Serverの設計
- 局所無矛盾性と距離コミットメントによる移動目標探索
- 印付け追跡法による移動目標探索
- 距離コミットメントによる移動目標探索
- ニューラルネットワークを用いた複数楽器の音源同定処理
- 2000-NL-137-9 / 2000-SLP-31-4 日本語略語の自動復元
- 分散並列関数型言語における動的なタスク粒度の選定手法
- 分散メモリ上の並列Lispへのストリーム通信の導入
- 並列ガーベジコレクションの効率改善の手法
- リスト処理におけるオブジェクトの生存率に関する解析
- リスト処理とGCのCPU割当てを動的に決定する並列Lisp
- オブジェクトの生存率の理論的解析に基づいた世代別ガーベッジコレクション
- 並列GCを備えた並列Lispシステムの実装および評価
- Adaptive Garbage Collection : 実装とその評価
- 部分印付けを併用した並列GCの提案および効率の解析
- 並列GCを備えた並列Lispシステム
- 参照カウンタ法を用いた並列ゴミ集め処理
- 相補型ガーベジコレクタ
- Adaptive Garbage Collectionの提案および実験
- Partial Marking GC
- LispマシンSYNAPSEの評価
- 対話音声認識における次発話予測の効果
- LISPマシンSYNAPSEのガーベッジ・コレクション・システムについて
- 5J-4 強化学習型マルチエージェント系における職能の分担の学習
- キューマシン方式並列実行の複数階層に渡る関数呼び出しフレームの併合による効率化
- キューマシン方式による並列Lisp処理系のスケジューリング手法
- ISLisp言語処理系のバイトコードインタプリタの実装
- 述語線形論理の自動証明器
- 文字の共起情報のみを利用した文字列抽出
- 実時間ゴミ集めにおけるルート挿入の効率化
- MELLの証明に要する計算の複雑さ
- AICを用いたデフォルトルール生成法の拡張
- 行動選択ネットワークによるマルチエージェントの適応学習
- LVQとHMMを用いた音楽コード認識システムの実装
- RTAとExplorationを導入した移動目標探索
- プロセス仕様の模倣関係検証
- プロセス等価性の自動証明器の実装
- 線形論理における帰納推論
- フラグメントの部分間差分を用いた例からのLISP関数の自動合成