研究者詳細 - 西田　直樹

論文 - 西田　直樹

分割表示 245 件中 81 - 100 件目／全件表示 >>

組合せ最適化問題記述のためのSQLの拡張

内田佑作, 酒井正彦, 西田直樹

電子情報通信学会技術報告 115 巻 ( 508 ) 頁： 25-30 2016年3月

記述言語：日本語

近年，充足可能性判定ソルバの高速化がめざましい．しかしながらこれらのソルバを用いて組合せ最適化問題を解くための論理式へのコーディングは容易ではない．本稿では，組合せ最適化問題の定義の容易な記述を可能にするため，データベース問い合わせ言語SQLに対して組合せ最適化問題を記述するための構文を追加し，その記述から充足可能性判定ソルバを利用して問題の解を得るための手法について論ずる．

拡張Farkas補題の部分適用による非線形ループ不変式生成を用いたプログラム検証

柳澤真志, 西田直樹, 酒井正彦

電子情報通信学会技術報告 115 巻 ( 508 ) 頁： 31-36 2016年3月

記述言語：日本語

ループ不変式を生成するための手法として，与えたテンプレートと事前条件と事後条件から得られる検証式をFarkas補題に基づき変換する手法が研究されている．Farkas補題に基づく変換では線形な多項式の不等式のみを原始論理式として含む論理式を等価変換する．それを変数や関数適用項の積を単項式とする多項式上に拡張した拡張Farkas補題が提案され，非線形なループ不変式を生成できる場合があることが示された．しかし，拡張Farkas補題を用いて生成したループ不変式がプログラム検証に有効かどうかについては議論されていない．本稿では，プロラム検証における拡張Farkas補題に基づくループ不変式の生成法の有効性を評価し，拡張Farkas補題を有効に利用する検証手法を提案する．具体的には，未知係数を含む複数の検証式の一部を拡張Farkas補題により変換し，それを充足する未知係数の割り当てを残りの検証式の未知係数に代入した後に恒真性を判定する．

ナローイングによる制約付き依存対の変換

笹野智裕, 西田直樹, 酒井正彦

電子情報通信学会技術報告 115 巻 ( 420 ) 頁： 123-128 2016年1月

記述言語：日本語

項書換え系の停止性証明の枠組みである依存対フレームワークは項書換え規則に制約を付随させた制約付き項書換え系を対象に拡張された．本論文では、拡張された依存対フレームワークにおけるナローイングによる依存対の変換の適用条件を緩和する．具体的には，先行研究における変換対象の依存対が直接接続可能でないという条件を満たさない場合にも変換が健全であることことを示す．

制約付き項書換え系における停止性と帰納的定理の同時証明

川本佳史, 西田直樹, 酒井正彦

電子情報通信学会技術報告 115 巻 ( 420 ) 頁： 75-80 2016年1月

Constrained Term Rewriting tooL 査読有り

Cynthia Kop and Naoki Nishida

Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, Lecture Notes in Computer Science ( 9450 ) 頁： 549-557 2015年11月

記述言語：英語

This paper discusses Ctrl, a tool to analyse - both automatically and manually - term rewriting with logical constraints. Ctrl can be used with TRSs on arbitrary underlying logics, and automatically analyse various properties such as termination, confluence and quasi-reductivity. Ctrl also offers both a manual and automatic mode for equivalence tests using inductive theorem proving, giving support for and verification of "hand-written" term equivalence proofs.

DOI： 10.1007/978-3-662-48899-7_38

SATソルバへの基数制約節導入における学習節の最大保持数

塚本尚秀, 酒井正彦, 西田直樹, 橋本健二

平成27年度電気・電子・情報関係学会東海支部連合大会講演論文集 ( A2-5 ) 頁： 1 2015年9月

Reducing Relative Termination to Dependency Pair Problems 査読有り

Jose Iborra, Naoki Nishida, German Vidal, and Akihisa Yamada

Proceddings of the 25th International Conference on Automated Deduction (CADE 2015), Lecture Notes in Computer Science 9195 巻頁： 163-178 2015年8月

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

Relative termination, a generalized notion of termination, has been used in a number of different contexts like proving the confluence of rewrite systems or analyzing the termination of narrowing. In this paper, we introduce a new technique to prove relative termination by reducing it to dependency pair problems. To the best of our knowledge, this is the first significant contribution to Problem #106 of the RTA List of Open Problems. The practical significance of our method is illustrated by means of an experimental evaluation.

DOI： 10.1007/978-3-319-21401-6_11

CO3: a COnverter for proving COfluence of COnditional TRSs

Naoki Nishida, Takayuki Kuroda, Makishi Yanagisawa, and Karl Gmeiner

Proceedings of the 4th International Workshop on Confluence (IWC 2015) 頁： 42 2015年8月

Confluence Competition 2015

Takahito Aoto, Nao Hirokawa, Julian Nagele, Naoki Nishida, and Harald Zankl

Proceddings of the 25th International Conference on Automated Deduction (CADE 2015), Lecture Notes in Computer Science 9195 巻頁： 101-104 2015年8月

パターン除去による制約付き項書換え系の等価変換

長尾貴浩, 西田直樹, 酒井正彦

電子情報通信学会技術報告 115 巻 ( 153 ) 頁： 167-172 2015年7月

