研究者詳細 - 酒井　正彦

論文 - 酒井　正彦

分割表示 >> ／全件表示 218 件中 1 - 218 件目

拍対応情報の利用による楽譜と実演奏の音符対応情報の自動生成法

佐藤宏志, 酒井正彦

情報処理学会技術報告　SIGMUS 142 巻 2025年3月

Solving Rep-Tile by Computers: Performance of Solvers and Analyses of Solutions 招待有り

Mutsunori Banbara, Kenji Hashimoto, Takashi Horiyama, Kosuke Oguri, Shin-ichi Minato, Masaaki Nishino, Masahiko Sakai, Ryuhei Uehara, Yushi Uno, and Norihito Yasuda

Algorithmic Foundations for Social Advancement 頁： 187 - 208 2025年3月

Tokenization of MIDI Sequences for Transcription 査読有り国際共著

Florent Jacquemard, Masahiko Sakai, Yosuke Amagasu

Proceedings of the International Conference on Technologies for Music Notation and Representation (TENOR 2024) 頁： 98 - 108 2024年4月

演奏MIDIのリズム量子化のためのトークン化の提案

天春陽介, 酒井正彦

情報処理学会技術報告　SIGMUS 2024年3月

Automatic Phrasing System for Expressive Performance Based on The Generative Theory of Tonal Music 査読有り

Madoka Goto, Masahiko Sakai, Satoshi Tojo

The 16th International Symposium on Computer Music Multidisciplinary Research 頁： 536 - 546 2023年9月

8+8=4: Formalizing Time Units to Handle Symbolic Music Durations 査読有り国際共著

Emmanouil Karystinaios, Francesco Foscarin, Florent Jacquemard, Masahiko Sakai, Satoshi Tojo and Gerhard Widmer

The 16th International Symposium on Computer Music Multidisciplinary Research 頁： 536 - 546 2023年9月

Ground Canonical Rewrite Systems Revisited 査読有り国際共著

Aart Middeldorp, Masahiko Sakai, Sarah Winkler

12th International Workshop on Confluence 頁： 44 - 48 2023年8月

SQL 型制約プログラミングシステム CombSQL+ の複数制約ソルバー連携

小菅脩司、酒井正彦、番原睦則

人工知能学会研究会資料 125 巻頁： 54 - 59 2023年8月

レプ・タイルの定式化を用いた各種ソルバの性能比較

番原睦則, 橋本健二, 堀山貴史, 湊真一, 中村駆, 西野正彬, 酒井正彦, 上原隆平, 宇野裕之, 安田宜仁

人工知能学会研究会資料人工知能基本問題研究会 119 巻 ( 0 ) 頁： 02 - 07 2022年1月

Solving Rep-tile by Computers: Performance of Solvers and Analyses of Solutions

Mutsunori Banbara, Kenji Hashimoto, Takashi Horiyama, Shin-ichi Minato, Kakeru Nakamura, Masaaki Nishino, Masahiko Sakai, Ryuhei Uehara, Yushi Uno, Norihito Yasuda

arXiv 2110.05184 2021年10月

SQL 型ソルバ CombSQL+による車両割当て問題の記述

井上和哉, 岸潤一郎, 酒井正彦

人工知能学会全国大会論文集 JSAI2021 巻 ( 0 ) 頁： 2E4OS13c01 - 2E4OS13c01 2021年6月

担当区分：最終著者,　責任著者記述言語：日本語掲載種別：研究論文（研究会，シンポジウム資料等）出版者・発行元：一般社団法人人工知能学会

<p>著者らはこれまで，SQL 言語を知っていれば組合せ最適化問題を比較的容易に記述し解くことができるようにすることを目的として，CombSQL+システムを開発した．まだこのシステムの利用例は少なく，応用例を増やし評価することが必要である. 本稿では，車両割当て問題に対するCombSQL+の記述を紹介する．ここで，些細とも思われる記述の差が，大きく実行性能に影響を及ぼす事が分かった．その理由について考察し，解決法のアイデアを述べる．</p>

DOI： 10.11517/pjsai.jsai2021.0_2e4os13c01

CiNii Research

Transformation of SQL-based Combinatorial Optimization Problems into Constraint Problems

Genki Sakanashi, Masahiko Sakai

SIG-FPAI-112 112 巻 ( 4 ) 頁： 6pages 2020年3月

Conditions for Confluence of Innermost Terminating Term Rewriting Systems 査読有り

Sayaka Ishizuki, Masahiko Sakai, and Michio Oyamaguchi

Applicable Algebra in Engineering, Communication and Computing 30 巻 ( 4 ) 頁： 349-360 2019年8月

A Parse-based Framework for Coupled Rhythm Quantization and Score Structuring 査読有り

Francesco Foscarin, Florent Jacquemard, Philippe Rigaux, and Masahido Sakai

Lecture Notes in Artificial Intelligence 11502 巻頁： 248-260 2019年6月

Transformation of Combinatorial Optimization Problems Written in Extended SQL into Constraint Problems 査読有り

Genki Sakanashi and Masahiko Sakai

Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming (PPDP 2018) 頁： 19:1-19:13 2018年9月

Reduced dependency spaces for existential parameterised Boolean equation system 査読有り

Yutaro Nagae, Masahiko Sakai

Electronic Proceedins in Theoretical Computer Science (EPTCS) 265 巻頁： 67-81 2018年1月

Transforming Dependency Chains of Constrained TRSs into Bounded Monotone Sequences of Integers 査読有り

Tomohiro Sasano, Naoki Nishida, Masahiko Sakai, and Tomoya Ueyama

Electronic Proceedins in Theoretical Computer Science (EPTCS) 265 巻頁： 82-97 2018年1月

Generating Equivalent Rhythmic Notations Based on Rhythm Tree Languages 査読有り

Florent Jacquemard, Adrien Ycart, and Masahiko Sakai

Proceedings of the International Conference on Technologies for Music Notation and Representation 頁： 145-153 2017年5月

Sound Structure-Preserving Transformation for Weakly-Left-Linear Deterministic Conditional Term Rewriting Systems 査読有り

Ryota Nakayama, Naoki Nishida and Masahiko Sakai

Electronic Proceedins in Theoretical Computer Science 235 巻頁： 62-77 2017年1月

An extension of proof graphs for disjunctive parameterised Boolean equation systems 査読有り

Yutaro Nagae, and Masahiko Sakai and Hiroyuki Seki

Electronic Proceedins in Theoretical Computer Science 235 巻頁： 46-61 2017年1月

An extension of proof graphs for disjunctive parameterised Boolean equation systems 査読有り

Yutaro Nagae, Masahiko Sakai

Informal Proceedings of the 3rd International Workshop on Rewriting Techniques f or Program Transformations and Evaluation (WPTE 2016) 頁： 3-14 2016年9月

Sound Structure-Preserving Transformation for Ultra-Weakly-Left-Linear Determini stic Conditional Term Rewriting Systems 査読有り

