Faculty Profiles - NISHIDA Naoki

Papers - NISHIDA Naoki

Division display 161 - 180 of about 247 ／ All the affair displays >>

Efficient Verification of Equivalence between Functions in Constrained Term Rewriting Systems

Kazuya Takakuwa, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe, and Keiichirou Kusakari

Record of 2010 Tokai-section Joint Conference of the Eight Institutes of Electrical and Related Engineers ( D3-6 ) page： 1 2010.8

Termination of Narrowing via Termination of Rewriting Reviewed

Naoki Nishida and Germán Vidal

Applicable Algebra in Engineering, Communication and Computing Vol. 21 ( 3 ) page： 177-225 2010.5

Goal-directed and Relative Dependency Pairs for Proving the Termination of Narrowing Reviewed

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 Vol. 6037 page： 52-66 2010.4

Proving Injectivity of Functions via Program Inversion in Term Rewriting Reviewed

Naoki Nishida and Masahiko Sakai

Proceedings of the 10th International Symposium on Functional and Logic Programming (FLOPS 2010), Lecture Notes in Computer Science Vol. 6009 page： 288-303 2010.4

Solving Satisfiability of CNF Formulas with Clauses based on Elementary Symmetric Functions Reviewed

Yohei Umano, Masahiko Sakai, Naoki Nishida, Toshiki Sakabe, and Keiichirou Kusakari

The IEICE Transactions on Information and Systems Vol. J93-D ( 1 ) page： 1-9 2010.1

Program Generation Based on Transformation of Conditional Equations

Masanori Nagashima, Masahiko Sakai, Toshiki Sakabe, Naoki Nishida, and Keiichirou Kusakari

IEICE Technical Report SS2009-41 Vol. 109 ( 343 ) page： 37-42 2009.12

Argument Filtering and Usable Rules in Higher-Order Rewrite Systems

Sho Suzuki, Keiichirou Kusakari, Toshiki Sakabe, Masahiko Sakai, and Naoki Nishida

IEICE Technical Report SS2009-39 Vol. 109 ( 343 ) page： 25-30 2009.12

On Decidability of Context-Sensitive Termination for Right-Linear Right-Shallow Term Rewriting Systems

Yoshimasa Mishuku, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari, and Naoki Nishida

IEICE Technical Report SS2009-40 Vol. 109 ( 343 ) page： 31-36 2009.12

Improving the Termination Analysis of Narrowing in Left-Linear Constructor Systems Reviewed

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

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

Language：English

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.

Lemma Generation Method in Rewriting Induction for Constrained Term Rewriting Systems

Naoki Nakabayashi, Naoki Nishida, Keiichirou Kusakari, Toshiki Sakabe, and Masahiko Sakai

Proceedings of the 26th Conference of Japan Society for Software Science and Technology (JSSST) ( 7B-2 ) page： 1-14 2009.9

Context-Sensitive Innermost Reachability is Decidable for Linear Right-Shallow Term Rewriting Systems Reviewed

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

IPSJ Transactions on Programming, Vol. 2 ( 3 ) page： 20-32 2009.7

Completion after Program Inversion of Injective Functions Reviewed

Naoki Nishida and Masahiko Sakai

Electronic Notes in Theoretical Computer Science Vol. 237 page： 39-56 2009.4

Authorship：Lead author Language：English Publishing type：Research paper (scientific journal)

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.

Rewriting Induction for Constrained Term Rewriting Systems Reviewed

Tsubasa Sakata, Naoki Nishida, Toshiki Sakabe, Masahiko Sakai, and Keiichirou Kusakari

IPSJ Transactions on Programming, Vol. 2 ( 2 ) page： 80-96 2009.3

Language：Japanese Publishing type：Research paper (scientific journal)

The implicit induction, which is one of induction principles for proving inductive
theorems of equational theories, has been extended to deal with constrained
term rewriting systems. It has been applied to a method for proving equivalence
of imperative programs. In this paper, we extend another induction principle,
the rewriting induction, to cope with the case of constrained term rewriting
systems, and show its correctness. We also propose a method for proving inductive
theorems being based on the extended rewriting induction. Moreover,
we show a technique to disprove inductive theorems.

Solving Satisfiability of CNF Formulas with Elementary Symmetric Functions

Yohei Umano, Masahiko Sakai, Naoki Nishida, Toshiki Sakabe, and Keiichirou Kusakari

IEICE Technical Report SS2008-44 Vol. 108 ( 362 ) page： 31-36 2008.12

Decidability of Termination Properties for Term Rewriting Systems Consisting of Shallow Dependency Pairs

Keita Uchiyama, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari, and Naoki Nishida

IEICE Technical Report SS2008-45 Vol. 108 ( 362 ) page： 37-42 2008.12

Behavior Analysis of Scalable CAN Protocol on a Bit-Error Channel

Kenji Ukai, Toshiki Sakabe, Hiroaki Takada, Ryo Kurachi, Masahiko Sakai, Keiichirou Kusakari, and Naoki Nishida

IEICE Technical Report SS2008-37 Vol. 108 ( 242 ) page： 61-66 2008.10

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

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

第71回情報処理学会・プログラミング研究会配布資料 page： 1-12 2008.10

A Preliminary Study on Behavior Analysis of Scalable CAN Protocol

Kenji Ukai, Toshiki Sakabe, Hiroaki Takada, Ryo Kurachi, Masahiko Sakai, Keiichirou Kusakari, and Naoki Nishida

Record of 2008 Tokai-section Joint Conference of the Eight Institutes of Electrical and Related Engineers ( O-262 ) page： 1 2008.9

Approach to Procedural-program Verification Based on Implicit Induction of Constrained Term Rewriting Reviewed

Yuki Furuichi, Naoki Nishida, Masahiko Sakai, Keiichirou Kusakari, and Toshiki Sakabe

IPSJ Transactions on Programming, Vol. 1 ( 2 ) page： 100-121 2008.9

Language：Japanese Publishing type：Research paper (scientific journal)

In the field of procedural programming, several verification methods based
on model checking or Hoare logic have been proposed. On the other hand,
in the field of term rewriting, implicit induction and rewriting induction have
been widely studied as methods for proving inductive theorems. In this paper,
we try to take advantages of methods for proving inductive theorems in verifying
procedural functions written in a "while" language with natural number
type. More precisely, we propose a transformation from procedural programs to
constrained term rewriting systems whose constraints are in Presburger arithmetic,
and show that the transformation reduces the equivalence of procedural
programs to that of functions in rewrite systems. By verifying the equivalence
between rewrite systems, we verify the equivalence between the corresponding
procedural functions. To establish this approach, we extend Critical Pair
Theorem and the basic completion procedure for constrained systems.

Completion as Post-Process in Program Inversion of Injective Functions Reviewed

Naoki Nishida and Masahiko Sakai

Proceedings of the 8th International Workshop on Reduction Strategies in Rewriting and Programming (WRS'08) page： 61-75 2008.7

　 PREV - NEXT 　

<NISHIDA Naoki>

Papers - NISHIDA Naoki