部分例示に基づく定理自動証明
スポンサーリンク
概要
- 論文の詳細を見る
定理自動証明に対するこれまでの研究として,1965年にRobinsonによって提案された導出原理に基づくさまざまな方法,戦略などが提案されており,現在の定理証明システムの多くはこの導出原理に基づいている.これに対して,Jeroslowは1988年に部分例示手法を提案している.しかしながら,Jeroslowの提案した方法は関数記号を含まない論理式のみを対象としていること,また,節形式を前提としていないために効率が悪いことなどの欠点があった.筆者らはこのこのJeroslowの方法を改善して,関数記号を含まない節形式の論理式の充足可能性を判定する手続きを提案して,その有効性を示している.本論文では,この手続きを拡張した定理証明手続きを提案する.すなわち,関数記号を含む論理式を扱えるようにしている.また,本手続きが完全であることの証明を与える.更に,比較実験を行い本手続きの有効性について検討する.
- 社団法人電子情報通信学会の論文
- 1995-07-25
著者
-
山本 雅人
北海道大学大学院情報科学研究科
-
大内 東
北海道大学大学院情報科学研究科
-
大柳 俊夫
札幌医科大学保健医療学部一般教育科
-
大柳 俊夫
札幌医科大学保健医療学部
-
大柳 俊夫
札幌医科大学 医療人育成センター 教養教育研究部門
-
大内 東
北海道大学 大学院 情報科学研究科 複合情報学専攻 複雑系工学講座 調和系工学研究室
-
山本 雅人
北海道大学
関連論文
- 2 観光情報学(新しい○○情報学)
- 小型自律飛行船シミュレーションの実装及び効果検証
- 数理モデルによるDNAメモリの容量解析
- スケールフリーネットワークの生成方法およびベキ指数が結合振動子ネットワークの同期へ与える影響
- F-056 ネットワーク間狭小性によるネットワークの時系列解析(人工知能・ゲーム,一般論文)
- 5C-1 ノード間関係の類似度を定量化するネットワーク間狭小性(複雑系,一般セッション,人工知能と認知科学)
- LF-006 セルの入出力観測に基づくセルオートマトンの定量的分析(人工知能・ゲーム)
- ブログによる情報収集と推薦技術を用いた飲食店情報サイトの構築(セッション7:ウェブにおける情報処理)
- ブログによる情報収集と推薦技術を用いた飲食店情報サイトの構築(セッション7:ウェブにおける情報処理,社会システムと知能)
- 集合行為問題におけるタグメカニズムと協調の形成に関する考察
- Davis-Putnam の手続きにおける分枝変数選択規則の提案
- 観光情報学
- 自律的行動獲得に基づく仮想ロボットの開発
- 円環構造型モジュラーロボットの自律移動行動の獲得
- 動的信号領域を用いたSOMによるネットワークの可視化
- 3B-4 自己組織化を利用したネットワーク可視化の評価と比較(アルゴリズムとその応用,一般セッション,ソフトウェア科学・工学)
- 3B-2 Modularityを用いた複雑ネットワークの成長と構築に関する研究(アルゴリズムとその応用,一般セッション,ソフトウェア科学・工学)
- 2B-5 個人の特性と話題を考慮した情報伝播モデルの研究(数理モデル化と問題解決,一般セッション,ソフトウェア科学・工学)
- 観光情報学会誌にみる国内研究動向
- 2-S-5 観光情報学会誌にみる国内研究動向(観光とOR(1))
- 時間制約付き飛行プランに基づく小型自律飛行船制御
- F-054 ネットワークモデルを用いた異なるカテゴリ間の嗜好性の解析(人工知能・ゲーム,一般論文)
- F-053 二部グラフにおけるクラスタリングアルゴリズムの比較(人工知能・ゲーム,一般論文)
- 5B-8 異なるカテゴリの嗜好情報に対する特徴解析及び評価(コンテンツ推薦,一般セッション,データベースとメディア)
- 6A-4 評判伝播ネットワークの成長モデルに関する基礎研究(グラフとネットワーク,一般セッション,ソフトウェア科学・工学)
- 6A-3 自己組織化を利用したネットワークの三次元可視化(グラフとネットワーク,一般セッション,ソフトウェア科学・工学)
- ノード特性とコミュニティ情報を考慮したシナジーテックなネットワーク成長モデル
- コミュニティ情報を考慮したネットワーク成長モデル
- ネットワーク構造の局所エネルギー最小化による可視化の高速化
- 局所クラスタリング組織化法による配送路問題の解法
- ノード特性とコミュニティ情報を考慮したシナジーテックなネットワーク成長モデル
- 郡市医師会情報化実態指標の構築
- 最適系列分割問題への遺伝的アルゴリズムの適用 : 個体の形質遺伝に関する考察
- 2T05 ゲノム情報処理におけるコピーパターンの抽出と解析
- 2T03 同時双方向探索によるアミノ酸配列の多重アラインメント
- 遺伝情報の統合処理支援モジュールの構築
- 総合成績を考慮したクラス編成法に関する一考察
- 強化学習を用いた小型飛行船の目標位置への誘導
- F-007 ブログを用いたWebサービス型情報共有・推薦システム「HARMO」の開発(F分野:人工知能・ゲーム)
- 状態遷移量に基づく屋内小型自律飛行船の動作設計に関する検討
- 小型自律飛行船の研究プラットホームの実現
- J_050 充電地点へのドッキングを行なう室内バルーンロボットの学習制御(J分野:グラフィクス・画像)
- 室内バルーンロボットにおける自律充電のドッキング制御(エンタテインメントコンピューティング一般(1))
- 2P1-S-059 超音波センサを搭載した室内バルーンロボットにおけるトポロジカルマップの自動生成(飛行ロボット4,生活を支援するロボメカ技術のメガインテグレーション)
- 1P1-S-060 T-Engineシステムを搭載した室内用バルーンロボットの開発と飛行制御(飛行ロボット1,生活を支援するロボメカ技術のメガインテグレーション)
- ホバリング制御に基づくエンタテインメントバルーンロボットの開発(エンタテインメントコンピューティング)
- カメラ搭載型バルーンロボットシステムの開発とPD制御による位置制御の実現(応用分野・領域)
- 人工市場研究の為のX-Economyシステムの開発と実装(情報・経済)
- X-Economyサーバによる仮想金融市場の設計と開発
- X-Economyサーバによる仮想金融市場の設計と開発
- 多目的評価関数を持つエージェント群の集団的挙動
- 6A-2 局所エネルギー最小可視化によるネットワークの大域的可視化(アルゴリズム,一般セッション,ソフトウェア科学・工学,情報処理学会創立50周年記念)
- F-031 複雑ネットワークの特徴量に基づくHexゲーム戦略の解析(F分野:人工知能・ゲーム,一般論文)
- 5D-6 Webタグの階層的クラスタリング手法の提案(自然言語処理(2),一般セッション,人工知能と認知科学,情報処理学会創立50周年記念)
- 6A-4 コミュニティ構造の影響を考慮したネットワーク成長モデルの提案(アルゴリズム,一般セッション,ソフトウェア科学・工学,情報処理学会創立50周年記念)
- 6A-3 振動子ネットワークからみた同期現象におけるネットワーク構造の変化(アルゴリズム,一般セッション,ソフトウェア科学・工学,情報処理学会創立50周年記念)
- コミュニティ情報を考慮したネットワーク成長モデル
- 327 複合環境に於ける人工生物モデルの行動獲得
- 326 ダ・ヴィンチのヘリコプターは飛ぶか?
- 325 Animated Robotの研究 : 人工生物の遊泳獲得とその挙動解析
- 324 仮想空気環境における安定飛翔行動の獲得
- 323 アニボットの協調行動の獲得
- A-002 観光経路作成支援における代替観光経路の提案手法(A分野:モデル・アルゴリズム・プログラミング)
- 遺伝的アルゴリズムによる最適系列分割問題の解法
- GPSログからの周遊型観光行動情報の抽出(「ネットワークデータマイニング」「センサデータマイニング」)
- GPSログからの周遊型観光行動情報の抽出(「ネットワークデータマイニング」「センサデータマイニング」)
- GPSログマイニングに基づく観光動態情報の獲得
- 観光動態情報の獲得を意図したGPSログデータマイニング(社会システムにおける知能 : 社会システムのモデル化)
- 観光動態情報の獲得を意図したGPSログデータマイニング(社会システムにおける知能(社会システムのモデル化))(「社会システムにおける知能」及び一般)
- 表情識別に対するMTS法の適用
- 撮影変動にロバストな顔同定システムの実現
- 集合行為問題におけるタグメカニズムと協調の形成に関する考察
- 適応的ハイパーゲームによる市場取引のモデル化と構造分析
- 適応的ハイパーゲームによる市場取引のモデル化と構造分析
- 要介護度一次判定アルゴリズムに関する基礎研究
- 317 物理モデリングを利用した直列多重倒立振子の振り上げ制御
- 宿泊施設の公式ホームページ収集システム(9月15日)(「アクティブマイニング」及び一般)
- 宿泊施設の公式ホームページ収集システム(「アクティブマイニング」及び一般)
- 319 Animated Robotの研究 : 多脚人工生物の行動獲得
- 人工蟻の餌争奪ゲームにおけるフェロモンコミュニケーションの進化的獲得
- H_019 DNAを用いたタイル構造における接着結合部の塩基配列設計(H分野:生体情報科学)
- H-032 自由エネルギーに基づいた塩基配列設計に関する研究(H分野:生体情報科学)
- H-031 自由エネルギーを用いたDNAナノ構造のための塩基配列設計(H分野:生体情報科学)
- H-030 DNAを記憶素子として用いた分子メモリの開発と大容量化に関する検討(H分野:生体情報科学)
- A-010 DNA分子を利用したリレーショナルデータベースの開発(A分野:モデル・アルゴリズム・プログラミング)
- 318 進化的手法を用いた仮想モジュラーロボットの適応行動の獲得
- 242 ネットワーク構造の変化が振動子の挙動に与える影響
- Webサイトの自動分類に向けた特徴分析とキーワード抽出に関する研究(「ネットワークデータマイニング」「センサデータマイニング」)
- Webサイトの自動分類に向けた特徴分析とキーワード抽出に関する研究(「ネットワークデータマイニング」「センサデータマイニング」)
- マルチエージェント分析による顧客主導予約調整メカニズムの有効性の検証(社会システムにおける知能 : エージェントと社会基盤)
- マルチエージェントシステムにおける相互作用の定量的分析法に関する基礎研究(一般 : マルチエージェントと学習)
- マルチエージェント分析による顧客主導予約調整メカニズムの有効性の検証(社会システムにおける知能(エージェントと社会基盤))(「社会システムにおける知能」及び一般)
- マルチエージェントシステムにおける相互作用の定量的分析法に関する基礎研究(一般(マルチエージェントと学習))(「社会システムにおける知能」及び一般)
- 大規模物流センターにおけるオーダーピッキングのナビゲーションスケジューリングに関する研究
- 命題論理充足可能性問題に対する定量的アプローチと記号的アプローチの比較
- Animated Robotの研究 : —剛体モデリングツールの開発とその応用—
- 宿泊施設の分類システムと自己評価 (特集 観光と知能情報)
- β節充足可能性問題の解法についての考察
- 部分例示に基づく定理自動証明
- β節集合に対するDavis-Putnamの手続きの一般化