Ryota Nakayama, Naoki Nishida, Masahiko Sakai

Informal Proceedings of the 3rd International Workshop on Rewriting Techniques f or Program Transformations and Evaluation (WPTE 2016) 頁： 61-75 2016年9月

Conditions for confluence of innermost terminating term rewriting systems 査読有り

Sayaka Ishizuki, Masahiko Sakai, Michio Oyamaguchi

Proceedings of the 5th International Workshop on Confluence (IWC 2016) 頁： 65-69 2016年9月

Term Rewriting with Prefix Context Constraints and Regularity Preservation and Bottom-Up Strategies 査読有り

Yoshiharu Kojima, Masahiko Sakai, Florent Jacquemard

Lecture Notes in Computer Science (CADE 2015) 9195 巻頁： 137-151 2015年8月

Non-E-overlapping, weakly shallow, and non-collapsing TRSs are confluent 査読有り

Masahiko Sakai, Michio Oyamaguchi, Mizuhito Ogawa

Lecture Notes in Computer Science (CADE 2015) 9195 巻頁： 111-126 2015年8月

Construction of an ROBDD for a PB-constraint in band form and related techniques for PB-solvers 査読有り

Masahiko Sakai, Hidetomo Nabeshima

IEICE Transaction on Information and Systems E98-D 巻 ( 6 ) 頁： 1121-1127 2015年6月

Towards an Equational Theory of Rhythm Notation 査読有り

Pierre Donat-Bouillud, Florent Jacquemard, and Masahiko Sakai

Proc. of The Music Encoding Conference 2015 頁： 2 pages 2015年5月

Non-E-overlapping and weakly shallow TRSs are confluent 査読有り

Masahiko Sakai, Michio Oyamaguchi, Mizuhito Ogawa

Proceedings of the 3rd International Workshop on Confluence (IWC 2014) 頁： 34-38 2014年7月

Inverse Unfold Problem and Its Heuristic Solving 査読有り

Masanori Nagashima, Tomofumi Kato, Masahiko Sakai and Naoki Nishida

OASIcs 40 巻頁： 27-38 2014年7月

On Constructing Constrained Tree Automata Recognizing Ground Instances of Constrained Terms 査読有り

Naoki Nishida, Masahiko Sakai, Yasuhiro Nakano

Electronic Proceedings in Theoretical Computer Science 134 巻頁： 1-10 2013年10月

Improving Determinization of Grammar Programs for Program Inversion 査読有り

Minami Niwa, Naoki Nishida, and Masahiko Sakai

Lecture Notes in Computer Science 7844 巻頁： 137-154 2013年4月

Determinization of conditional term rewriting systems 招待有り査読有り

Masanori Nagashima, Masahiko Sakai, Toshiki Sakabe

Theoretical Computer Science 464 巻頁： 72-89 2012年12月

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

This paper discusses determinization of conditional term rewriting systems with oriented constructor rules. We present a rule-based transformation system, which transforms a non-deterministic one into a deterministic one, together with examples of the transformation. We prove that the transformation system is simulation sound and simulation complete. We also prove that the transformation system is complete for some class by introducing a strategy for the transformation system.

DOI： 10.1016/j.tcs.2012.09.005

Extending Matching Operation in Grammar Program for Program Inversion 査読有り

Minami Niwa, Naoki Nishida, and Masahiko Sakai

Proceedings of the 22nd International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2012) 頁： 130-139 2012年9月

Soundness of Unravelings for Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity 査読有り

Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

Logical Methods in Computer Science 8 巻 ( 3-4 ) 頁： 1-49 2012年8月

On determinazation of conditional term rewriting systems 査読有り

Masahiko Sakai

Proc. of 9th Asian Workshop on Foundation of Software (AWFS 2012) 頁： 18-19 2012年6月

Constrained Tree Automata and their Closure Properties 査読有り

Naoki Nishida, Futoshi Nomura, Katsuhisa Kurahashi and Masahiko Sakai

Proceedings of the 1st International Workshop on Trends in Tree Automata and Tree Transducers (TTATT 2012) 頁： 24-34 2012年6月

A Sound Type System for Typing Runtime Errors 査読有り

YAMADA Akihisa, KUSAKARI Keiichirou, SAKABE Toshiki, SAKAI Masahiko, NISHIDA Naoki

IPSJ Transactions on Programming 頁： to appear 2012年3月

Controlled Term Rewriting 査読有り

Florent Jacquemard, KOJIMA Yoshiharu, and SAKAI Masahiko

Proceedings of the 8th International Symposium on Frontiers of Combining Systems (FroCos 2011), LNCS 6989 巻頁： 179-194 2011年10月

Decidability of Reachability for Right-Shallow Context-Sensitive Term Rewriting Systems 査読有り

KOJIMA Yoshiharu, SAKAI Masahiko, NISHIDA Naoki, KUSAKARI Keiichirou, SAKABE Toshiki

IPSJ Transactions on Programming 4 巻 ( 4 ) 頁： 12-35 2011年9月

Soundness of Unravelings for Deterministic Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity 査読有り

NISHIDA Naoki, SAKAI Masahiko, SAKABE Toshiki

Proceedings of the 22nd International Conference on Rewriting Techniques and Applications (RTA 2011), LIPIcs 10 巻頁： 267-282 2011年5月

例外処理を持つ関数型プログラムの停止性・非停止性証明法査読有り

濱口毅, 酒井正彦, 馬場正貴, 阿草清滋

4 巻 ( 2 ) 頁： 1-19 2011年3月

制約付き項書換え系の書換え帰納法における補題等式の自動生成法査読有り

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

コンピュータソフトウェア 28 巻 ( 1 ) 頁： 173-189 2011年2月

順方向ナローイングに基づく右線形右シャロー項書換え系の非停止性証明について

服部達哉、酒井正彦、西田直樹、草刈圭一朗、坂部俊樹

電子情報通信学会技術研究報告 110 巻 ( 336 ) 頁： 31-36 2010年12月

等式理論を法とするDPLL遷移系について

馬場達也、坂部俊樹、西田直樹、草刈圭一朗、酒井正彦

電子情報通信学会技術研究報告 110 巻 ( 227 ) 頁： 49-54 2010年10月

難解言語Malbolgeのチューリング完全性について

長坂　哲、酒井正彦、坂部俊樹、草刈圭一朗、西田直樹

電子情報通信学会技術研究報告 110 巻 ( 227 ) 頁： 55-60 2010年10月

Weakly-non-overlapping non-collapsing shallow term rewriting systems are confluent 査読有り

Masahiko Sakai, Mizuhito Ogawa

Information Processing Letters 110 巻 ( 18-19 ) 頁： 795-844 2010年9月

等式論理を法とする抽象DPLLアルゴリズムの提案

馬場達也、坂部俊樹、酒井正彦、草刈圭一朗、西田直樹

平成22年度電気関係学会東海支部連合大会講演論文集頁： D3-4 2010年8月

