Faculty Profiles - NISHIDA Naoki

Papers - NISHIDA Naoki

Division display 141 - 160 of about 249 ／ All the affair displays >>

A Sound Type System for Typing Runtime Errors Reviewed

Akihisa Yamada, Keiichirou Kusakari, Toshiki Sakabe, Masahiko Sakai, and Naoki Nishida

IPSJ Transactions on Programming, Vol. 5 ( 2 ) page： 16-24 2012.3

On Rewriting Induction for Simply-typed Term Rewriting Systems

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

IEICE Technical Rerport Vol. 111 ( 406 ) page： 51-56 2012.1

On class of equation sets whose word problems are reducible to those of ground equation sets

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

IEICE Technical Rerport Vol. 111 ( 406 ) page： 45-49 2012.1

Automatic Generation of Non-linear Loop Invariants for Programs with Function Calls

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

IEICE Technical Rerport Vol. 111 ( 406 ) page： 39-44 2012.1

On Usable Rules under Argument Filterings in Higher-Order Rewrite Systems

Kazuhiro Ooi, Keiichirou Kusakari, Masahiko Sakai, Toshiki Sakabe and Naoki Nishida

IEICE Technical Rerport Vol. 111 ( 406 ) page： 57-62 2012.1

Incorporating Elementary Symmetric Clauses into SAT Solvers with Two-Watched-Literal Scheme

Yoshizane Hino, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari, and Naoki Nishida

IEICE Technical Rerport Vol. 111 ( 268 ) page： 67-72 2011.10

Verification of Equivalence between Functions in Constrained Term Rewriting Systems via Tree Homomorphisms

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

Proceedings of the 28th Conference of Japan Society for Software Science and Technology ( 7B-1 ) page： 1-12 2011.9

Disproving and Postulating for Multi-Context Rewriting Induction

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

Proceedings of the 28th Conference of Japan Society for Software Science and Technology ( 1A-4 ) page： 1-12 2011.9

Introducing Addition Instruction into High-Level Assembly Language for Malbolge

Satoshi Ando, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari, and Naoki Nishida

Proceedings of the 28th Conference of Japan Society for Software Science and Technology ( 5A-3 ) page： 1-12 2011.9

On Automatic Generation of Loop Invariants for Programs with Function Calls

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

Record of 2011 Tokai-section Joint Conference of the Eight Institutes of Electrical and Related Engineers ( H1-5 ) page： 1 2011.9

Decidability of Termination for Linear Left-Shallow Term Rewriting Systems

Tatsuya Hattori, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari, and Naoki Nishida

Record of 2011 Tokai-section Joint Conference of the Eight Institutes of Electrical and Related Engineers ( H1-6 ) page： 1 2011.9

Decidability of Reachability for Right-shallow Context-sensitive Term Rewriting Systems Reviewed

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

IPSJ Transactions on Programming, Vol. 4 ( 4 ) page： 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 ) page： 1-10 2011.7

On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs Reviewed

Tsubasa Sakata, Naoki Nishida, and Toshiki Sakabe

Proceedings of the 20th International Workshop on Functional and (Constraint) Logic Programming, Lecture Notes in Computer Science Vol. 6816 page： 138-155 2011.7

Language：English

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 Reviewed

Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, LIPICcs Vol. 10 page： 267-282 2011.5

Authorship：Lead author Language：English

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 Reviewed

Naoki Nishida and German Vidal

Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, LIPIcs Vol. 10 page： 283-298 2011.5

Authorship：Lead author Language：English

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

Tree Automata with Constraints and their Closure-Properties

Katsuhisa Kurahashi, Masahiko Sakai, Naoki Nishida, Futoshi Nomura, Toshiki Sakabe, Keiichirou Kusakari

IEICE Technical Rerport Vol. 110 ( 458 ) page： 61-66 2011.3

On non-termination proof of right-linear and right-shallow term rewriting systems based on forward narrowing

Tatsuya Hattori, Masahiko Sakai, Naoki Nishida, Keiichirou Kusakari and Toshiki Sakabe

IEICE Technical Report SS2010-44 Vol. 110 ( 336 ) page： 31-36 2010.12

Proposal of Abstract DPLL Algorithm Modulo Equational Theories

Tatsuya Baba, Toshiki Sakabe, Naoki Nishida, Keiichirou Kusakari, and Masahiko Sakai

IEICE Technical Report SS2010-36 Vol. 110 ( 227 ) page： 49-54 2010.10

On Turing Compeleteness of an Esoteric Language, Malbolge

Satoshi Nagasaka, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari, and Naoki Nishida

IEICE Technical Report SS2010-37 Vol. 110 ( 227 ) page： 55-60 2010.10

　 PREV - NEXT 　

<NISHIDA Naoki>

Papers - NISHIDA Naoki