お知らせ 2023年度・2024年度 学生員 会費割引キャンペーン実施中です
お知らせ 技術研究報告と和文論文誌Cの同時投稿施策(掲載料1割引き)について
お知らせ 電子情報通信学会における研究会開催について
お知らせ NEW 参加費の返金について
電子情報通信学会 研究会発表申込システム
講演論文 詳細
技報閲覧サービス
[ログイン]
技報アーカイブ
 トップに戻る 前のページに戻る   [Japanese] / [English] 

講演抄録/キーワード
講演名 2013-01-10 13:30
制約付き項のインスタンスを受理する制約付き木オートマトンの構成法
中野靖大西田直樹酒井正彦坂部俊樹草刈圭一朗名大
抄録 (和) 制約付き項書換え系の書換え帰納法に基づいた定理自動証明の際に,制約付き項書換え系のR完全性の判定手続きが必要である.
また,対象の制約付き項書換え系が十分完全性を持つ場合に,定理自動証明中の推論規則の適用条件を緩和することができる.
これらの性質は,制約付き項のインスタンスの集合に関する積集合空問題に帰着できる.
本論文では,制約付き項のインスタンスを受理する制約付き木オートマトンの構成法を提案する.
さらに,制約付き木オートマトン中でどの入力基底項も到達することのない状態を削除する手法を提案することで,R完全性や十分完全性の判定の精度向上と効率化をめざす. 
(英) A theorem proving method for constrained term rewriting systems, which is based on rewriting induction, needs a decision procedure for R-completeness of constrained term rewriting systems.
In addition, sufficient completeness of constrained term rewriting systems enables us to relax the side conditions of some inference rules in the proving method.
These two properties of constrained term rewriting systems can be reduced to intersection emptiness problems related to sets of ground instances for constrained terms.
In this paper, we propose a method to construct constrained tree automata recognizing ground instances of constrained terms.
We also propose a method to remove states from a constrained tree automaton, to which no ground term transitions, thus improving the accuracy for the judgements of R-completeness and sufficient completeness.
キーワード (和) 制約付き項書換え系 / 積集合空問題 / 十分完全性 / / / / /  
(英) constrained term rewriting system / intersection emptiness problem / sufficient completeness / / / / /  
文献情報 信学技報, vol. 112, no. 373, SS2012-47, pp. 7-12, 2013年1月.
資料番号 SS2012-47 
発行日 2013-01-03 (SS) 
ISSN Print edition: ISSN 0913-5685    Online edition: ISSN 2432-6380
PDFダウンロード

研究会情報
研究会 SS  
開催期間 2013-01-10 - 2013-01-11 
開催地(和) 沖縄県石垣市民会館 
開催地(英)  
テーマ(和) 一般 
テーマ(英)  
講演論文情報の詳細
申込み研究会 SS 
会議コード 2013-01-SS 
本文の言語 日本語 
タイトル(和) 制約付き項のインスタンスを受理する制約付き木オートマトンの構成法 
サブタイトル(和)  
タイトル(英) Construction of Constrained Tree Automata Recognizing Ground Instances of Constrained Terms 
サブタイトル(英)  
キーワード(1)(和/英) 制約付き項書換え系 / constrained term rewriting system  
キーワード(2)(和/英) 積集合空問題 / intersection emptiness problem  
キーワード(3)(和/英) 十分完全性 / sufficient completeness  
キーワード(4)(和/英) /  
キーワード(5)(和/英) /  
キーワード(6)(和/英) /  
キーワード(7)(和/英) /  
キーワード(8)(和/英) /  
第1著者 氏名(和/英/ヨミ) 中野 靖大 / Yasuhiro Nakano / ナカノ ヤスヒロ
第1著者 所属(和/英) 名古屋大学 (略称: 名大)
Nagoya University (略称: Nagoya Univ.)
第2著者 氏名(和/英/ヨミ) 西田 直樹 / Naoki Nishida / ニシダ ナオキ
第2著者 所属(和/英) 名古屋大学 (略称: 名大)
Nagoya University (略称: Nagoya Univ.)
第3著者 氏名(和/英/ヨミ) 酒井 正彦 / Masahiko Sakai / サカイ マサヒコ
第3著者 所属(和/英) 名古屋大学 (略称: 名大)
Nagoya University (略称: Nagoya Univ.)
第4著者 氏名(和/英/ヨミ) 坂部 俊樹 / Toshiki Sakabe / サカベ トシキ
第4著者 所属(和/英) 名古屋大学 (略称: 名大)
Nagoya University (略称: Nagoya Univ.)
第5著者 氏名(和/英/ヨミ) 草刈 圭一朗 / Keiichirou Kusakari / クサカリ ケイイチロウ
第5著者 所属(和/英) 名古屋大学 (略称: 名大)
Nagoya University (略称: Nagoya Univ.)
第6著者 氏名(和/英/ヨミ) / /
第6著者 所属(和/英) (略称: )
(略称: )
第7著者 氏名(和/英/ヨミ) / /
第7著者 所属(和/英) (略称: )
(略称: )
第8著者 氏名(和/英/ヨミ) / /
第8著者 所属(和/英) (略称: )
(略称: )
第9著者 氏名(和/英/ヨミ) / /
第9著者 所属(和/英) (略称: )
(略称: )
第10著者 氏名(和/英/ヨミ) / /
第10著者 所属(和/英) (略称: )
(略称: )
第11著者 氏名(和/英/ヨミ) / /
第11著者 所属(和/英) (略称: )
(略称: )
第12著者 氏名(和/英/ヨミ) / /
第12著者 所属(和/英) (略称: )
(略称: )
第13著者 氏名(和/英/ヨミ) / /
第13著者 所属(和/英) (略称: )
(略称: )
第14著者 氏名(和/英/ヨミ) / /
第14著者 所属(和/英) (略称: )
(略称: )
第15著者 氏名(和/英/ヨミ) / /
第15著者 所属(和/英) (略称: )
(略称: )
第16著者 氏名(和/英/ヨミ) / /
第16著者 所属(和/英) (略称: )
(略称: )
第17著者 氏名(和/英/ヨミ) / /
第17著者 所属(和/英) (略称: )
(略称: )
第18著者 氏名(和/英/ヨミ) / /
第18著者 所属(和/英) (略称: )
(略称: )
第19著者 氏名(和/英/ヨミ) / /
第19著者 所属(和/英) (略称: )
(略称: )
第20著者 氏名(和/英/ヨミ) / /
第20著者 所属(和/英) (略称: )
(略称: )
講演者 第1著者 
発表日時 2013-01-10 13:30:00 
発表時間 30分 
申込先研究会 SS 
資料番号 SS2012-47 
巻番号(vol) vol.112 
号番号(no) no.373 
ページ範囲 pp.7-12 
ページ数
発行日 2013-01-03 (SS) 


[研究会発表申込システムのトップページに戻る]

[電子情報通信学会ホームページ]


IEICE / 電子情報通信学会