記述言語：日本語

制約付き項書換え系は整数制約などにより規則の適用を制御できるように項書換え系を拡張した枠組みである．書換え規則の左辺に現れるパターンの一部を意味を変えることなく除去することにより，様々な性質の解析が容易となる．本稿では，左辺に解釈項のパターンのみを持つ制約付き項書換え系のパターン除去に基づく変換を提案し，この変換が十分完全性や最内停止性などの性質に関して等価変換となる十分条件を示す．また，変換の応用として書換え完全性の判定法を提案する．

制約付き項書換え系における関数合成の可換性を自動証明するためのヒューリスティック

栗木隆太朗, 西田直樹, 酒井正彦, 坂部俊樹

電子情報通信学会技術報告 114 巻 ( 510 ) 頁： 91-96 2015年3月

木構造データを扱う関数の逆Unfold問題の発見的解法

加藤友郁, 長島正憲, 酒井正彦, 西田直樹, 坂部俊樹

電子情報通信学会技術報告 114 巻 ( 510 ) 頁： 85-90 2015年3月

A framework for computing finite SLD trees 査読有り

Naoki Nishida and German Vidal

Journal of Logical and Algebraic Methods in Programming 84 巻 ( 2 ) 頁： 197-217 2015年3月

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

The search space of SLD resolution, usually represented by means of a so-called SLD tree, is often infinite. However, there are many applications that must deal with possibly infinite SLD trees, like partial evaluation or some static analyses. In this context, being able to construct a finite representation of an infinite SLD tree becomes useful.

In this work, we introduce a framework to construct a finite data structure representing the (possibly infinite) SLD derivations for a goal. This data structure, called closed SLD tree, is built using four basic operations: unfolding, flattening, splitting, and subsumption. We prove some basic properties for closed SLD trees, namely that both computed answers and calls are preserved. We present a couple of simple strategies for constructing closed SLD trees with different levels of abstraction, together with some examples of its application. Finally, we illustrate the viability of our approach by introducing a test case generator based on exploring closed SLD trees.

DOI： 10.1016/j.jlamp.2014.11.006

制約付き項書換え系の停止性証明におけるナローイングの効果について

上山智也, 西田直樹, 酒井正彦, 坂部俊樹

電子情報通信学会技術報告 114 巻 ( 416 ) 頁： 43-48 2015年1月

例外処理を含む関数型プログラムの停止性証明のための条件付き依存対法の実現

太田浩一, 濱口毅, 酒井正彦, 山田晃久, 西田直樹, 坂部俊樹

電子情報通信学会技術報告 114 巻 ( 416 ) 頁： 55-60 2015年1月

A Finite Representation of the Narrowing Space 査読有り

Naoki Nishida and German Vidal

Revised Selected Papers of the 23rd International Conference on Logic-Based Program Synthesis and Transformation, Lecture Notes in Computer Science 8901 巻頁： 54-71 2014年12月

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

Narrowing basically extends rewriting by allowing free vari- ables in terms and by replacing matching with unification. As a con- sequence, the search space of narrowing becomes usually infinite, as in logic programming. In this paper, we introduce the use of some operators that allow one to always produce a finite data structure that still rep- resents all the narrowing derivations. Furthermore, we extract from this data structure a novel, compact equational representation of the (pos- sibly infinite) answers computed by narrowing for a given initial term. Both the finite data structure and the equational representation of the computed answers might be useful in a number of areas, like program comprehension, static analysis, program transformation, etc.

DOI： 10.1007/978-3-319-14125-1

Automatic Constrained Rewriting Induction towards Verifying Procedural Programs 査読有り

Cynthia Kop and Naoki Nishida

Proceedings of the 12th Asian Symposium on Programming Languages and Systems (APLAS 2014) ( 8858 ) 頁： 334-353 2014年11月

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

This paper aims at developing a verification method for procedural programs via a transformation into logically constrained term rewriting systems (LCTRSs). To this end, we adapt existing rewriting induction methods to LCTRSs and propose a simple yet effective method to generalize equations. We show that we can handle realistic functions, involving, e.g., integers and arrays. An implementation is provided.

DOI： 10.1007/978-3-319-12736-1_18

A Simple Sufficient Condition for the Completeness of a Heuristic Procedure for Inverse Unfold Problem

Masanori Nagashima, Tomofumi Kato, Masahiko Sakai, and Naoki Nishida

IPSJ Special Interest Group on Programming ( 2014-3-(9) ) 頁： 1-7 2014年11月

制約付き項書換え系の書換え帰納法における関数合成の可換性を利用した補題生成について

栗木隆太朗, 西田直樹, 酒井正彦

平成26年度電気・電子・情報関係学会東海支部連合大会講演論文集 ( M4-1 ) 頁： 1 2014年9月

条件除去変換を用いた条件付き項書換え系の合流性証明手続きについて

柳澤真志, 西田直樹, 酒井正彦, 坂部俊樹

平成26年度電気・電子・情報関係学会東海支部連合大会講演論文集 ( M4-4 ) 頁： 1 2014年9月

　前のページ - 次のページ　

<西田 直樹>

論文 - 西田 直樹

<西田　直樹>

論文 - 西田　直樹