Committee |
Date Time |
Place |
Paper Title / Authors |
Abstract |
Paper # |
SS, MSS |
2012-01-26 14:45 |
Kochi |
Kochi City Culture-Plaza Cul-Port |
On class of equation sets whose word problems are reducible to those of ground equation sets Toshimitsu Sakai, Masahiko Sakai, Toshiki Sakabe, Naoki Nishida, Keiichirou Kusakari (Nagoya Univ.) MSS2011-62 SS2011-47 |
The word problem of an equation set is to decide, given two terms, whether the two terms are equivalent under the equati... [more] |
MSS2011-62 SS2011-47 pp.45-49 |
SS, MSS |
2012-01-26 15:30 |
Kochi |
Kochi City Culture-Plaza Cul-Port |
On Rewriting Induction for Simply-typed Term Rewriting Systems Akira Ozeki, Keiichirou Kusakari, Tsubasa Sakata, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe (Nagoya Univ.) MSS2011-63 SS2011-48 |
Rewriting induction is a principle of proving inductive theorems by means of derivations obtained by applying inference ... [more] |
MSS2011-63 SS2011-48 pp.51-56 |
SS, MSS |
2012-01-26 16:00 |
Kochi |
Kochi City Culture-Plaza Cul-Port |
On Usable Rules under Argument Filterings in Higher-Order Rewrite Systems Kazuhiro Ooi, Keiichirou Kusakari, Masahiko Sakai, Toshiki Sakabe, Naoki Nishida (Nagoya Univ.) MSS2011-64 SS2011-49 |
The static dependency pair method is known as a powerful method for proving termination of higher-order rewrite systems ... [more] |
MSS2011-64 SS2011-49 pp.57-62 |
SS |
2011-10-28 12:15 |
Ishikawa |
JAIST |
Incorporating Elementary Symmetric Clauses into SAT Solvers with Two-Watched-Literal Scheme Yoshizane Hino, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari, Naoki Nishida (Nagoya Univ.) SS2011-38 |
Umano et al.\ introduced elementary symmetric clauses (ES-clauses) into CNF formula in 2010 as a method for improving SA... [more] |
SS2011-38 pp.67-72 |
SS |
2011-03-07 14:45 |
Okinawa |
Okinawa-ken Seinen Kaikan |
Tree Automata with Constraints and their Closure-Properties Katsuhisa Kurahashi, Masahiko Sakai, Naoki Nishida, Futoshi Nomura, Toshiki Sakabe, Keiichirou Kusakari (Nagoya Univ.) SS2010-63 |
Tree automata are useful in analyzing properties of term rewriting systems since the class of recognizable tree language... [more] |
SS2010-63 pp.61-66 |
SS |
2010-12-14 16:20 |
Gunma |
Ikaho-Onsen Hotel Tenbo |
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, Toshiki Sakabe (Nagoya Univ.) SS2010-44 |
Detecting non-termination of term rewriting systems based on forward narrowing is used in termination tools such as APro... [more] |
SS2010-44 pp.31-36 |
SS |
2010-10-15 11:00 |
Iwate |
Iwate Prefectural Univ. |
On DPLL Transition Systems Modulo Equational Theories Tatsuya Baba, Toshiki Sakabe, Naoki Nishida, Keiichirou Kusakari, Masahiko Sakai (Nagoya Univ.) SS2010-36 |
SMT solvers are tools for deciding satisfiability of formulas under given theories such as arrays, lists, queues and so ... [more] |
SS2010-36 pp.49-54 |
SS |
2010-10-15 11:30 |
Iwate |
Iwate Prefectural Univ. |
On Turing Completness of an Esoteric Language, Malbolge Satoshi Nagasaka, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari, Naoki Nishida (Nagoya Univ.) SS2010-37 |
Malbolge is known as one of the most esoteric programming languages. In this paper, we prove that Malbolge is weakly Tur... [more] |
SS2010-37 pp.55-60 |
SS |
2010-08-05 16:00 |
Hokkaido |
Asahikawa Shimin-Bunka-Kaikan (Civic Culture Hall) |
Argument Filterings and Usable Rules in Higher-Order Rewrite Systems Sho Suzuki, Keiichirou Kusakari (Nagoya Univ.), Frederic Blanqui (INRIA) SS2010-24 |
The static dependency pair method is a method for proving the termination
of higher-order rewrite systems {\em \`a la} ... [more] |
SS2010-24 pp.47-52 |
SS |
2009-12-17 15:50 |
Kagawa |
Kagawa Univ. |
Argument Filtering and Usable Rules in Higher-Order Rewrite Systems Sho Suzuki, Keiichirou Kusakari, Toshiki Sakabe, Masahiko Sakai, Naoki Nishida (Nagoya Univ.) SS2009-39 |
Simply-typed term rewriting systems (STRSs) and higher-order rewrite systems (HRSs)
have been proposed to extend term r... [more] |
SS2009-39 pp.25-30 |
SS |
2009-12-17 16:20 |
Kagawa |
Kagawa Univ. |
On Decidability of Context-Sensitive Termination for Right-Linear Right-Shallow Term Rewriting Systems Yoshimasa Mishuku, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari, Naoki Nishida (Nagoya Univ.) SS2009-40 |
It is known that termination and innermost termination are decidable for term rewriting systems (TRSs for short) whose d... [more] |
SS2009-40 pp.31-36 |
SS |
2009-12-18 08:40 |
Kagawa |
Kagawa Univ. |
Program Generation Based on Transformation of Conditional Equations Masanori Nagashima, Masahiko Sakai, Toshiki Sakabe, Naoki Nishida, Keiichirou Kusakari (Nagoya Univ.) SS2009-41 |
Program-generation system GeneSys, which we have ever proposed, generates executable programs from first order equationa... [more] |
SS2009-41 pp.37-42 |
CAS, NLP |
2009-01-22 10:00 |
Miyazaki |
|
A study of a bit-block circuit that realizes a 14-bit, 50MS/s, and 1.8V operational ADC Keiichirou Mizutani, Yasuhiro Sugimoto (Chuo Univ.) CAS2008-66 NLP2008-96 |
In a high-speed and high-precision pipelined A-D converter, an operational amplifier with high gain and high frequency b... [more] |
CAS2008-66 NLP2008-96 pp.19-24 |
SS |
2008-12-19 10:00 |
Kochi |
Kochi Univiersity of Technology |
Solving Satisfiability of CNF Formulas with Elementary Symmetric Functions Yohei Umano, Masahiko Sakai, Naoki Nishida, Toshiki Sakabe, Keiichirou Kusakari (Nagoya Univ.) SS2008-44 |
In recent years, several efficient SAT solvers, which decide satisfiability of boolean formulas, have been developed.
S... [more] |
SS2008-44 pp.31-36 |
SS |
2008-12-19 10:30 |
Kochi |
Kochi Univiersity of Technology |
Decidability of Termination Properties for Term Rewriting Systems Consisting of Shallow Dependency Pairs Keita Uchiyama, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari, Naoki Nishida (Nagoya Univ.) SS2008-45 |
In this paper, we show some decidable properties: termination, innermost termination and context-sensitive termination f... [more] |
SS2008-45 pp.37-42 |
SS |
2008-10-17 11:00 |
Yamanashi |
University of Yamanashi, Kofu Campus |
Behavior Analysis of Scalable CAN Protocol on a Bit-Error Channel Kenji Ukai, Toshiki Sakabe, Hiroaki Takada, Ryo Kurachi, Masahiko Sakai, Keiichirou Kusakari, Naoki Nishida (Nagoya Univ.) SS2008-37 |
Scalable CAN protocol is an improvement of the original CAN (Controller Area Network) protocol so that more than ten tim... [more] |
SS2008-37 pp.61-66 |
SS |
2008-07-31 17:30 |
Hokkaido |
Future University-Hakodate |
A Reduction Order for Orienting Equations in Theorem Proving of Constrained TRSs Naoki Nishida, Tsubasa Sakata, Masahiko Sakai, Keiichirou Kusakari, Toshiki Sakabe (Nagoya Univ.) SS2008-20 |
In automated theorem proving, we often face cases where the procedure
keeps running. To avoid such cases, the theorem p... [more] |
SS2008-20 pp.43-48 |
KBSE, SS |
2008-05-29 13:30 |
Miyazaki |
Miyazaki Citizens' Plaza |
On Rewriting Induction for Presburger-Constrained Term Rewriting Systems Tsubasa Sakata, Naoki Nishida, Toshiki Sakabe, Masahiko Sakai, Keiichirou Kusakari (Nagoya Univ.) SS2008-1 KBSE2008-1 |
A method for verifying equivalence between procedural programs has been proposed, where the implicit induction is extend... [more] |
SS2008-1 KBSE2008-1 pp.1-6 |
SS |
2008-03-03 11:00 |
Nagasaki |
Nagasaki Univ. |
Error Detection with Soft Typing for Dynamically Typed Languages Akihisa Yamada, Keiichirou Kusakari, Masahiko Sakai, Toshiki Sakabe, Naoki Nishida (Nagoya Univ.) SS2007-59 |
We propose a rich extension of soft typing for dynamically-typed languages like LISP,
and prove its soundness.
This e... [more] |
SS2007-59 pp.13-18 |
SS |
2008-03-03 13:05 |
Nagasaki |
Nagasaki Univ. |
Static Dependency Pair Method for Simply-Typed Term Rewriting and Related Techniques Keiichirou Kusakari, Masahiko Sakai (Nagoya Univ.) SS2007-61 |
We proposed a static dependency pair method,
which can effectively prove termination of functional programs.
Since the... [more] |
SS2007-61 pp.25-30 |