田村 直之

J-GLOBALへ         更新日: 18/11/14 11:23
 
アバター
研究者氏名
田村 直之
 
タムラ ナオユキ
URL
http://bach.istc.kobe-u.ac.jp/tamura-jp.html
所属
神戸大学
部署
情報基盤センター
職名
教授
学位
工学修士(神戸大学)(神戸大学), 学術博士(神戸大学)

プロフィール

制約プログラミング,論理プログラミング,SAT技術に興味を持つ.

研究キーワード

 
 

研究分野

 
 

経歴

 
2003年
   
 
神戸大学 学術情報基盤センター・工学部 教授
 
1992年
   
 
神戸大学 工学部・自然科学研究科 助教授
 
1988年
   
 
神戸大学 工学部 講師
 
1985年
   
 
日本IBM
 

受賞

 
2018年9月
情報処理学会 情報処理学会 2018 年度特選論文 SAT技術を用いたペトリネットのデッドロック検出手法の提案
受賞者: 寸田 智也, 宋 剛秀, 番原 睦則, 田村 直之, 井上 克巳
 
2018年8月
XCSP3 Competition Organization 2018 XCSP3 Competition 2部門優勝 (逐次CSPソルバー部門, 並列CSPソルバー部門) sCOP
受賞者: Takehide Soh, Daniel Le Berre, Mutsunori Banbara, Naoyuki Tamura
 
2017年3月
人工知能学会 2016年度全国大会優秀賞 SAT型制約ソルバーによるナンバーリンクの解法とその評価
受賞者: 迫 龍哉, 川原 征大, 宋 剛秀, 番原 睦則, 田村 直之, 鍋島 英知
 
2017年3月
日本ソフトウェア科学会 プログラミング論研究会 PPL2017発表賞(一般の部) SATソルバーの最新動向と利用技術
受賞者: 宋 剛秀, 田村 直之
 
2016年3月
日本ソフトウェア科学会 第20回研究論文賞 パッキング配列問題の制約モデリングとSAT符号化
受賞者: 則武 治樹, 番原 睦則, 宋 剛秀, 田村 直之, 井上 克巳
 

論文

 
SAT技術を用いたペトリネットのデッドロック検出手法の提案
寸田 智也, 宋 剛秀, 番原 睦則, 田村 直之, 井上 克巳
情報処理学会論文誌   59(9) 1749-1760   2018年9月   [査読有り]
南 雄之, 宋 剛秀, 番原 睦則, 田村 直之
コンピュータソフトウェア   35(3) 65-78   2018年8月   [査読有り]
Mutsunori Banbara, Katsumi Inoue, Benjamin Kaufmann, Tenda Okimoto, Torsten Schaub, Takehide Soh, Naoyuki Tamura, Philipp Wanko
Annals of Operations Research      2018年1月   [査読有り]
sCOP: SAT-based Constraint Programming System
Takehide Soh, Daniel Le Berre, Mutsunori Banbara, Naoyuki Tamura
Solver Descriptions of XCSP3 Competition 2018 (XCSP18)   1-2   2018年
catnap: Generating Test Suites of Constrained Combinatorial Testing with Answer Set Programming
Mutsunori Banbara, Katsumi Inoue, Hiromasa Kaneyuki, Tenda Okimoto, Torsten Schaub, Takehide Soh, Naoyuki Tamura
The 14th International Conference on Logic Programming and Non-monotonic Reasoning (LPNMR-17)   265-278   2017年7月   [査読有り]