制約付き項書換え系における関数の効率的な等価性検証

高桑一也、西田直樹、酒井正彦、坂部俊樹、草刈圭一朗

平成22年度電気関係学会東海支部連合大会講演論文集頁： D3-6 2010年8月

2カウンタ法に基づく基本対称節を持つCNF論理式のSATソルバ

日野善信、酒井正彦、草刈圭一朗、坂部俊樹、西田直樹

平成22年度電気関係学会東海支部連合大会講演論文集頁： D3-5 2010年8月

On Disproving Termiation of Constrained Term Rewriting Systems 査読有り

Naoki Nishida, Masahiko Sakai, Tatsuya Hattori

Proc. of Ninth International Workshop on Termination, (WST2010) 頁： 5 pages 2010年7月

Decidability of Termination and Innermost Termination for Term Rewriting Systems with Right-Shallow Dependency Pairs 査読有り

UCHIYAMA Keita, SAKAI Masahiko, SAKABE Toshiki

IEICE Transaction on Information and Systems E93-D 巻 ( 5 ) 頁： 953-962 2010年5月

Proving Injectivity of Functions via Program Inversion in Term Rewriting. 査読有り

Naoki Nishida and Masahiko Sakai

Proceedings of the 10th International Symposium on Functional and Logic Programming (FLOPS 2010),Lecture Notes in Computer Science 6009 巻頁： 288-303 2010年4月

Decidability of Termination and Innermost Termination for Term Rewriting Systems with Right-Shallow Dependency Pairs 査読有り

Keita Uchiyama, Masahiko Sakai, Toshiki Sakabe

IEICE Trans. on Information and Systems E93-D 巻 ( 5 ) 頁： 953-962 2010年1月

基本対象関数に基づく節を持つCNF論理式の充足可能性判定査読有り

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

電子情報通信学会論文誌 J93-D 巻 ( 1 ) 頁： 1-9 2010年1月

高階書換え系における引数切り落とし法と実効規則

鈴木翔、草刈圭一朗、坂部俊樹、酒井正彦、西田直樹

電子情報通信学会技術研究報告 109 巻 ( 343 ) 頁： 25-30 2009年12月

条件付き等式の変換に基づくプログラム生成

長島正憲，酒井正彦，坂部俊樹，西田直樹，草刈圭一朗

電子情報通信学会技術研究報告 109 巻 ( 343 ) 頁： 37-42 2009年12月

右線形右シャローな項書換え系における文脈依存停止性の決定可能性について

御宿義勝、酒井正彦、坂部俊樹、草刈圭一朗、西田直樹

電子情報通信学会技術研究報告 109 巻 ( 343 ) 頁： 31-36 2009年12月

Static Dependency Pair Method based on Strong Computability for Higher-Order Rewrite Systems 査読有り

Yasuo Isogai, Keiichirou Kusakari, Masahiko Sakai, Frederic Blanqui

IEICE Trans. on Information and Systems E92-D 巻 ( 10 ) 頁： 235-247 2009年10月

制約付き項書換え系の書換え帰納法における補題等式の自動生成法

中林直生，西田直樹，草刈圭一朗，坂部俊樹，酒井正彦

日本ソフトウェア科学会第26回大会論文集 7B-12 巻頁： 1-14 2009年9月

Context-sensitive Innermost Reachability is Decidable for Linear Right-shallow Term Rewriting Systems 査読有り

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

IPSJ Transactions of Programming 2 巻 ( 3 ) 頁： 20-32 2009年7月

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

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

情報処理学会論文誌プログラミング 2 巻 ( 2 ) 頁： 80-96 2009年3月

Recognizability of Redexes for Higher-Order Rewrite Systems 査読有り

Hideto Kasuya, Masahiko Sakai, Kiyoshi Agusa

IPSJ Transactions of Programming 2 巻 ( 2 ) 頁： 166-175 2009年3月

Head-Needed Strategy of Higher-Order Rewrite Systems and Its Decidable Classes 査読有り

Hideto Kasuya, Masahiko Sakai, Kiyoshi Agusa

IPSJ Transactions of Programming 2 巻 ( 2 ) 頁： 144-165 2009年3月

Static Dependency Pair Method for Simply-Typed Term Rewriting and Related Techniques 査読有り

Keiichirou Kusakari, Masahiko Sakai

IEICE Trans. on Information and Systems E92-D 巻 ( 2 ) 頁： 235-247 2009年2月

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

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

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

*Innermost Reachability and Context Sensitive Reachability Properties are Decidable for Linear Right-Shallow Term Rewriting Systems 査読有り

Yoshiharu Kojima, Masahiko Sakai

Proc. of 19th Int'l Conference on Rewriting Techniqes and Applications, Hagenberg RTA2008, LNCS 5117 巻頁： 187-201 2008年7月

記述言語：英語

A reachability problem is a problem used to decide whether s is reachable to t by R or not for a given two terms s, t and a term rewriting system R. Since it is known that this problem is undecidable, effort has been devoted to finding subclasses of term rewriting systems in which the eachabilit
y is decidable. However few works on decidability exist for innermost reduction strategy or context-sensitive rewriting.

In this paper, we show that innermost reachability and
context-sensitive reachability are decidable for linear right-shallow term rewriting systems. Our approach is based on the tree automata technique that is commonly
used for analysis of reachability and its related properties.

Completion as Post-Process in Program Inversion of Injective Functions 査読有り

Naoki Nishida, Masahiko Sakai

"Proc. of 8th International Workshop on Reduction Strategies in Rewriting and Programming, Hagenberg (WRS2008)" 頁： 61-75 2008年7月

Decidability of Innermost Termination and Context-Sensitive Termination for Semi-Constructor Term Rewriting Systems 査読有り

Keita Uchiyama, Masahiko Sakai and Toshiki Sakabe

Electronic Notes in Theoretical Computer Science 204 巻 ( 4 ) 頁： 21-34 2008年4月

*Undecidable Properties on Length-Two String Rewriting Systems 査読有り

Masahiko Sakai and Wang Yi

Electronic Notes in Theoretical Computer Science 204 巻 ( 4 ) 頁： 53-69 2008年4月

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

Length-two string rewriting systems are length-preserving string rewriting systems that consist of length-two rules. This paper shows that confluence, termination, left-most termination and right-most termination are undecidable
properties for length-two string rewriting systems. These results mean that these properties are undecidable for
the class of linear term rewriting systems in which depth-two variables are allowed in both-hand sides of rules.

Error Detection with Soft Typing for Dynamically Typed Language

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

IEICE Technical Report 107 巻 ( 505 ) 頁： 7-12 2008年3月

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

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

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

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

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

電子情報通信学会技術研究報告 107 巻 ( 505 ) 頁： 25-30 2008年3月

Static Dependency Pair Method for Simply-Typed Term Rewriting and Related Techniques

"Keiichirou Kusakari, Masahiko Sakai"

IEICE Technical Report 107 巻 ( 505 ) 頁： 19-24 2008年3月

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

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

