研究者詳細 - 西田　直樹

論文 - 西田　直樹

分割表示 254 件中 181 - 200 件目／全件表示 >>

基本対称関数を付加した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月

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

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

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

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

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

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

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

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

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

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

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

Open Access

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月

例外処理付きオブジェクト指向プログラムにおける情報流の安全性解析のための型システム査読有り Open Access

黒川翔, 桑原寛明, 山本晋一郎, 坂部俊樹, 酒井正彦, 草刈圭一朗, 西田直樹

電子情報通信学会論文誌 D J91-D 巻 ( 3 ) 頁： 757-770 2008年3月

潜在帰納法を利用した手続き型プログラム検証の試み

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

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

等式を規則化する変換の停止条件 Open Access

水野清貴, 西田直樹, 坂部俊樹, 酒井正彦, 草刈圭一朗

信学技報 SS2007-61 107 巻 ( 505 ) 頁： 25-30 2008年3月

動的型言語への柔らかい型付けによるエラー検出

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

信学技報 SS2007-58 107 巻 ( 505 ) 頁： 7-12 2008年3月

プログラム生成系GeneSysにおける等式仕様への否定の導入 Open Access

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

信学技報 SS2007-45 107 巻 ( 392 ) 頁： 43-48 2007年12月

対話型埋込みによる数独問題の設計ツール Open Access

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

信学技報 SS2007-50 107 巻 ( 392 ) 頁： 73-78 2007年12月

導出木からのループ検出による論理プログラムの非停止性証明法 Open Access

水谷知博, 西田直樹, 酒井正彦, 坂部俊樹, 草刈圭一朗

信学技報 SS2007-30 107 巻 ( 275 ) 頁： 1-6 2007年10月

論理式への変換に基づく魔方陣の発見

伊藤寛之, 酒井正彦, 草刈圭一朗, 坂部俊樹, 西田直樹

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

左線形な定向条件付き項書換え系における到達可能な項集合の近似集合を認識する木オートマトン Open Access

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

信学技報 SS2007-16 107 巻 ( 176 ) 頁： 1-6 2007年8月

振舞等価性の証明のための等式付き書換えに基づく潜在帰納法 Open Access

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

信学技報 SS2007-17 107 巻 ( 176 ) 頁： 7-12 2007年8月

* Transformation for Refining Unraveled Conditional Term Rewriting Systems 査読有り

Naoki Nishida, Tomohiro Mizutani, and Masahiko Sakai

Electronic Notes in Theoretical Computer Science 174 巻 ( 10 ) 頁： 75-95 2007年7月

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

Unravelings, transformations from conditional term rewriting systems (CTRSs, for short) into unconditional
term rewriting systems, are valuable for analyzing properties of CTRSs. In order to completely simulate
rewrite sequences of CTRSs, the restriction by a particular context-sensitive and membership condition that
is determined by extra function symbols introduced due to the unravelings, must be imposed on the rewrite
relations of the unraveled CTRSs. In this paper, in order to weaken the context-sensitive and membership
condition, we propose a transformation applied to the unraveled CTRSs, that reduces the number of the
extra symbols. In the transformation, updating the context-sensitive condition properly, we remove the
extra symbols that satisfy a certain condition. If the transformation succeeds in removing all of the extra
symbols, we obtain the TRSs that are computationally equivalent with the original CTRSs.

　前のページ - 次のページ　

<西田 直樹>

論文 - 西田 直樹

<西田　直樹>

論文 - 西田　直樹