Misc

 
宋 剛秀, 番原 睦則, 田村 直之, 鍋島 英知
コンピュータソフトウェア   35(4) 72-92   2018年11月   [査読有り]
松永 裕介, 田村 直之
情報処理   59(3) 232–238   2018年3月   [査読有り][依頼有り]
宋 剛秀, 番原 睦則, 田村 直之
コンピュータソフトウェア   34(1) 67-80   2017年1月   [査読有り]
SATとパズル
田村 直之, 宋 剛秀, 番原 睦則
情報処理   57(8) 710-715   2016年7月   [査読有り]
国際シンポジウムFLOPS 2012開催報告
田村 直之, 番原 睦則, 平山 勝敏, 宋 剛秀
コンピュータソフトウェア   30(1):16-19    2013年3月   [査読有り]
私のブックマーク:SAT ソルバー
番原 睦則, 宋 剛秀, 田村 直之, 井上 克巳
人工知能学会誌   28巻2号    2013年3月
SATソルバーの基礎
井上 克巳, 田村 直之
人工知能学会誌   25巻1号    2010年1月   [査読有り]
番原 睦則, 田村 直之
人工知能学会誌   25(1) 122-129   2010年1月   [査読有り]
制約最適化問題とSAT符号化
田村 直之, 丹生 智也, 番原 睦則
人工知能学会誌   25巻1号    2010年1月   [査読有り]
番原睦則, 田村直之, 井上克已
コンピュータソフトウェア   24(3) 75-86   2007年8月
本論文では,PrologからJavaへのトランスレータ処理系Prolog Cafeについて述べる.本システムでは,Prologプログラムは,WAMを介して,Javaプログラムに変換され,既存のJava処理系を用いてコンパイル・実行される.つまりProlog Cafeでは,項,述語などPrologの構成要素のすべてがJavaに変換される.このため,PrologCafeはJavaとの連携,拡張性に優れたProlog処理系となっている.Prolog Cafeはマルチスレッドによる並列実行をサポー...
田村直之, 番原睦則
人工知能学会誌   21(4) 455-462   2006年8月
田村直之, 番原睦則
コンピュータソフトウェア   22(1) 98-103   2005年2月
本論文では,著者らの開発した線形論理型言語コンパイラ処理系のLLPを用いて,古典命題線形論理の論理式の証明探索を行うシステムLL2LLPについて述べる.本システムは,古典命題線形論理式を直観主義線形論理式に変換し,さらにLLPコンパイラを用いてLLP抽象機械命令にコンパイルしたのち実行することで高速な証明探索を実現している点に特徴がある.いくつかの線形論理式に対して,既存の線形論理定理証明システムと性能を比較した所,ほとんどの問題でより良い結果が得られた.
線形論理の自動演繹システムに関する研究
田村 直之, 番原 睦則
科学研究費補助金(基盤研究(C)(2))研究成果報告書      2005年2月
田村直之, 番原睦則
コンピュータソフトウェア   20(5) 502-508   2003年10月
一階述語論理の節形式をPrologプログラムに変換し, Prologコンパイラ処理系を用いて定理証明を行うシステムとしてPTTP (Prolog Technology Theorem Prover)が知られている.本論文では,節形式を線形論理型言語LLPのプログラムに変換し, LLPコンパイラ処理系を用いることで,より効率的な証明探索が可能になることを示す.特に,証明中のリテラルをリソースとして追加することにより, ME (model elimination)処理を高速化している点に特徴がある.
Javaによる異種協調制約解消システムの開発
番原 睦則, 田村 直之, 井上 克巳, 川村 尚生
IPA Spring 2003   未記入    2003年
Javaによる異種協調制約解消システムの開発
番原 睦則, 田村 直之, 井上 克巳, 川村 尚生
平成14年度IPA未踏ソフトウェア創造事業成果報告書   未記入    2003年
Javaによる分散協調制約解消システム
番原 睦則, 田村 直之, 井上 克巳, 川村 尚生, 玉置 久
ソフトウェアデザイン(技術評論社)   134    2003年
田村直之
電子情報通信学会技術研究報告. AI, 人工知能と知識処理   102(91) 37-42   2002年6月
Girardによる線形論理は,計算機科学の様々な分野への応用が期待されている新しい論理体系である.線形論理に基づく論理型言語の研究は,特に活発な分野の一つであり,LO,LinLog,ACL,Lolli,Lygon,Forum,LLP等の言語が提案されている.本稿では,線形論理および線形論理プログラミングの概要について述べる.
金田悠紀夫, 瀧和男, 和田耕一, 田村直之
情報処理   43(2) 114-115   2002年3月
番原睦則, 姜京順, 田村直之
情報処理学会論文誌. プログラミング   42(11) 52-66   2001年12月
線形論理に基づく論理型言語については, 過去10年間にわたり数多くの言語が提案されている.これらの言語では, リソース(使用回数を制限されたプログラム節)を動的に追加, 消費(使用)することが可能である.しかしながら, 「リソースを消費する際の時間的順序を正確に記述する」というようなリソースの時間に依存した性質を表現することは困難であった.本稿では, 直観主義時相線形論理に基づく論理型言語TLLPの概要と, そのコンパイラ処理系のための抽象機械について述べる.TLLP言語はPrologと線...
番原睦則, 姜京順, 田村直之
コンピュータソフトウェア   18(1) 195-216   2001年2月
吉見 毅彦, JELINEK Jiri, 西田 収, 田村 直之, 村上 温夫
自然言語処理 = Journal of natural language processing   7(4) 143-162   2000年11月
姜京順, 番原睦則, 田村直之
情報処理学会論文誌. プログラミング   41(4) 42-55   2000年7月
本稿では古典線形論理に基づいた論理型プログラミング言語の静的解析方法を提案する.線形論理に基づく論理型プログラミング言語としてはLolli, LinLog, LO, Lygon, Forumなどが提案されている.特に, Forumは古典線形論理に対し完全である論理型プログラミング言語である.しかし, Forumのプログラムの証明探索は非決定性が非常に大きいため, 静的解析することでプログラムの実行前に証明不可能なシーケントを取り除くことは重要である.Andreoliらは古典線形論理に基づく...
田村直之, 平井崇晴, 吉川英男, 姜京順, 番原睦則
情報処理学会論文誌. プログラミング   41(4) 11-23   2000年7月
1987年にJ.-Y.Girardによって考え出された線形論理は, 環境が動的に変化するソフトウェアを表現するための論理として非常に有望である.しかしながら, 線形論理では「動的に変化する環境」を表現することはできるが, 「時間経過とともに動的に変化する環境」を表現しきれているとは言えない.これは線形論理には時間の概念が直接的には入っておらず, 時間に存在した資源という概念を表現できないからである.そこで, 本論文では, 線形論理と時相論理の特徴を融合した時相線形論理の体系について述べ, ...
番原睦則, 姜京順, 田村直之
情報処理学会論文誌. プログラミング   40(10) 1-16   2000年1月
フランスの論理学者J.-Y.Girardによって線形論理(linear logic)が発表されて以来,プログラミング言語への応用が盛んに研究されている.線形論理に基づく論理型言語については,すでにいくつかが提案されている:Lolli, Lygon, LO, LinLog, Forum, HACL.しかし,Java上の処理系が実現されたものはまだ存在していない. これらの言語では,動的に生成,消費される「リソース」を論理式のレベルで表現できる.そのため効率のよいリソース処理は実装上最も重要な...
吉見 毅彦, JELINEK Jiri, 西田 収, 田村 直之, 村上 温夫
自然言語処理 = Journal of natural language processing   4(1) 3-21   1997年2月
堀内清光, 田村直之
日本ファジィ学会誌   6(6) 1094-1104   1995年1月
吉見毅彦, 田村直之, BosMarco J. W., 西田収, JelinekJiri, 村上温夫
コンピュータソフトウェア   10(1) 20-28   1993年2月
本稿では,文法的に可能な解釈の中から最も優先度の高い解釈を小さい計算量で選び出せるモデルを提案する.すなわち,入力が長くなるにつれ解釈の数が組み合わせ的に増大することに対処するために,構文解析系から得る解析木をAND-ORグラフで表し,それに含まれる部分グラフを表現するためにORチャイルド・リストという表現手段を導入する.さらに,AND-ORグラフとストリームを対応させ,ストリームに対する遅延評価技法を用いて効率的に最良解釈から順に取り出す方法について述べる.このモデルでは,グラフ上の節点...
馬野 元秀, 田村 直之
システム/制御/情報 : システム制御情報学会誌 = Systems, control and information   36(8)    1992年9月
Prologのプログラミング環境 (大特集 新しいプログラミング環境)
田村 直之, 浅川康夫
情報処理   30(4) 326-333   1989年5月   [査読有り]
松田秀雄, 田村直之, 小畑正貴, 金田悠紀夫, 前川禎男
情報処理学会論文誌   26(2) 296-303   1985年4月
試作マルチマイクロプロセッサシステム上への並列Prolog処理系"k-Prolog"の実装とその評価について述べる. まずマルチプロセッサ上でProlog処理系を実現するための並列実行モデルを与えそのモデルをもとにパイプライニング並列とOR並列という二つの並列処理方式の記述を行う. パイプライニング並列とは後戻り処理のときに必要となる別解を他のプロセッサがあらかじめ求めておくもので解の求められる順番が逐次実行の場合と同じになるという特徴をもっている. OR並列とはゴール節中の述語からの入力...