電子情報通信学会技術研究報告 107 巻 ( 392 ) 頁： 43-48 2007年12月

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

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

電子情報通信学会技術研究報告 107 巻 ( 392 ) 頁： 73-78 2007年12月

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

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

電子情報通信学会技術研究報告 107 巻 ( 275 ) 頁： 1-6 2007年10月

*Enhancing Dependency Pair Method using Strong Computability in Simply-Typed Term Rewriting 査読有り

Keiichirou Kusakari, Masahiko Sakai

Applicable Algebra in Engineering, Communication and Computing 18 巻 ( 5 ) 頁： 407-431 2007年10月

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

We enhance the dependency pair method in order to prove termination using recursive structure analysis in simply-typed term rewriting systems, which is one of the computational models of functional programs. The primary advantage of our method is that one can exclude higher-order variables which are difficult to analyze theoretically, from recursive structure analysis. The key idea of our method is to analyze recursive structure from the viewpoint of strong computability. This property was introduced for proving termination in typed lambda-calculus, and is a stronger condition than the property of termination. The difficulty in incorporating this concept into recursive structure analysis is that because it is defined inductively over type structure, it is not closed under the subterm relation. This breaks the correspondence between strong computability and recursive structure. In order to guarantee the correspondence, we propose plain function-passing as a restriction, which is satisfied by
many non-artificial functional programs.

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

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

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

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

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

電子情報通信学会技術研究報告 107 巻 ( 176 ) 頁： 1-6 2007年8月

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

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

電子情報通信学会技術研究報告 107 巻 ( 176 ) 頁： 7-12 2007年8月

Decidability of Innermost Termination and Context-Sensitive Termination for Semi-Constructor Term Rewriting Systems 査読有り

"Keita Uchiyama, Masahiko Sakai and Toshiki Sakabe"

"Proc. of 7th International Workshop on Reduction Strategies in Rewriting and Programming, Paris (WRS2007)" 頁： 16-27 2007年6月

Static Dependency Pair Method for Proving Termination of Higher-Order Rewriting Systems

"Kiichirou Kusakari, Yasuo Isogai, Masahiko Sakai, Toshiki Sakabe and Naoki Nishida"

107 巻 ( 99 ) 頁： 17-22 2007年6月

二階の書換え系における引数切り落とし法

磯谷泰巨、草刈圭一朗、酒井正彦、坂部俊樹、西田直樹

電子情報通信学会技術研究報告 107 巻 ( 99 ) 頁： 23-28 2007年6月

Convergent Term Rewriting Systems for Inverse Computation of Injective Functions 査読有り

"WaNaoki Nishida, Masahiko Sakai, and Terutoshi Kato"

"Proc. of Ninth International Workshop on Termination, Paris (WST2007)" 頁： 77-81 2007年6月

Undecidable Properties on Length-Two String Rewriting Systems 査読有り

Masahiko Sakai and Wang Yi

"Proc. of 7th International Workshop on Reduction Strategies in Rewriting and Programming, Paris (WRS2007)" 頁： 43-57 2007年6月

Decidability of Innermost Termination for Semi-Constructor Term Rewriting Systems

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

"RIMS Technical Report, Kyoto Universty" 1554 巻頁： 166-170 2007年5月

Confluence of Length Preserving String Rewriting System is Undecidable

"Yi Wang, Masahiko Sakai, Naoki Nishida, Toshiki Sakabe and Keiichirou Kusakari"

"RIMS Technical Report, Kyoto Universty" 1554 巻頁： 171-177 2007年5月

単純型項書き換え系上の依存対法における実効規則と直積型項へのラベル付け査読有り

櫻井敬大、草刈圭一朗、酒井正彦、坂部俊樹、西田直樹

電子情報通信学会論文誌 J90-D 巻 ( 4 ) 頁： 978-989 2007年4月

単純型項書換え系における定理自動証明系HOPSYS

蒲田明憲，草刈圭一朗，西田直樹，酒井正彦，坂部俊樹

電子情報通信学会技術研究報告 106 巻 ( 424 ) 頁： 7-12 2006年12月

手続き型プログラムから書換え系への変換に基づくソフトウェア検証の試み

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

電子情報通信学会技術研究報告 106 巻 ( 324 ) 頁： 7-12 2006年10月

GeneSysによるプログラム生成例とIntroduction規則の追加

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

電子情報通信学会技術研究報告 106 巻 ( 324 ) 頁： 37-42 2006年10月

例外処理付きオブジェクト指向言語における情報流の安全性解析

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

電子情報通信学会技術研究報告 106 巻 ( 324 ) 頁： 13-18 2006年10月

高階関数機能を持つ項書換え系のコンパイル

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

平成18年度電気関係学会東海支部連合大会講演論文集頁： O-437 2006年9月

所属制約を持つ条件付き項書換え系の紐解き変換

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

平成18年度電気関係学会東海支部連合大会講演論文集頁： O-438 2006年9月

*Decidability of Termination Left-Linear Shallow TRSs and Related Systems for Semi-Constructor TRSs 査読有り

Wang Yi and Masahiko Sakai

Proc. of 17th Int'l Conference on Rewriting Techniqes and Applications, Seattle RTA2006, LNCS 4098 巻頁： 343-356 2006年8月

記述言語：英語

"We consider several classes of term rewriting systems and prove that termination is decidable for these classes. By showing the cycling property of infinite dependency chains, we prove that termination is decidable for semi-constructor case, which is a superclass of right-ground TRSs. By analyzing argument propagation cycles in the dependency graph, we show that termination is also decidable for left-linear shallow TRSs. Moreover we extend these by combining these two techniques."

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

"Naoki Nishida, Tomohiro Mizutani, and Masahiko Sakai"

"Proc. of 6th International Workshop on Reduction Strategies in Rewriting and Programming, Seattle (WRS2006)" 頁： 34-48 2006年8月

On Non-looping Term Rewriting 査読有り

Wang Yi and Masahiko Sakai

"Proc. of Eighth International Workshop on Termination, Seattle (WST2006)" 頁： 17-21 2006年8月

等式付き書換え系の等式数を削減する変換

三浦浩一，西田直樹，酒井正彦，坂部俊樹，草刈圭一朗

電子情報通信学会技術研究報告 106 巻 ( 120 ) 頁： 7-12 2006年6月

単純型項書換え系上の依存対法における実行規則と直積型項へのラベル付け

櫻井敬大，草刈圭一朗，酒井正彦，坂部俊樹，西田直樹

電子情報通信学会技術研究報告 106 巻 ( 120 ) 頁： 13-18 2006年6月

紐解かれた項書換え系の文脈依存条件の除去のための変換

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

京都大学数理解析研究所講究録 1489 巻頁： 195-201 2006年5月

強計算依存対法による高階書換え系の停止性証明

磯谷泰巨，草刈圭一朗，酒井正彦，坂部俊樹，西田直樹

