定理証明器SATCHMOREの効率化に関する一手法
スポンサーリンク
概要
- 論文の詳細を見る
本稿では, 定理証明器SATCHMOREに有効性の概念を組み込んだΑ-SATCHMOREを提案する. 前向き推論に用いる非ホーン節を選ぶ基準として「関連性」の概念を導入したSATCHMOREが提案されている. しかし, 実際には証明に貢献しないアトムも関連があるとしてしまうことにより, 探索空間の爆発を起こしてしまうこともある. そこで, Α-SATCHMOREでは, 関連のあるアトムの中でも, さらに証明に有効であるもののみに注目し, 証明に用いる非ホーン節をさらに制限することによって探索空間を絞りこんでいる. また, 本方法に基づく定理証明器を計算機上に実装し, 実験を行い効果を確認した.
- 一般社団法人情報処理学会の論文
- 1997-03-15
著者
-
伊藤 英則
名古屋工業大学大学院工学研究科情報工学専攻
-
世木 博久
名古屋工業大学
-
島尻 優香
名古屋工業大学工学部知能情報システム学科
-
島尻 優香
名古屋工業大学 知能情報システム学科
-
伊藤 英則
名古屋工業大学知能情報システム学科
-
巣 宇燕
名古屋大学 人間文化情報学工学研究科
-
何 立風
名古屋工業大学
-
伊藤 英則
名古屋工業大学
-
何 立風
愛知県立大学情報科学研究科
関連論文
- 結び目、自己相似などを用いたグラフィック処理について
- Simple Recurrent Network を用いた感性ロボットのインタラクティブ表情表出
- 関節制御の動的受動化とCPGに基づく二足ロボットの歩容生成
- 感性ロボット ifbot の感情空間を用いた感情遷移に伴う表情変化の主観的影響
- セルフキャリブレーションとNN学習によるカラーテクスチャ物体のレンダリング(一般セッション,光と色の解析・表現とその応用)
- 同調・差別化欲求を持つエージェントモデルによる多種循環型流行の発現
- 遺伝的アルゴリズムによるあやとり図形生成 : 紐デザイン処理(2)
- ネットワーク上のワークステーションを用いた並列仮説推論システム
- ワークステーションクラスタを用いた並列仮説推論システム
- 異機種分散環境上の並列仮説推論システム
- 三次元2値画像における高速ラベル付けアルゴリズム(画像認識,コンピュータビジョン)
- ウイルス進化型遺伝的アルゴリズムにおける感染手法による個体進化の相違に関する一考察
- 楷書オンライン入力からの連筆文字生成法について
- ファジィ・スプライン関数近似による手話テキスト作成の効率化について
- エージェント間通信による人体パーツ追跡の一手法
- 編物操作の記号表現とその可視化への応用
- 3次元紐図形表現方法を用いた編物パターン処理について
- 編物における紐状態の表現方法と編目記号生成システムの作成
- 編目記号生成システムの構成 : 紐図形の認識の編み物デザイン処理への応用
- n-BDDのための節点の動的追加手法 : ロボットの行動則獲得への適用
- 分散知識システムにおける一貫性保持機構について
- 個人生体信号からのマイサウンド生成システムについて
- ロバスト推定を用いた3次元形状の咬合評価のための一手法(画像情報)
- H-055 ニューラルネットと2自由度の回転による3次元物体の局所曲面分類(H分野:画像認識・メディア理解)
- 帰納論理プログラミングを用いた詰将棋ヒューリスティックの帰納
- 帰納論理プログラミングを用いた詰め将棋のルール獲得
- ILPを利用した問題解決のためのヒューリスティクスの獲得
- ILPを利用した問題解決のためのヒューリスティクスの獲得
- 多出力二分決定グラフの Flexible APPLY 交叉を用いた生態分化モデル
- 6S-7 先天的な脳機能局在性を考慮した認知機構のモデル化(遺伝的アルゴリズム・人口生命,学生セッション,人工知能と認知科学)
- 同調遺伝子とミームを用いた性選択モデルにおける循環型流行の発現
- 対話者好感度に基づく感性会話ロボットの感情生成モデル
- J-045 遠隔コミュニケーションのための感性ロボットと人の表情対応付け(J分野:ヒューマンコミュニケーション&インタラクション)
- J-044 感性ロボットの感情空間を用いた表情変化によるインタラクション効果(J分野:ヒューマンコミュニケーション&インタラクション)
- LJ-011 ベイジアンネットワークを用いた感性会話ロボットのための対話者感情の推定法(ヒューマンコミュニケーション&インタラクション)
- LJ-010 感性ロボットの表情変化による性格付け(ヒューマンコミュニケーション&インタラクション)
- 経験からの知識獲得に基づいたヒューマノイドの運動制御
- 感性ロボットのための感情領域を用いた表情生成
- F_022 ワクチンを考慮したウイルス感染エージェントモデルの提案(F分野:人工知能・ゲーム)
- 感情指定パラメータからの感性ロボットの表情生成
- 色彩パターンと輪郭形状の重み付き類似度を用いた接合判別法
- 輪郭形状の階層表現に基づく接合箇所検出と土器復元への応用
- ロボットの混合感情表出のための表情制御手法(エンタテインメントコンピューティング)
- 破片表面の輪郭形状と色彩パターンのマッチングに基づく土器復元の一手法
- パチンコの数理モデル化, 大当り回数期待値解析, および大当りの波の制御について
- パチンコの数理モデル化, 大当り回数期待値解析, および大当りの波の制御について
- 画像アーカイブ情報からの類似箇所検出技術と考古遺物復元への応用--土器復元システム
- パチンコの数理モデル化について(応用)
- サブエルブラン領域の特定およびモデル生成定理証明への応用(その他の基礎理論)
- ロボットを用いた独居高齢者のための生活支援システム(OS6 ロボット・ヒューマンコミュニケーション)
- 拡散律速凝集体の形状特性に着目したサウンド変換の一手法
- 一次元セルオートマトンの時間発展パタンに基づくサウンド変換の一手法
- 出生前淘汰による遺伝的アルゴリズムの効率化
- 外敵遭遇時における魚群の行動特性 : 進化計算を用いた群行動のシミュレーションモデル
- 判別の難易度に基づく類似箇所検出の高速化(21世紀のグループウェア)
- PARCAR : コストに基づく並列仮説推論システム
- 5D-7 画像輪郭の接合のための探索制御の一手法
- BDDを用いた仮説推論における高速化の一方法
- 契約ネットプロトコルに基づいたマルチエージェントプランニング
- 帰納学習を使った詰め将棋戦略の獲得
- BDDを用いた仮説推論の並列化の一方法
- 二分決定グラフを用いた仮説推論処理の一手法
- コストに基づく仮説推論における最適解探索の一方法
- コストに基づく仮説推論の並列化について
- コスト付き仮説推論に対する近似解法の一手法
- コスト付仮説推論における最適解探索について
- プログラム解析に基づく仮説推論の高速化技法
- コストに基く仮設推論における最適解探索について
- 不確定論理データベースを対象とした仮説推論
- プログラム解析に基づく仮説推論の高速化技法
- H-037 単眼カメラからの移動物体の3次元位置復元(H分野:画像認識・メディア理解)
- 進化的学習エージェントによる役割分担の発現
- 進化的学習エージェントによる役割分担の創発
- 高齢者音声韻律特徴を用いたHDS-Rスコアとの相関分析 : 音声を用いた認知症の早期スクリーニングをめざして
- 同等ラベル解析に基づく1回走査ラベル付けアルゴリズム
- ラスタ走査型ラベル付けアルゴリズムにおける第一走査の効率化手法(研究速報)
- 連に基づく高速2回走査ラベル付けアルゴリズム
- 高速2回走査ラベル付けアルゴリズム(パターン認識)
- F-046 サブエルブラン領域計算の効率化の一手法(F分野:人工知能・ゲーム)
- 線形表現を用いたウイルス進化型遺伝的プログラミング
- 対話型進化計算による画像間色彩変換について
- 定理証明器SATCHMOに関する新しい効率化手法(システムLSIの設計技術と設計自動化)
- 血縁淘汰による複数個体採餌モデルの進化(21世紀のグループウェア)
- 適応度評価を導入した拡張二分決定グラフの進化手法
- 多出力二分決定グラフのAPPLY交叉を用いた食物連鎖モデル
- 血縁淘汰による「種」の分化と利他行動の獲得
- ルールベースを用いた編物デザイン支援システム
- 強化学習結果の再構築への概念学習の適用
- 多色編み物デザイン支援システムの提案と構築について
- 4U-5 環境変動に対する適応行動と繁殖休眠の進化による渡りの創発(遺伝的アルゴリズム(1),学生セッション,人工知能と認知科学,情報処理学会創立50周年記念)
- 2W-5 ヒューマノイドロボットによるキネティックチェイン投球運動学習(学習(1),学生セッション,人工知能と認知科学,情報処理学会創立50周年記念)
- 定理証明器A-SATCHMOREの改良の一手法
- F-TPP:ファジィ推論を用いたTPP画像圧縮法
- 運筆状態規則を用いた平仮名毛筆文字生成について
- SRAMCs : 細線化骨格の歪み補正手法について
- 定理証明器SATCHMOREの効率化に関する一手法
- 知識と時間の論理のための推論システムの並列化手法
- コンピュータ将棋における危険判別探索
- 編物における紐状態表現と編み上がり模様生成の一手法
- アヤトリ図形のトポロジカルな性質と結び目多項式による特性化