講演・口頭発表等

 
SATソルバーを用いた様相命題論理S4の充足可能性判定
飯野 有軌, 田村 直之, 番原 睦則, 宋 剛秀
日本ソフトウェア科学会第35回大会   2018年8月   
正規制約のSAT符号化とその性能評価
生田 哲也, 田村 直之, 番原 睦則, 宋 剛秀
日本ソフトウェア科学会第35回大会   2018年8月   
teaspoon: Solving the Curriculum-Based Course Timetabling Problems with Answer Set Programming
Mutsunori Banbara, Katsumi Inoue, Benjamin Kaufmann, Tenda Okimoto, Torsten Schaub, Takehide Soh, Naoyuki Tamura, Philipp Wanko
The 28th International Conference on Automated Planning and Scheduling, (ICAPS 2018)   2018年6月   
SAT型制約ソルバーを用いた3次元ナンバーリンクの解法
寸田 智也, 南 雄之, 宋 剛秀, 田村 直之
DAシンポジウム2017   2017年8月   情報処理学会システムとLSIの設計技術研究会
解集合プログラミングを用いた3次元ナンバーリンクソルバー
坡山 直樹, 飯野 有軌, 番原 睦則, 田村 直之
DAシンポジウム2017   2017年8月   

担当経験のある科目

 

競争的資金等の研究課題

 
科学研究費補助金/基盤研究(B)
研究期間: 2016年4月 - 2019年3月    代表者: 田村 直之
学術研究助成基金助成金/基盤研究(C)
研究期間: 2015年4月 - 2018年3月    代表者: 番原 睦則
科学研究費一部基金/基盤研究(B)
研究期間: 2012年4月 - 2015年3月    代表者: 田村 直之
科学研究費補助金/基盤研究(A)
研究期間: 2008年       代表者: 田村 直之
科学研究費補助金/基盤研究(C)
研究期間: 2005年       代表者: 田村 直之

学歴

 
 
 - 
1985年3月
神戸大学 大学院自然科学研究科博士課程システム科学専攻修了  
 

特許

 
特許3182471 : 文章解析方式
田村 直之, 村上 温夫, 吉見 毅彦, 西田 収