電子情報通信学会技術研究報告 106 巻 ( 15 ) 頁： 31-36 2006年4月

項正規表現に基づくSpi計算の機密性検証

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

電子情報通信学会技術研究報告 105 巻 ( 596 ) 頁： 35-40 2006年2月

関数プログラムの停止性証明に関する辞書式経路順序

"星野由美, 草刈圭一朗, 酒井正彦, 坂部俊樹, 西田直樹"

電子情報通信学会技術研究報告 105 巻 ( 597 ) 頁： 13-18 2006年2月

Primitive Indeuctive Theorems Bridge Implicit Induction methods and Inductive Theorems in Higher-Order Rewriting 査読有り

"Keiichirou Kusakari, Masahiko Sakai, Toshiki Sakabe"

IEICE Trans. on Information and Systems E88-D 巻 ( 12 ) 頁： 2715-2726 2005年12月

Decidability of Termination fo Left-Linear Shallow Term Rewriting Systems and Related

"Yi Wang, Masahiko Sakai, Naoki Nishida, Keiichiro Kusakari, Toshiki Sakabe"

IEICE Technical Report 105 巻 ( 499 ) 頁： 9-13 2005年12月

分散JoinJAVAプログラムの通信エラーに対する型判定システム

佐伯昌樹，坂部俊樹，酒井正彦，草刈圭一朗，西田直樹

電子情報通信学会技術報告 105 巻 ( 491 ) 頁： 25-30 2005年12月

強計算性による単純型項書換え系の依存対法の改良

105 巻 ( 491 ) 頁： 13-18 2005年12月

暗号プロトコル記述からカラーペトリネットへの変換による機密性検証

奥谷大介，坂部俊樹，酒井正彦，草刈圭一朗，西田直樹

電子情報通信学会技術報告 105 巻 ( 490 ) 頁： 19-24 2005年12月

重なりを持つTRSにおける最外戦略の完全性について

"岩田篤史，酒井正彦，西田直樹，草刈圭一朗, 西田直樹"

電子情報通信学会技術報告 SS2005-46 105 巻 ( 331 ) 頁： 39-44 2005年10月

カラーペトリネットを用いた暗号プロトコルの安全性検証

奥谷大介、坂部俊樹、酒井正彦、草刈圭一朗、西田直樹

平成17年度電気関係学会東海支部連合大会講演論文集頁： O-198 2005年9月

分散JoinJAVAプログラムの正常実行判定のための型システム

佐伯昌樹、坂部俊樹、酒井正彦、草刈圭一朗、西田直樹

平成17年度電気関係学会東海支部連合大会講演論文集頁： O-306 2005年9月

関数プログラムの再帰構造解析と強計算性に基づく十分完全性の証明法査読有り

櫻井敬大、草刈圭一朗、西田直樹、酒井正彦、坂部俊樹

情報科学技術レターズ LA-001 巻頁： 1-4 2005年9月

構成子項書換え系の逆計算プログラムの生成査読有り

西田直樹、酒井正彦、坂部俊樹

電子情報通信学会論文誌 J88-D-I 巻 ( 8 ) 頁： 1171-1183 2005年8月

Decidability of Termination for Semi-Constructor Term Rewriting Systems

"Yi Wang, Masahiko Sakai, Naoki Nishida, Keiichirou Kusakari, Toshiki Sakabe"

"Tech. Reort of IEICE, SS2005-27" 105 巻 ( 228 ) 頁： 13-18 2005年8月

難読プログラミング言語Malbolgeにおけるプログラム構成手法

"飯澤恒, 坂部俊樹, 酒井正彦, 草刈圭一朗, 西田直樹"

電子情報通信学会技術報告 SS2005-22 巻頁： 25-30 2005年6月

弱最内戦略を完全にする項書換え系の等価変換

"岡本晃治, 酒井正彦, 西田直樹, 草刈圭一朗"

京都大学数理解析研究所講究録 1426 巻頁： 119-125 2005年4月

Partial Inversion of Constructor Term Rewriting Systems 査読有り

"Naoki Nishida, Masahiko Sakai, Toshiki Sakabe"

"Proc. of 16th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science" 3647 巻頁： 264-278 2005年4月

配列を扱う非線形先頭再帰プログラムからの再帰除去

"高須洋平, 酒井正彦, 西田直樹, 草刈圭一朗, 坂部俊樹"

京都大学数理解析研究所講究録 1426 巻頁： 39-44 2005年4月

項到達可能性の判定における成長TRSに対する手法と正規化規則による手法の関係

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

京都大学数理解析研究所講究録 1426 巻頁： 106-112 2005年4月

変換と部分評価に基づく非左辺正規なメタ項の停止性証明

"蛸島洋明, 酒井正彦, 坂部俊樹, 西田直樹, 草刈圭一朗"

京都大学数理解析研究所講究録 1426 巻頁： 113-118 2005年4月

On Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems 査読有り

"Masahiko Sakai, Keiichirou Kusakari"

IEICE Trans. on Information and Systems E88-D 巻 ( 3 ) 頁： 583-593 2005年3月

項の全正規形を探索するためのTRSコンパイラ

岩田篤史、草刈圭一朗、酒井正彦、坂部俊樹

平成16年度電気関係学会東海支部連合大会講演論文集頁： 363 2004年9月

項書換え系と木オートマトンを用いた共通鍵方式暗号プロトコルの検証法

奥谷大介、坂部俊樹、酒井正彦

平成16年度電気関係学会東海支部連合大会講演論文集頁： 352 2004年9月

高階書換え系の決定可能な計算戦略について

粕谷英人、酒井正彦、阿草清滋

電子情報通信学会技術報告 SS2004-6 巻頁： 1-6 2004年8月

On Simulation-Completeness of Unraveling for Conditional Term Rewriting Systems

"Naoki Nishida, Masahiko Sakai, Toshiki Sakabe"

Technical Report of IEICE SS2004-6 巻頁： 25-30 2004年8月

On Simulation-Completeness of Unraveling for Conditional Term Rewriting Systems

Naoki Nishida, Masahiko Sakai, Toshiki Sakabe

LA symposium 頁： 7.1-7.6 2004年7月

限量子付き等式理論の変換に基づく仕様からのプログラム生成査読有り

長島正徳、酒井正彦、坂部俊樹、草刈圭一朗

コンピュータソフトウェア 21 巻 ( 4 ) 頁： 49-54 2004年7月

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

本論文では、既知関数を記述する項書換え系と生成したい未知関数の仕様を論理式の集合とみなして、その変換に基づくプログラム自動生成を試みる。まず、等式と論理和・論理積・限量子からなる論理式の集合を対象とする変換系を提案する。次に、変換により得られた論理式集合から元の論理式集合の全ての論理式が証明可能であることを示す。このことは、変換によって得られた論理式集合が実行可能なプログラムとみなせるときに、そのプログラムが仕様を満足することを保障している。最後に、プログラム自動生成の一例を挙げる。

