研究者詳細 - 西田　直樹

論文 - 西田　直樹

分割表示 245 件中 161 - 180 件目／全件表示 >>

Goal-directed and Relative Dependency Pairs for Proving the Termination of Narrowing 査読有り

José Iborra, Naoki Nishida, and Germán Vidal

Postproceedings of the 19th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2009), Lecture Notes in Computer Science 6037 巻頁： 52-66 2010年4月

Proving Injectivity of Functions via Program Inversion in Term Rewriting 査読有り

Naoki Nishida and Masahiko Sakai

Proceedings of the 10th International Symposium on Functional and Logic Programming (FLOPS 2010), Lecture Notes in Computer Science 6009 巻頁： 288-303 2010年4月

基本対象関数に基づく節を持つCNF論理式の充足可能性判定査読有り

馬野洋平, 酒井正彦, 西田直樹, 坂部俊樹, 草刈圭一朗

電子情報通信学会論文誌 D J93-D 巻 ( 1 ) 頁： 1-9 2010年1月

条件付き等式の変換に基づくプログラム生成

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

信学技報 SS2009-41 109 巻 ( 343 ) 頁： 37-42 2009年12月

高階書換え系における引数切り落とし法と実効規則

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

信学技報 SS2009-39 109 巻 ( 343 ) 頁： 25-30 2009年12月

右線形右シャローな項書換え系における文脈依存停止性の決定可能性について

御宿義勝, 酒井正彦, 坂部俊樹, 草刈圭一朗, 西田直樹

信学技報 SS2009-40 109 巻 ( 343 ) 頁： 31-36 2009年12月

Improving the Termination Analysis of Narrowing in Left-Linear Constructor Systems 査読有り

José Iborra, Naoki Nishida, and Germán Vidal

Proceedings of the 19th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2009) 頁： 9 pages 2009年9月

記述言語：英語

In this extended abstract, we introduce an extension of a previous technique
for proving the termination of narrowing. Basically, given a rewrite system
and an argument filtering, the previous technique required the filtered
program to be free of extra-variables. In this work, we transform the original
rewrite system so that, in some cases (namely when the filtered rewrite system
is left-shallow), termination can still be proved despite the occurrence of
extra-variables in the filtered system.

制約付き項書換え系の書換え帰納法における補題等式の自動生成法

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

日本ソフトウェア科学会第26回大会講演論文集 ( 7B-2 ) 頁： 1-14 2009年9月

Context-Sensitive Innermost Reachability is Decidable for Linear Right-Shallow Term Rewriting Systems 査読有り

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

IPSJ Transactions on Programming, 2 巻 ( 3 ) 頁： 20-32 2009年7月

Completion after Program Inversion of Injective Functions 査読有り

Naoki Nishida and Masahiko Sakai

Electronic Notes in Theoretical Computer Science 237 巻頁： 39-56 2009年4月

担当区分：筆頭著者記述言語：英語掲載種別：研究論文（学術雑誌）

Given a constructor term rewriting system that defines injective functions, the inversion compiler proposed
by Nishida, Sakai and Sakabe generates a conditional term rewriting system that defines the inverse relations
of the injective functions, and then the compiler unravels the conditional system into an unconditional term
rewriting system. In general, the resulting unconditional system is not (innermost-)confluent even if the
conditional system is (innermost-)confluent. In this paper, we propose a modification of the Knuth-Bendix
completion procedure, which is used as a post-processor of the inversion compiler. Given a confluent and
operationally terminating conditional system, the procedure takes the resulting unconditional systems as
input. When the procedure halts successfully, it returns convergent systems that are computationally
equivalent to the conditional systems. To adapt the modified procedure to the conditional systems that are
not confluent but innermost-confluent, we propose a simplified variant of the modified procedure. We report
that the implementations of the procedures succeed in generating innermost-convergent inverse systems for
all the examples we tried.

制約付き項書換え系における書換え帰納法査読有り

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

情報処理学会論文誌プログラミング 2 巻 ( 2 ) 頁： 80-96 2009年3月

記述言語：日本語掲載種別：研究論文（学術雑誌）

帰納的定理の証明原理の1 つである潜在帰納法が制約付き項書換え系に対応するよ
うに拡張され，命令型プログラムの等価性検証に応用されている．本論文では，別の
証明原理である書換え帰納法を制約付き項書き換え系に対応するように拡張するとと
もに，その正しさを証明する．また，拡張された書換え帰納法に基づいた帰納的定理
の証明法を提案する．さらに，帰納的定理でないことを示す反証の手法についても議
論する．

基本対称関数を付加したCNF論理式の充足可能性判定

馬野洋平, 酒井正彦, 西田直樹, 坂部俊樹, 草刈圭一朗

信学技報 SS2008-44 108 巻 ( 362 ) 頁： 31-36 2008年12月

シャローな依存対から構成される項書換え系の停止性の決定可能性

内山敬太, 酒井正彦, 坂部俊樹, 草刈圭一朗, 西田直樹

信学技報 SS2008-45 108 巻 ( 362 ) 頁： 37-42 2008年12月

ビットエラー通信路におけるスケーラブルCANの動作解析

鵜飼謙児, 坂部俊樹, 高田広章, 倉地亮, 酒井正彦, 草刈圭一朗, 西田直樹

信学技報 SS2008-37 108 巻 ( 242 ) 頁： 61-66 2008年10月

制約付き項書換え系における書換え帰納法

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

第71回情報処理学会・プログラミング研究会配布資料頁： 1-12 2008年10月

スケーラブルCANプロトコルの動作解析に関する予備的考察

鵜飼謙児, 坂部俊樹, 高田広章, 倉地亮, 酒井正彦, 草刈圭一朗, 西田直樹

平成20年度電気関係学会東海支部連合大会論文集 ( O-262 ) 頁： 1 2008年9月

制約付き項書換え系の潜在帰納法を利用した手続き型プログラム検証の試み査読有り

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

情報処理学会論文誌プログラミング 1 巻 ( 2 ) 頁： 100-121 2008年9月

記述言語：日本語掲載種別：研究論文（学術雑誌）

手続き型プログラムの検証手法として，モデル検査やホーア論理に基づく検証手法
が代表的である．一方，項書換えの分野では帰納的定理の証明手法として潜在帰納法
や書換え帰納法などが広く研究されている．本論文では，帰納的定理の証明法を利用
して手続き型プログラムの等価性の検証を試みる．具体的には，自然数上のwhile 言
語で定義された手続き型関数からプレスブルガー文を規則の制約として持つことが許
された制約付き項書換え系への変換を与え，その変換により手続き型プログラムの等
価性を書換え系の関数の等価性に帰着させ，潜在帰納法を用いて等価性検証を試みる．
この手法を実現するために，合流性を保証するための危険対定理および完備化手続き
を制約付き書換えに対応するように拡張する．

Completion as Post-Process in Program Inversion of Injective Functions 査読有り

Naoki Nishida and Masahiko Sakai

Proceedings of the 8th International Workshop on Reduction Strategies in Rewriting and Programming (WRS'08) 頁： 61-75 2008年7月

制約付き項書換え系の定理自動証明における等式の方向付けのための簡約化順序

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

信学技報 SS2008-20 108 巻 ( 173 ) 頁： 43-48 2008年7月

プレスブルガー文付き項書換え系における書換え帰納法について

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

信学技報 SS2008-1 108 巻 ( 64 ) 頁： 1-6 2008年5月

　前のページ - 次のページ　

<西田 直樹>

論文 - 西田 直樹

<西田　直樹>

論文 - 西田　直樹