帰納法に基づく定理証明器によるシストリックアレイの検証
スポンサーリンク
概要
- 論文の詳細を見る
帰納法に基づく定理証明器によるシストリックアレイの検証において, 帰納法を効果的に適用するための問題点を指摘しその解決策を示す.2次元シストリックアレイに対し, 時刻や回路パラメータを陽に含む式で表される実装記述から入出力信号の関係式を導出する手続きを定式化し, 行列の乗算回路に適用する.さらに, 時刻や回路パラメータを陽に含まない値の関係式として表現された仕様と, それらの値が入出力ポートで観測されるべきタイミングが与えられたときに, 実装記述から導出された入出力信号の関係式が仕様を満たすことを証明する際の技法についても述べる.
- 一般社団法人情報処理学会の論文
- 1998-07-15
著者
-
藤田 博
九州大学大学院システム情報科学研究院
-
藤田 博
九州大学大学院システム情報科学研究科
-
高橋 和子
三菱電機株式会社先端技術総合研究所
-
高橋 和子
三菱電機株式会社中央研究所
-
高橋 和子
順天堂大学医学部病理学第二講座
-
高橋 和子
三菱電機株式会社先端技術総合研究所:(現)atr音声翻訳通信研究所
-
高橋 和子
関西学院大学理工学研究科
関連論文
- 帰納論理プログラミングを用いたブログからのルール抽出 (「Web情報処理」および一般発表)
- モデル列挙とモデル計数(最近のSAT技術の発展)
- 青壮年層の地域住民が高齢者に期待する役割
- ODPを利用したユーザプロファイルを用いた個人化検索システム(情報検索)
- 調査・研究 閉じこもり傾向にある女性高齢者のHealth-Related QOLおよび活動能力に関する研究
- 宮城県大和町における高齢者の転倒予防に関する研究(第1報)つまずきと転倒の実態およびその関連要因
- 帰納論理プログラミングを用いたWebページ評価ルールの抽出とその評価(「Webインテリジェンス」及び一般)
- 2C-6 Blogデータのクラスタリングと分析(コンテンツ推薦,一般セッション,データベースとメディア)
- 関連単語抽出アルゴリズムを用いたWeb検索クエリの生成(Web情報検索,データ工学論文)
- F-039 モデル生成法を用いた極小モデル生成(人工知能・ゲーム,一般論文)
- モデル生成型定理証明と要素技術(論理と推論技術の展開)
- Wikipediaへの関連単語抽出アルゴリズムの適用とその評価(Wikipedia)
- 関連単語抽出アルゴリズムを用いたWeb検索クエリの生成(Web解析・検索クエリ)
- 1V-6 変数のアクティビティ情報を共有するマルチスレッドSATソルバ(学習・推論,学生セッション,人工知能と認知科学)
- 6S-9 ユーザーのスケジュールを用いたWebページ推薦(ユーザ指向・推薦,学生セッション,データベースとメディア)
- D-008 相関ルールに基づく文書検索システム(D分野:データベース)
- スケジュールに基づくWebページ推薦に用いる検索単語の選定(WEBサービス,特集「Web情報処理」及び一般)
- スケジュールに基づく Web ページ推薦に用いる検索単語の選定
- FPGA上のSATソルバPCMGTPへの前処理の導入
- D_024 ユーザの意思を反映したWeb検索の効率化(D分野:データベース)
- C_003 FPGAを用いたN-Queens問題の解決について(C分野:ハードウェア)
- WEB検索におけるキーワード関連語提案システム
- B_025 モデル検査器を用いたFUCEマルチスレッドプログラムの開発(B分野:ソフトウェア)
- ダイアグラムに基づく法的論争支援システム
- FUCE上のストリーム処理とその記述言語
- FUCE言語とその処理系について
- 生活習慣病予防における健康行動とソーシャルサポートの関連
- 東北地方の在宅高齢者における地域・家庭での役割の実態と関連要因の検討
- 高齢者夫婦世帯で在宅療養している要介護高齢者の介護者の精神的健康状態の良好群と低群における介護状態の比較
- 高齢者夫婦世帯における介護者のインフォーマルサポートの実態と精神的健康の関連
- 都市部と農村部における高齢者の地域ケアシステムに関するニーズとその傾向
- 在宅療養高齢者の介護者と訪問看護婦の介護の必要性に関する判断の比較と要介護者のADL状況との関連について
- GA-MGTPによる Condensed Detachment問題の解法
- Twitterにおける流行語先取り発言者の検出システムの開発
- Twitterにおける流行語先取り発言者の検出システムの開発
- ソーシャルブックマークにおける有用なユーザの発見
- Wikipediaのリンク共起とカテゴリに基づくリランキング手法
- Wikipediaのリンク共起とカテゴリに基づくリランキング手法
- Wikipediaへの関連単語抽出アルゴリズムの適用とその評価(Wikipedia)
- 関連単語抽出アルゴリズムを用いたWeb検索クエリの生成(Web解析・検索クエリ)
- ODPを利用したユーザプロファイルを用いた個人化検索システム(情報検索)
- 5S-4 Twitterの流行語発言者の抽出に基づくフォロワー推薦システムの開発(情報推薦(2),学生セッション,データベースとメディア,情報処理学会創立50周年記念)
- Twitter における流行語先取り発言者の検出システムの開発
- Wikipedia のリンク共起とカテゴリに基づくリランキング手法
- 帰納法に基づく定理証明器によるシストリックアレイの検証
- 帰納法に基づく定理証明器によるシストリックアレイの検証
- NQTHMを用いたシストリックアレイの検証
- Partial Max-SATソルバーQMaxSATの評価 (特集 「AIの基本問題SATと応用技術」および一般)
- SLEマウスにおける脾臓リンパ濾胞胚中心の免疫組織化学的特徴
- FPGA上に実装されたPCMGTPを用いたSAT問題の解決(応用1, FRGAとその応用及び一般)
- FPGA上に実装されたPCMGTPを用いたSAT問題の解決(応用1, FRGAとその応用及び一般)
- FPGA上に実装されたPCMGTPを用いたSAT問題の解決(応用1, FRGAとその応用及び一般)
- FPGA上に実装されたPCMGTPを用いたSAT問題の解決
- F-021 基数制約を用いたMax-SATソルバーの試作(F分野:人工知能・ゲーム,一般論文)
- F-019 BOINCによるSATソルバーの並列実行(F分野:人工知能・ゲーム,一般論文)
- D-033 データ解析における並列分散処理基盤Hadoopの利用(D分野:データベース,一般論文)
- 1W-9 モデル生成によるSATソルバの並列化(最適化,学生セッション,人工知能と認知科学,情報処理学会創立50周年記念)
- 5R-2 ODPを利用した個人化検索システムの比較と効率化(Webシステム,学生セッション,データベースとメディア,情報処理学会創立50周年記念)
- 3C-2 動詞の提示による動的な検索支援システム(Web検索支援,一般セッション,データベースとメディア,情報処理学会創立50周年記念)
- 一般化補題を利用したモデル生成法
- AND/OR両並列性をいかしたプラン生成について
- ANDOR並列論理型言語ANDOR-IIの並列論理型言語への変換
- FPGA上のSATソルバPCMGTPの改良について
- 帰納論理プログラミングを用いた棋譜からのルール抽出
- Twitterのリスト機能を用いたユーザの特徴抽出
- Twitter発言の時系列解析に基づくハッシュタグの内容説明
- Wikipediaの時系列アクセス数に着目した関連度算出
- 定理証明系PCMGTPのFPGA上の実装について
- モデル生成型定理証明器のFPGA上の実装(FPGAとその応用及び一般)
- モデル生成型定理証明器のFPGA上の実装(FPGAとその応用及び一般)
- モデル生成型定理証明器のFPGA上の実装(FPGAとその応用及び一般)
- 畳込みと分岐補題を統合したモデル生成
- ユーザに特化した情報収集エージェントの作成
- 帰納論理プログラミングを用いたTwitterからのルール抽出 (人工知能と知識処理)
- 帰納論理プログラミングを用いたTwitterからのルール抽出(「コンテキストを意識した知識の利用」及び一般)
- 空間情報の抽象化について
- 帰納論理プログラミングを用いた Twitter からのルール抽出
- 矩形同士の埋め込み型重ね合わせについての定性空間推論
- F-028 MaxSATの一拡張について(学習・最適化,F分野:人工知能・ゲーム)
- A-002 帰納論理プログラミングを用いた化学反応からのルール抽出(数理モデル化と問題解決(1),A分野:モデル・アルゴリズム・プログラミング)
- A-012 帰納論理プログラミングを用いた高分子の組成と物性との関係に関する考察(数理モデル(1),A分野:モデル・アルゴリズム・プログラミング)
- Twitterの時系列解析による注目話題の抽出
- 基数制約に基づくMaxSATソルバーにおける変数アクティビティ調整とその評価