左辺が一致するオーバレイ性を持つ左線形ＴＲＳの正規化戦略

水野健一、草刈圭一朗、酒井正彦、坂部俊樹

京都大学数理解析研究所講究録 1375 巻頁： 247-252 2004年5月

右辺のみに現れる変数を持つ線形構成子項書換え系の計算の効率化査読有り

西田直樹、酒井正彦、坂部俊樹

コンピュータソフトウェア 21 巻 ( 3 ) 頁： 40-47 2004年5月

非完全な仕様における振舞等価性の自動証明法

山本友和、草刈圭一朗、酒井正彦、坂部俊樹

電子情報通信学会技術報告 COMP2003 巻 ( 66 ) 頁： 29-36 2003年12月

Characterizing Inductive Theorems by Extensional Initial Models in a Higher-Order Equational Logic

"Keiichiro Kusakari, Masahiko Sakai, Toshiki Sakabe"

46 巻 ( 9 ) 2003年10月

メタ項書き換え計算における左辺正規性を持つメタ項の停止性について、

蛸島洋明、酒井正彦、坂部俊樹

平成15年度電気関係学会東海支部連合大会講演論文集頁： 565 2003年10月

最内書換えに基づく項書換え系の完全な書換え戦略

岡本晃治、酒井正彦、坂部俊樹

平成15年度電気関係学会東海支部連合大会講演論文集頁： 564 2003年10月

右辺のみに現れる変数を持つ項書換え系の計算モデル査読有り

西田直樹、酒井正彦、坂部俊樹

コンピュータソフトウェア 20 巻 ( 5 ) 頁： 85-89 2003年9月

右辺のみに現れる変数を持つ右線形構成子項書換え系の計算の効率化

西田直樹、酒井正彦、坂部俊樹

日本ソフトウェア科学会第20回大会論文集 441-445 巻 2003年9月

高階項書換え系の決定可能性問題のためのNk木オートマトンとその性質、

粕谷英人、酒井正彦、阿草清滋

日本ソフトウェア科学会第20回大会論文集頁： 436-440 2003年9月

限量子付き等式理論の変換に基づく仕様からのプログラム生成、

長島正徳、酒井正彦、坂部俊樹、草刈圭一朗

日本ソフトウェア科学会第20回大会論文集頁： 431-435 2003年9月

右辺のみに現れる変数を持つ右線形オーバーレイ項書換え系の最左最内ナローイングによる正規形の計算

西田直樹、酒井正彦、坂部俊樹

2003年度夏のLAシンポジウム頁： 24.1-24.6 2003年8月

右辺のみに現れる変数を持つ右線形オーバーレイ項書換え系の最左最内ナローイングによる正規形の計算

西田直樹、酒井正彦、坂部俊樹

2003年度夏のLAシンポジウム頁： 24.1-24.6 2003年8月

Innermost Reductions Find All Normal Forms on Right-Linear Terminating Overlay TRSs 査読有り

"Masahiko Sakai, Kouji Okamoto, Toshiki Sakabe"

Proc. of 3rd Int'l Workshop on Reduction Strategies in Rewriting and Programming WRS'03 巻頁： 79-88 2003年6月

Narrowing-based Simulation of Term Rewriting Systems with Extra Variables and its Termination Proof 査読有り

"Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe"

Proc. of 12th Int'l Workshop on Functional and (Constraint) Logic Programming WFLP'03 巻頁： 198-211 2003年6月

右辺のみに現れる変数を持つ項書換え系のナローイングに基づく実効的書き換えとその停止性

西田直樹、酒井正彦、坂部俊樹

京都大学数理解析研究所講究録 1325 巻頁： 238-243 2003年5月

再帰型をもつオブジェクト指向計算モデルにおける例外処理の型付

堀江美保子、酒井正彦、坂部俊樹

京都大学数理解析研究所講究録 1325 巻頁： 104-109 2003年5月

オブジェクト指向計算モデルにおける例外処理機能の型付査読有り

堀江美保子、酒井正彦、坂部俊樹

コンピュータソフトウェア 20 巻 ( 2 ) 頁： 54-58 2003年3月

Descendants and Head Normalization of Higher-Order Rewrite Systems 査読有り

"Hideto Kasuya, Masahiko Sakai, Kiyoshi Agusa"

Lecture Notes in Computer Science 2441 巻 2002年9月

On Proving Termination of Higher-Order Rewrite Systems by Dependency Pair technique 査読有り

"Masahiko Sakai, Keiichirou Kusakari"

"Proc. of the First International Workshop on Higher-Order Rewriting (HOR'02), Copenhagen, Denmark" 頁： 25 2002年7月

PT関数の逆関数を定義するTRSの生成査読有り

西田直樹、酒井正彦、坂部俊樹

コンピュータソフトウェア 19 巻 ( 1 ) 頁： 29-33 2002年1月

優先順序付き項書換え系の頭必須戦略の決定可能性

鈴木剛、酒井正彦、坂部俊樹

電子情報通信学会技術報告 COMP2001-80 巻頁： 49-55 2002年1月

潜在帰納法による弱完全振舞仕様に対する振舞等価性の自動証明

加納康資、酒井正彦、坂部俊樹

電子情報通信学会技術報告 COMP2001-79 巻頁： 41-47 2002年1月

高階書換え系におけるディセンダントと頭必須書換えの頭正規化性

粕谷英人、酒井正彦、阿草清滋

電子情報通信学会技術報告 COMP2001-82 巻頁： 65-72 2002年1月

n箇所パターン照合関数のDeforestationに基づく効率化

中村敏広、酒井正彦、坂部俊樹

シンポジウム，情報基礎理論ワークショップ 2002年

n箇所パターン照合関数のDeforestationに基づく効率化

中村敏広、酒井正彦、坂部俊樹

シンポジウム，情報基礎理論ワークショップ 2002年

Generation of a TRS Implementing the Inverses of the Functions with Specified Arguments Fixed

"Naoki Nishida, Masahiko Sakai, Toshiki Sakabe"

Technical Report of IEICE COMP2001-67 巻頁： 33-40 2001年12月

Generation of Inverse Term Rewriting Systems for Pure Treeless Functions 査読有り

"Naoki Nishida, Masahiko Sakai, Toshiki Sakabe"

"Proc. of the International workshop on Rewriting in Proof and Computaion, Sendai, Japan" 頁： 188-198 2001年10月

On New Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems 査読有り

"Masahiko Sakai, Keiichirou Kusakari"

"Proc. of the International Workshop on Rewriting in Proof and Computation (RPC'01), Sendai, Japan" 頁： 176-187 2001年10月

An Extension of Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems 査読有り

"Masahiko Sakai, Yoshitsugu Watanabe, Toshiki Sakabe"

IEICE Trans. on Information and Systems E84-D 巻 ( 8 ) 頁： 1025-1032 2001年8月

PT関数の逆関数を定義する条件付きTRSの生成

西田直樹、酒井正彦、坂部俊樹

