研究者詳細 - 西田　直樹

論文 - 西田　直樹

分割表示 245 件中 141 - 160 件目／全件表示 >>

高階書換え系における引数切り落とし関数の下での実効規則について

大井一展, 草刈圭一朗, 酒井正彦, 坂部俊樹, 西田直樹

電子情報通信学会技術報告 111 巻 ( 406 ) 頁： 57-62 2012年1月

2リテラル監視法で実装されたSATソルバへの基本対称節処理機能の組み込み

日野善信, 酒井正彦, 坂部俊樹, 草刈圭一朗, 西田直樹

電子情報通信学会技術報告 111 巻 ( 268 ) 頁： 67-72 2011年10月

制約付き項書換え系における木準同型写像を用いた関数等価性検証

高桑一也, 西田直樹, 酒井正彦, 坂部俊樹, 草刈圭一朗

日本ソフトウェア科学会第28回大会論文集 ( 7B-1 ) 頁： 1-12 2011年9月

多重文脈書換え帰納法における反証と補題追加

坂田翼, 西田直樹, 酒井正彦, 草刈圭一朗, 坂部俊樹

日本ソフトウェア科学会第28回大会論文集 ( 1A-4 ) 頁： 1-12 2011年9月

Malbolgeの高級アセンブリ言語への加算命令の追加

安藤聡, 酒井正彦, 坂部俊樹, 草刈圭一朗, 西田直樹

日本ソフトウェア科学会第28回大会論文集 ( 5A-3 ) 頁： 1-12 2011年9月

関数呼び出しを持つプログラムの不変式の自動生成について

鈴木英一, 坂部俊樹, 酒井正彦, 草刈圭一朗, 西田直樹

平成23年度電気関係学会東海支部連合大会論文集 ( H1-5 ) 頁： 1 2011年9月

線形左シャロー項書換え系の停止性の決定可能性について

服部達哉, 酒井正彦, 坂部俊樹, 草刈圭一朗, 西田直樹

平成23年度電気関係学会東海支部連合大会論文集 ( H1-6 ) 頁： 1 2011年9月

Decidability of Reachability for Right-shallow Context-sensitive Term Rewriting Systems 査読有り

Yoshiharu Kojima, Masahiko Sakai, Naoki Nishida, Keiichirou Kusakari, and Toshiki Sakabe

IPSJ Transactions on Programming, 4 巻 ( 4 ) 頁： 12-35 2011年9月

Decidability and Undecidability of Reachability for Right-Linear Left-Shallow Non-Erasing Term Rewriting Systems

Yoshiharu Kojima, Masahiko Sakai, Naoki Nishida, Keiichirou Kusakari, and Toshiki Sakabe

LA Symposium 2011 Summer ( 15 ) 頁： 1-10 2011年7月

On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs 査読有り

Tsubasa Sakata, Naoki Nishida, and Toshiki Sakabe

Proceedings of the 20th International Workshop on Functional and (Constraint) Logic Programming, Lecture Notes in Computer Science 6816 巻頁： 138-155 2011年7月

記述言語：英語

In this paper, we propose methods for proving termination of constrained term rewriting systems, where constraints are interpreted by built-in semantics given by users, and rewrite rules are assumed to be sound for the interpretation. To this end, we extend the dependency pair framework for proving termination of unconstrained term rewriting systems to constrained term rewriting systems. Moreover, we extend the dependency pair framework so that dependency pair processors take a subgraph of the dependency graph as input and they output a finite set of graphs which can be obtained by eliminating nodes and/or edges from the input graph.

DOI： 10.1007/978-3-642-22531-4_9

Soundness of Unravelings for Deterministic Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity 査読有り

Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, LIPICcs 10 巻頁： 267-282 2011年5月

担当区分：筆頭著者記述言語：英語

Unravelings are transformations from a conditional term rewriting system (CTRS, for short) over an original signature into an unconditional term rewriting systems (TRS, for short) over an extended signature. They are not sound for every CTRS w.r.t. reduction, while they are complete w.r.t. reduction. Here, soundness w.r.t. reduction means that every reduction sequence of the corresponding unraveled TRS, of which the initial and end terms are over the original signature, can be simulated by the reduction of the original CTRS. In this paper, we show that an optimized variant of Ohlebusch's unraveling for deterministic CTRSs is sound w.r.t. reduction if the corresponding unraveled TRSs are left-linear or both right-linear and non-erasing. We also show that soundness of the variant implies that of Ohlebusch's unraveling.

DOI： 10.4230/LIPIcs.RTA.2011.267

Program Inversion for Tail Recursive Functions 査読有り

Naoki Nishida and German Vidal

Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, LIPIcs 10 巻頁： 283-298 2011年5月

担当区分：筆頭著者記述言語：英語

Program inversion is a fundamental problem that has been addressed in many different programming settings and applications. In the context of term rewriting, several methods already exist for computing the inverse of an injective function. These methods, however, usually return non-terminating inverted functions when the considered function is tail recursive. In this paper, we propose a direct and intuitive approach to the inversion of tail recursive functions. Our new technique is able to produce good results even without the use of an additional post-processing of determinization or completion. Moreover, when combined with a traditional approach to program inversion, it constitutes a promising approach to define a general method for program inversion. Our experimental results confirm that the new technique compares well with previous approaches.

DOI： 10.4230/LIPIcs.RTA.2011.283

制約付き木オートマトンとその閉包性

倉橋克尚, 酒井正彦, 西田直樹, 野村太志, 坂部俊樹, 草刈圭一朗

電子情報通信学会技術報告 110 巻 ( 458 ) 頁： 61-66 2011年3月

順方向ナローイングに基づく右線形右シャロー項書換え系の非停止性証明について

服部達哉, 酒井正彦, 西田直樹, 草刈圭一朗, 坂部俊樹

信学技報 SS2010-44 110 巻 ( 336 ) 頁： 31-36 2010年12月

等式理論を法とするDPLL遷移系について

馬場達也, 坂部俊樹, 西田直樹, 草刈圭一朗, 酒井正彦

信学技報 SS2010-36 110 巻 ( 227 ) 頁： 49-54 2010年10月

難解言語Malbolgeのチューリング完全性について

長坂哲, 酒井正彦, 坂部俊樹, 草刈圭一朗, 西田直樹

信学技報 SS2010-37 110 巻 ( 227 ) 頁： 55-60 2010年10月

2カウンタ法に基づく基本対称節を持つCNF論理式のSATソルバ

日野善信, 酒井正彦, 草刈圭一朗, 坂部俊樹, 西田直樹

平成22年度電気関係学会東海支部連合大会論文集 ( D3-5 ) 頁： 1 2010年8月

等式理論を法とする抽象DPLLアルゴリズムの提案

馬場達也, 坂部俊樹, 酒井正彦, 草刈圭一朗, 西田直樹

平成22年度電気関係学会東海支部連合大会論文集 ( D3-4 ) 頁： 1 2010年8月

制約付き項書換え系における関数の効率的な等価性検証

高桑一也, 西田直樹, 酒井正彦, 坂部俊樹, 草刈圭一朗

平成22年度電気関係学会東海支部連合大会論文集 ( D3-6 ) 頁： 1 2010年8月

Termination of Narrowing via Termination of Rewriting 査読有り

Naoki Nishida and Germán Vidal

Applicable Algebra in Engineering, Communication and Computing 21 巻 ( 3 ) 頁： 177-225 2010年5月

　前のページ - 次のページ　

<西田 直樹>

論文 - 西田 直樹

<西田　直樹>

論文 - 西田　直樹