電子情報通信学会技術報告 COMP2001-14 巻頁： 9-16 2001年6月

メタ項書換え計算における規則中に規則を含む直交メタ項の合流性査読有り

洪順姫、酒井正彦、坂部俊樹

コンピュータソフトウェア 17 巻 ( 6 ) 頁： 47-51 2000年11月

ユーザにごみ集めを意識させないCライブラリの設計法

西田直樹、酒井正彦、坂部俊樹

電子情報通信学会技術報告 SS2000-9 巻頁： 25-32 2000年5月

Confluence of Weakly Orthogonal CTRSs with Extra Variables

Ould Seyid Ahmed, Masahiko Sakai, Toshiki Sakabe

LA symposium 2000年

Confluence of Weakly Orthogonal CTRSs with Extra Variables

"Ould Seyid Ahmed, Masahiko Sakai, Toshiki Sakabe"

LA symposium 2000年

直交メタ項書換え計算のデベロップメントと合流性

洪順姫、酒井正彦、坂部俊樹

電子情報通信学会技術報告 COMP99-9 巻頁： 65-70 1999年4月

順序ソートの自動推論とラベル付けに基づく合流性判定への応用

宮下大、酒井正彦、坂部俊樹

計算モデルとアルゴリズム、数理解析研究所講究録 1093 巻頁： 136-141 1999年2月

項集合書換え系の完備化について

粕谷英人、酒井正彦、山本晋一郎、阿草清滋

電子情報通信学会技術報告 SS98-66 巻頁： 25-31 1998年12月

Semantics and Strong Sequentiality of Priority Term Rewriting Systems 査読有り

"Masahiko Sakai, Yoshihito Toyama"

Theoretical Computer Science 208 巻頁： 87-110 1998年11月

An Improved Recursive Decomposition Ordering for Higher-Order Rewrite Systems 査読有り

"Munehiro Iwami, Masahiko Sakai, Yoshihito Toyama"

IEICE Trans. on Information and Systems E81-D 巻 ( 9 ) 頁： 988-996 1998年9月

Index Reduction of Overlapping Strongly Sequential Systems 査読有り

"Takashi Nagaya, Masahiko Sakai, Yoshihito Toyama"

IEICE Trans. on Information and Systems E81-D 巻 ( 5 ) 頁： 419-426 1998年5月

項書換え系の拡張された階層的結合における停止性のモジュラー性

大野健治、河口信夫、酒井正彦、坂部俊樹、稲垣康善

電子情報通信学会技術報告 SS97-84 巻頁： 57-61 1998年3月

依存対に基づく高階項書換え系の停止性証明

渡辺啓嗣、河口信夫、酒井正彦、坂部俊樹、稲垣康善

電子情報通信学会技術報告 SS97-85 巻頁： 63-70 1998年3月

IIn型条件付き書換え系の合流性について

西村徹、酒井正彦、坂部俊樹

電子情報通信学会技術報告 COMP97-84 巻頁： 45-49 1998年1月

Left-Incompatible Term Rewriting Systems and Functional Strategy 査読有り

Masahiko Sakai

IEICE Trans. on Information and Systems E80-D 巻 ( 12 ) 頁： 1176-1182 1997年12月

項集合書換え系とその合流性査読有り

粕谷英人，酒井正彦，山本晋一郎，阿草清滋

電子情報通信学会誌 J80-D-I 巻 ( 4 ) 頁： 325-334 1997年4月

An Improved Recursive Decomposition Ordering for Higher-Order Rewrite Systems

"Munehiro Iwami, Masahiko Sakai, Yoshihito Toyama"

"Tech. Rep., IEICE" COMP96-73 巻頁： 17-24 1997年1月

条件付き書換え系の合流性について査読有り

高橋宜孝，酒井正彦，外山芳人

電子情報通信学会誌 J79-D-I 巻 ( 11 ) 頁： 897-902 1996年11月

Semantics and Strong Sequentiality of Priority Term Rewriting Systems 査読有り

"Masahiko Sakai, Yoshihito Toyama"

"Proc. on Rewriting Techniques and Applications at New Brunswick NJ USA, LNCS" 1103 巻頁： 377-391 1996年7月

Index reduction of Overlapping Strong Sequential Systems

"Takashi Nagaya, Masahiko Sakai, Yoshihito Toyama"

"Tech. Rep., IEICE" COMP96-32 巻頁： 39-48 1996年7月

Church-Rosser Property of Finite Ranked Terms of Non-Linear Term Rewriting Systems

"Keiichiro Kusakari, Masahiko Sakai, Yoshihito Toyama"

LA Symposium 頁： 160-165 1996年7月

Index reduction of Overlapping Strong Sequential Systems

"Takashi Nagaya, Masahiko Sakai, Yoshihito Toyama"

LA Symposium 頁： 154-165 1996年7月

高階項書換え系の停止性について

岩見宗弘，酒井正彦，外山芳人

シンポジウム，情報基礎理論ワークショップ頁： 55-60 1996年7月

項書換え系のAC停止性について

中野賢司，酒井正彦，外山芳人

電子情報通信学会技術報告 COMP95-104 巻頁： 69-78 1996年3月

NVNF-sequeentiality of Left-linear Term Rewriting Systems

"Takashi Nagaya, Masahiko Sakai, Yoshihito Toyama"

"Kyokyuroku, Kyoto University" 950 巻頁： 153-159 1996年2月

高階項書換え系の停止性について

岩見宗弘，酒井正彦，外山芳人

電子情報通信学会技術報告 COMP95-85 巻頁： 113-121 1996年1月

非線形項書換え系の合流性について

草刈圭一朗，酒井正彦，外山芳人

電子情報通信学会技術報告 COMP95-86 巻頁： 123-129 1996年1月

The Semantics of Priority Term Rewriting Systems and their Strong Sequentiality

"Masahiko Sakai, Yoshihito Toyama"

"Technical report, IEICE" SS95-40 巻頁： 31-38 1996年1月

The Functional Strategy: the Extended Left-incompatible Systems

Masahiko Sakai

"Technical Report, IEICE" SS95-17 巻頁： 55-62 1995年7月

NVNF-sequeentiality of Left-linear Term Rewriting Systems

"Takashi Nagaya, Masahiko Sakai, Yoshihito Toyama"

"Proc. of RIMS Workshop on Theory of Rewriting Systems and its Applications, Kyokyuroku, Kyoto University" 918 巻頁： 109-117 1995年7月

共有メモリ型並列計算機における項書換え系の実現方式査読有り

山本晋一郎，石川亮，酒井正彦，阿草清滋

電子情報通信学会論文誌 J78-D-I 巻 ( 6 ) 頁： 559-562 1995年6月

形式的仕様を用いた再利用モデル査読有り

川北誠，酒井正彦，山本晋一郎，阿草清滋

情報処理学会論文誌 36 巻 ( 5 ) 頁： 1050-1058 1995年5月

エラーつき代数的仕様とエラー記述の自動付加査読有り

"濱口毅, 酒井正彦, 山本晋一郎, 阿草清滋"

電子情報通信学会論文誌 J78-D-I 巻 ( 3 ) 頁： 323-330 1995年3月

項書換え系の合流性を保存する合併条件について

北原彰，酒井正彦，外山芳人

情報処理学会，プログラミング -言語・基礎・実践- 研究会 20 巻 ( 2 ) 頁： 11-20 1995年1月

仕様に基づく部品再利用法とその適用

川北誠，酒井正彦，山本晋一郎，阿草清滋

第1回ソフトウェア工学の基礎ワークショップ FOSE94 巻 1994年12月

条件つき項書換え系の合流性について

高橋宜孝，酒井正彦，外山芳人

電子情報通信学会技術報告 COMP94-65 巻頁： 105-111 1994年11月

NVNF-逐次系におけるインデックスの決定可能性

長谷崇，酒井正彦，外山芳人

電子情報通信学会，コンピュテーション研究会 COMP94-63 巻頁： 87-94 1994年11月

項集合書換え系の合流性について

粕谷英人，酒井正彦，山本晋一郎，阿草清滋

電子情報通信学会，ソフトウェアサイエンス研究会 SS94-14 巻頁： 17-24 1994年7月

On Term Set Rewriting System

"Masahiko Sakai, Hideto Kasuya, Shinichiro Yamamoto and Kiyoshi Agusa"

LA Symposium 頁： 45-48 1994年7月

Similarity on Algebraic Specifications toward Specification Databases

Masahiko Sakai

"Technical Report, JAIST" IS-RR-94-0012S 巻頁： 1-20 1994年5月

項の集合の書換え系とKnuth-Bendixの完備化に関する考察

粕谷英人，酒井正彦，山本晋一郎，阿草清滋

電子情報通信学会，ソフトウェアサイエンス研究会 SS93-41 巻頁： 17-22 1994年1月

ソフトウェア操作言語の提案

吉田敦，山本晋一郎，酒井正彦，阿草清滋

電子情報通信学会，ソフトウェアサイエンス研究会 SS92-18 巻頁： 1-8 1993年1月

代数的仕様へのエラー記述の自動付加について

濱口毅，酒井正彦，山本晋一郎，阿草清滋

電子情報通信学会，ソフトウェアサイエンス研究会 SS92-26 巻頁： 25-32 1993年1月

代数的仕様の検証のための被覆集合帰納法査読有り

酒井正彦，坂部俊樹，稲垣康善

電子情報通信学会論文誌 J75-D-I 巻 ( 3 ) 頁： 170-179 1992年3月

Similarity on Algebraic Specifications toward Specification Databases

"Masahiko Sakai, Soichi Matsui, Shinichiro Yamamoto, Kiyoshi Agusa"

LA Symposium 頁： 30-35 1992年2月

代数的仕様の検証のための被覆集合帰納法

酒井正彦，坂部俊樹，稲垣康善

情報基礎理論ワークショップ，LAシンポジュウム頁： 12-17 1991年2月

コンパイラの代数的仕様記述と自動生成査読有り

酒井正彦，坂部俊樹，稲垣康善

電子情報通信学会論文誌 J73-D-I 巻 ( 12 ) 頁： 979-989 1990年12月

代数的仕様記述法に基づく言語処理系の自動生成システムLass 査読有り

酒井正彦，坂部俊樹，稲垣康善

電子情報通信学会論文誌 J73-D-1 巻 ( 10 ) 頁： 829-838 1990年10月

代数的仕様の検証のための被覆集合帰納法

酒井正彦，坂部俊樹，稲垣康善

電子情報通信学会，コンピュテーション研究会 COMP90-5 巻 1990年5月

コンパイル機能を持つTRSインタプリタの実現

酒井正彦，坂部俊樹，稲垣康善

電子情報通信学会，コンピュテーション研究会 COMP88-93 巻 1989年2月

TRSインタプリタの並列最外戦略実現法

山本晋一郎，酒井正彦，坂部俊樹，稲垣康善

電子情報通信学会，コンピュテーション研究会 COMP88-94 巻 1989年2月

代数的仕様における帰納的性質の証明法

酒井正彦，坂部俊樹，稲垣康善

電子情報通信学会，コンピュテーション研究会 COMP88-86 巻頁： 83-92 1989年1月

抽象データ型の代数的仕様の直接実現系Cdimple 査読有り

酒井正彦，坂部俊樹，稲垣康善

コンピュータソフトウェア 4 巻 ( 4 ) 頁： 16-27 1987年10月

An Algebraic Approach to Specification of Programming Languages and Automatic Generation of Language Processors 査読有り

"Yasuyoshi Inagaki, Hidehiko Kita, Masahiko Sakai, Toshiki Sakabe"

Proceedings of Regional Symposium on Computer Science and its Applications in Thai 頁： 35-1-35-25 1987年1月

抽象データ型の代数的仕様の直接実現系Cdimple

酒井正彦，坂部俊樹，稲垣康善

電子通信学会技術研究報告，コンピュテーション研究会 COMP96-67 巻頁： 61-69 1987年1月

An Algebraic Approach to Specification of Programming Languages and Automatic Generation of Language Processors

"Yasuyoshi Inagaki, Hidehiko Kita, Masahiko Sakai, Toshiki Sakabe"

"Technical Research Report, Nagoya University" 8601 巻 1986年11月

抽象データ型直接実現システムCdimple

酒井正彦，坂部俊樹，稲垣康善

ソフトウエア科学会，関数的プログラミング研究会 FP-86-07 巻頁： 122-127 1986年11月

コンパイラの代数的仕様記述とその自動生成

酒井正彦，坂部俊樹，稲垣康善

情報処理学会研究報告，プログラミング言語研究会 86-PL-8-1 巻頁： 1-9 1986年10月

コンパイラの代数的仕様記述法

酒井正彦，坂部俊樹，稲垣康善

電子通信学会技術研究報告，ソフトウエアサイエンス研究会 SS86-9 巻頁： 1-6 1986年7月

代数的手法に基づくプログラミング言語の仕様記述法と処理系の自動生成

稲垣康善，北英彦，酒井正彦，坂部俊樹

情報処理学会，知識情報処理シンポジウム論文集頁： 165-174 1985年9月

プログラミング言語の代数的仕様記述からのコンパイラ自動生成に関する基礎的考察

酒井正彦，北英彦，坂部俊樹，稲垣康善

言語理論とオートマトン理論シンポジウム論文集頁： 98-101 1985年7月

プログラミング言語の代数的仕様記述からのコンパイラ自動生成

酒井正彦，北英彦，坂部俊樹，稲垣康善

電子通信学会技術研究報告，オートマトンと言語研究会 AL85-10 巻頁： 1-10 1985年5月

　前のページ - 次のページ　

<酒井 正彦>

論文 - 酒井 正彦

<酒井　正彦>

論文 - 酒井　正彦