2021/04/20 更新

写真a

アオト タカヒト
青戸 等人
Takahito Aoto
所属
教育研究院 自然科学系 情報電子工学系列 教授
工学部 工学科 教授
職名
教授
外部リンク

学位

  • 博士(情報科学) ( 1997年3月   北陸先端科学技術大学院大学 )

  • 学士(工学) ( 1992年3月   東京大学 )

研究分野

  • 情報通信 / 情報学基礎論

経歴(researchmap)

  • 新潟大学   工学部 工学科   教授

    2017年4月 - 現在

      詳細を見る

  • 新潟大学   工学部 情報工学科 コンピュータサイエンス   教授

    2015年10月 - 2017年3月

      詳細を見る

  • 東北大学   電気通信研究所   准教授

    2007年4月 - 2015年9月

      詳細を見る

  • 東北大学   電気通信研究所   助教授

    2004年3月 - 2007年3月

      詳細を見る

  • 東北大学   電気通信研究所   講師

    2003年1月 - 2004年2月

      詳細を見る

  • 群馬大学   工学部   助手

    1998年3月 - 2002年12月

      詳細を見る

  • 北陸先端科学技術大学院大学   情報科学研究科   助手

    1997年4月 - 1998年2月

      詳細を見る

▶ 全件表示

経歴

  • 新潟大学   工学部 工学科   教授

    2017年4月 - 現在

  • 新潟大学   コンピュータサイエンス   教授

    2015年10月 - 2017年3月

学歴

  • 北陸先端科学技術大学院大学   Graduate School, Division of Information Science  

    - 1997年3月

      詳細を見る

    国名: 日本国

    researchmap

  • 東京大学   工学部  

    - 1992年3月

      詳細を見る

    国名: 日本国

    researchmap

所属学協会

▶ 全件表示

 

論文

  • Confluence Competition 2018

    Takahito Aoto, Makoto Hamana, Nao Hirokawa, Aart Middeldorp, Julian Nagele, Naoki Nishida, Kiraku Shintani, Harald Zankl

    Proc. of 3rd FSCD, Leibniz International Proceedings in Informatics108   32:1 - 32:5   2018年7月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)   出版者・発行元:Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik  

    DOI: 10.4230/LIPIcs.FSCD.2018.32

    researchmap

  • Improving rewriting induction approach for proving ground confluence 査読

    Takahito Aoto, Yoshihito Toyama, Yuta Kimura

    Leibniz International Proceedings in Informatics, LIPIcs84   7:1 - 7:18   2017年9月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)   出版者・発行元:Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing  

    In (Aoto&amp
    Toyama, FSCD 2016), a method to prove ground confluence of many-sorted term rewriting systems based on rewriting induction is given. In this paper, we give several methods that add wider flexibility to the rewriting induction approach for proving ground confluence. Firstly, we give a method to deal with the case in which suitable rules are not presented in the input system. Our idea is to construct additional rewrite rules that supplement or replace existing rules in order to obtain a set of rules that is adequate for applying rewriting induction. Secondly, we give a method to deal with non-orientable constructor rules. This is accomplished by extending the inference system of rewriting induction and giving a sufficient criterion for the correctness of the system. Thirdly, we give a method to deal with disproving ground confluence. The presented methods are implemented in our ground confluence prover AGCP and experiments are reported. Our experiments reveal the presented methods are effective to deal with problems for which state-of-The-Art ground confluence provers can not handle.

    DOI: 10.4230/LIPIcs.FSCD.2017.7

    Scopus

    researchmap

  • Parallel closure theorem for left-linear nominal rewriting systems 査読

    Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama

    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)10483   115 - 131   2017年

     詳細を見る

    記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)   出版者・発行元:Springer Verlag  

    Nominal rewriting has been introduced as an extension of first-order term rewriting by a binding mechanism based on the nominal approach. In this paper, we extend Huet’s parallel closure theorem and its generalisation on confluence of left-linear term rewriting systems to the case of nominal rewriting. The proof of the theorem follows a previous inductive confluence proof for orthogonal uniform nominal rewriting systems, but the presence of critical pairs requires a much more delicate argument. The results include confluence of left-linear uniform nominal rewriting systems that are not α-stable and thus are not represented by any systems in traditional higher-order rewriting frameworks.

    DOI: 10.1007/978-3-319-66167-4_7

    Scopus

    researchmap

  • Ground confluence prover based on rewriting induction 査読

    Takahito Aoto, Yoshihito Toyama

    Leibniz International Proceedings in Informatics, LIPIcs52   33:1 - 33:12   2016年6月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)   出版者・発行元:Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing  

    Ground confluence of term rewriting systems guarantees that all ground terms are confluent. Recently, interests in proving confluence of term rewriting systems automatically has grown, and confluence provers have been developed. But they mainly focus on confluence and not ground confluence. In fact, little interest has been paid to developing tools for proving ground confluence automatically. We report an implementation of a ground confluence prover based on rewriting induction, which is a method originally developed for proving inductive theorems.

    DOI: 10.4230/LIPIcs.FSCD.2016.33

    Scopus

    researchmap

  • Critical pair analysis in nominal rewriting 査読

    Takaki Suzuki, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama

    EPiC Series in Computing39   156 - 168   2016年3月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)   出版者・発行元:EasyChair  

    researchmap

  • Nominal confluence tool 査読

    Takahito Aoto, Kentaro Kikuchi

    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)9706   173 - 182   2016年

     詳細を見る

    記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)   出版者・発行元:Springer Verlag  

    Nominal rewriting is a framework of higher-order rewriting introduced in (Fernández, Gabbay &amp
    Mackie, 2004
    Fernández &amp
    Gabbay, 2007). Recently, (Suzuki et al., 2015) revisited confluence of nominal rewriting in the light of feasibility. We report on an implementation of a confluence tool for (non-closed) nominal rewriting, based on (Suzuki et al., 2015) and succeeding studies.

    DOI: 10.1007/978-3-319-40229-1_12

    Scopus

    researchmap

  • 書き換え規則の重なりに基づく到達可能性判定法 査読

    島貫健太郎, 青戸等人, 外山 芳人

    コンピュータソフトウェア33 ( 3 ) 93 - 107   2016年

     詳細を見る

    記述言語:日本語   掲載種別:研究論文(学術雑誌)   出版者・発行元:ソフトウェア科学会  

    DOI: 10.11309/jssst.33.3_93

    researchmap

  • Confluence of orthogonal nominal rewriting systems revisited 査読

    Takaki Suzuki, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama

    Leibniz International Proceedings in Informatics, LIPIcs36   301 - 317   2015年6月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)   出版者・発行元:Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing  

    Nominal rewriting systems (Fernández, Gabbay &amp
    Mackie, 2004
    Fernández &amp
    Gabbay, 2007) have been introduced as a new framework of higher-order rewriting systems based on the nominal approach (Gabbay &amp
    Pitts, 2002
    Pitts, 2003), which deals with variable binding via permutations and freshness conditions on atoms. Confluence of orthogonal nominal rewriting systems has been shown in (Fernández &amp
    Gabbay, 2007). However, their definition of (non-trivial) critical pairs has a serious weakness so that the orthogonality does not actually hold for most of standard nominal rewriting systems in the presence of binders. To overcome this weakness, we divide the notion of overlaps into the self-rooted and proper ones, and introduce a notion of α-stability which guarantees α-equivalence of peaks from the self-rooted overlaps. Moreover, we give a sufficient criterion for uniformity and α-stability. The new definition of orthogonality and the criterion offer a novel confluence condition effectively applicable to many standard nominal rewriting systems. We also report on an implementation of a confluence prover for orthogonal nominal rewriting systems based on our framework.

    DOI: 10.4230/LIPIcs.RTA.2015.301

    Scopus

    researchmap

  • Correctness of Context-Moving Transformations for Term Rewriting Systems 査読

    Koichi Sato, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama

    LOGIC-BASED PROGRAM SYNTHESIS AND TRANSFORMATION (LOPSTR 2015)9527   331 - 345   2015年

     詳細を見る

    記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)   出版者・発行元:SPRINGER INT PUBLISHING AG  

    Proofs by induction are often incompatible with functions in tail-recursive form as the accumulator changes in the course of unfolding the definitions. Context-moving and context-splitting (Giesl, 2000) for functional programs transform tail-recursive programs into non tail-recursive ones which are more suitable for proofs by induction and thus for verification. In this paper, we formulate context-moving and context-splitting transformations in the framework of term rewriting systems, and prove their correctness with respect to both eager evaluation semantics and initial algebra semantics under some conditions on the programs to be transformed. The conditions for the correctness with respect to initial algebra semantics can be checked by automated methods for inductive theorem proving developed in the field of term rewriting systems.

    DOI: 10.1007/978-3-319-27436-2_20

    Web of Science

    researchmap

  • Confluence Competition 2015

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

    AUTOMATED DEDUCTION - CADE-259195   101 - 104   2015年

     詳細を見る

    記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)   出版者・発行元:SPRINGER-VERLAG BERLIN  

    Confluence is one of the central properties of rewriting. Our competition aims to foster the development of techniques for proving/disproving confluence of various formalisms of rewriting automatically. We explain the background and setup of the 4th Confluence Competition.

    DOI: 10.1007/978-3-319-21401-6_5

    Web of Science

    researchmap

  • 項書き換えシステムの変換を利用した帰納的定理自動証明

    佐藤洸一, 菊池健太郎, 青戸等人, 外山芳人

    コンピュータソフトウェア32 ( 1 ) 179 - 193   2015年

     詳細を見る

    記述言語:日本語   掲載種別:研究論文(学術雑誌)  

    DOI: 10.11309/jssst.32.1_179

    researchmap

  • Decision procedures for proving inductive theorems without induction 査読

    Takahito Aoto, Sorin Stratulat

    PPDP 2014 - Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming   237 - 248   2014年9月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)   出版者・発行元:Association for Computing Machinery, Inc  

    Automated inductive reasoning for term rewriting has been extensively studied in the literature. Classes of equations and term rewriting systems (TRSs) with decidable inductive validity have been identified and used to automatize the inductive reasoning. We give procedures for deciding the inductive validity of equations in some standard TRSs on natural numbers and lists. Contrary to previous decidability results, our procedures can automatically decide without involving induction reasoning the inductive validity of arbitrary equations for these TRSs, that is, without imposing any syntactical restrictions on the form of equations. We also report on the complexity of our decision procedures. These decision procedures are implemented in our automated provers for inductive theorems of TRSs and experiments are reported.

    DOI: 10.1145/2643135.2643156

    Scopus

    researchmap

  • Proving confluence of term rewriting systems via persistency and decreasing diagrams 査読

    Takahito Aoto, Yoshihito Toyama, Kazumasa Uchida

    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)8560   46 - 60   2014年

     詳細を見る

    記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)   出版者・発行元:Springer Verlag  

    The decreasing diagrams technique (van Oostrom, 1994) has been successfully used to prove confluence of rewrite systems in various ways
    using rule-labelling (van Oostrom, 2008), it can also be applied directly to prove confluence of some linear term rewriting systems (TRSs) automatically. Some efforts for extending the rule-labelling are known, but non-left-linear TRSs are left beyond the scope. Two methods for automatically proving confluence of non-(left-)linear TRSs with the rule-labelling are given. The key idea of our methods is to combine the decreasing diagrams technique with persistency of confluence (Aoto &amp
    Toyama, 1997). © 2014 Springer International Publishing Switzerland.

    DOI: 10.1007/978-3-319-08918-8_4

    Scopus

    researchmap

  • 書き換え帰納法に基づく帰納的定理の決定可能性

    中嶋辰成, 青戸等人, 外山芳人

    コンピュータソフトウェア31 ( 3 ) 294 - 306   2014年

     詳細を見る

    記述言語:日本語   掲載種別:研究論文(学術雑誌)  

    DOI: 10.11309/jssst.31.3_294

    researchmap

  • ボトムアップ最内項書き換えシステムの最内到達可能性

    高橋翔大, 青戸等人, 外山芳人

    コンピュータソフトウェア31 ( 1 ) 75 - 89   2014年

     詳細を見る

    記述言語:日本語   掲載種別:研究論文(学術雑誌)  

    DOI: 10.11309/jssst.31.1_75

    researchmap

  • Termination of Rule-Based Calculi for Uniform Semi-Unification. 査読

    Takahito Aoto, Munehiro Iwami

    LATA   56 - 67   2013年

     詳細を見る

    記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)  

    DOI: 10.1007/978-3-642-37064-9_7

    researchmap

  • 永続性に基づく項書き換えシステムの合流性証明法

    鈴木翼, 青戸等人, 外山芳人

    コンピュータソフトウェア30 ( 3 ) 148 - 162   2013年

     詳細を見る

    記述言語:日本語   掲載種別:研究論文(学術雑誌)  

    DOI: 10.11309/jssst.30.3_148

    researchmap

  • 片側減少ダイアグラム法による項書き換えシステムの可換性証明法

    的場正樹, 青戸等人, 外山芳人

    コンピュータソフトウェア30 ( 1 ) 187 - 202   2013年

     詳細を見る

    記述言語:日本語   掲載種別:研究論文(学術雑誌)  

    DOI: 10.11309/jssst.30.1_187

    researchmap

  • Disproving Confluence of Term Rewriting Systems by Interpretation and Ordering. 査読

    Takahito Aoto

    FroCos   311 - 326   2013年

     詳細を見る

    記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)  

    DOI: 10.1007/978-3-642-40885-4_22

    researchmap

  • Rational term rewriting revisited: Decidability and confluence 査読

    Takahito Aoto, Jeroen Ketema

    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)7562   172 - 186   2012年

     詳細を見る

    記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)  

    We consider a variant of rational term rewriting as first introduced by Corradini et al., i.e., we consider rewriting of (infinite) terms with a finite number of different subterms. Motivated by computability theory, we show a number of decidability results related to the rewrite relation and prove an effective version of a confluence theorem for orthogonal systems. © 2012 Springer-Verlag.

    DOI: 10.1007/978-3-642-33654-6_12

    Scopus

    researchmap

  • A reduction-preserving completion for proving confluence of non-terminating term rewriting systems 査読

    Takahito Aoto, Yoshihito Toyama

    Logical Methods in Computer Science8 ( 1 )   2012年

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)  

    We give a method to prove con uence of term rewriting systems that contain non-terminating rewrite rules such as commutativity and associativity. Usually, con uence of term rewriting systems containing such rules is proved by treating them as equational term rewriting systems and considering E-critical pairs and/or termination modulo E. In contrast, our method is based solely on usual critical pairs and it also (partially) works even if the system is not terminating modulo E. We first present con uence criteria for term rewriting systems whose rewrite rules can be partitioned into a terminating part and a possibly non-terminating part. We then give a reduction-preserving completion procedure so that the applicability of the criteria is enhanced. In contrast to the well-known Knuth- Bendix completion procedure which preserves the equivalence relation of the system, our completion procedure preserves the reduction relation of the system, by which con uence of the original system is inferred from that of the completed system. © A REDUCTION-PRESERVING COMPLETION FOR PROVING CONFLUENCE.

    DOI: 10.2168/LMCS-8(1:31)2012

    Scopus

    researchmap

  • 多項式サイズ正規形を保証する項書き換えシステムの経路順序

    磯部耕己, 青戸等人, 外山芳人

    コンピュータソフトウェア29 ( 1 ) 176 - 190   2012年

     詳細を見る

    記述言語:日本語   掲載種別:研究論文(学術雑誌)  

    DOI: 10.11309/jssst.29.1_176

    researchmap

  • 無限項書き換えシステムにおける強頭部正規化可能性および一般生成性の自動反証

    岩見宗弘, 青戸等人

    コンピュータソフトウェア29 ( 1 ) 211 - 239   2012年

     詳細を見る

    記述言語:日本語   掲載種別:研究論文(学術雑誌)  

    DOI: 10.11309/jssst.29.1_211

    researchmap

  • Preface.

    Takahito Aoto, Aart Middeldorp

    Theor. Comput. Sci.464   1 - 2   2012年

     詳細を見る

    記述言語:英語  

    DOI: 10.1016/j.tcs.2012.09.009

    researchmap

  • A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems 査読

    Takahito Aoto, Yoshihito Toyama

    22ND INTERNATIONAL CONFERENCE ON REWRITING TECHNIQUES AND APPLICATIONS (RTA'11)10   91 - 106   2011年

     詳細を見る

    記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)   出版者・発行元:SCHLOSS DAGSTUHL, LEIBNIZ CENTER INFORMATICS  

    We give a method to prove confluence of term rewriting systems that contain non-terminating rewrite rules such as commutativity and associativity. Usually, confluence of term rewriting systems containing such rules is proved by treating them as equational term rewriting systems and considering E-critical pairs and/or termination modulo E. In contrast, our method is based solely on usual critical pairs and usual termination. We first present confluence criteria for term rewriting systems whose rewrite rules can be partitioned into terminating part and possibly non-terminating part. We then give a reduction-preserving completion procedure so that the applicability of the criteria is enhanced. In contrast to the well-known Knuth-Bendix completion procedure which preserves the equivalence relation of the system, our completion procedure preserves the reduction relation of the system, by which confluence of the original system is inferred from that of the completed system.

    DOI: 10.4230/LIPIcs.RTA.2011.91

    Web of Science

    researchmap

  • Natural Inductive Theorems for Higher-Order Rewriting 査読

    Takahito Aoto, Toshiyuki Yamada, Yuki Chiba

    22ND INTERNATIONAL CONFERENCE ON REWRITING TECHNIQUES AND APPLICATIONS (RTA'11)10   107 - 121   2011年

     詳細を見る

    記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)   出版者・発行元:SCHLOSS DAGSTUHL, LEIBNIZ CENTER INFORMATICS  

    The notion of inductive theorems is well-established in first-order term rewriting. In higher-order term rewriting, in contrast, it is not straightforward to extend this notion because of extensionality (Meinke, 1992). When extending the term rewriting based program transformation of Chiba et al. (2005) to higher-order term rewriting, we need extensibility, a property stating that inductive theorems are preserved by adding new functions via macros. In this paper, we propose and study a new notion of inductive theorems for higher-order rewriting, natural inductive theorems. This allows to incorporate properties such as extensionality and extensibility, based on simply typed S-expression rewriting (Yamada, 2001).

    DOI: 10.4230/LIPIcs.RTA.2011.107

    Web of Science

    researchmap

  • Program Transformation Templates for Tupling Based on Term Rewriting 査読

    Yuki Chiba, Takahito Aoto, Yoshihito Toyama

    IEICE TRANSACTIONS ON INFORMATION AND SYSTEMSE93D ( 5 ) 963 - 973   2010年5月

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)   出版者・発行元:IEICE-INST ELECTRONICS INFORMATION COMMUNICATIONS ENG  

    Chiba et al. (2006) proposed a framework of program transformation of term rewriting systems by developed templates. Contrast to the previous framework of program transformation by templates based on lambda calculus, this framework provides a method to verify the correctness of transformation automatically. Tupling (Bird, 1980) is a well-known technique to eliminate redundant recursive calls for improving efficiency of programs. In Chiba et al's framework, however, one can not use tuple symbols to construct developed templates. Thus their framework is not capable of tupling transformations. In this paper, we propose a more flexible notion of templates so that a wider variety of transformations, including tupling transformations, can be handled.

    DOI: 10.1587/transinf.E93.D.963

    Web of Science

    researchmap

  • AUTOMATED CONFLUENCE PROOF BY DECREASING DIAGRAMS BASED ON RULE-LABELLING 査読

    Takahito Aoto

    PROCEEDINGS OF THE 21ST INTERNATIONAL CONFERENCE ON REWRITING TECHNIQUES AND APPLICATIONS (RTA'10)6   7 - 16   2010年

     詳細を見る

    記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)   出版者・発行元:SCHLOSS DAGSTUHL, LEIBNIZ CENTER INFORMATICS  

    Decreasing diagrams technique (van Oostrom, 1994) is a technique that can be widely applied to prove confluence of rewrite systems. To directly apply the decreasing diagrams technique to prove confluence of rewrite systems, rule-labelling heuristic has been proposed by van Oostrom (2008). We show how constraints for ensuring confluence of term rewriting systems constructed based on the rule-labelling heuristic are encoded as linear arithmetic constraints suitable for solving the satisfiability of them by external SMT solvers. We point out an additional constraint omitted in (van Oostrom, 2008) that is needed to guarantee the soundness of confluence proofs based on the rule-labelling heuristic extended to deal with non-right-linear rules. We also present several extensions of the rule-labelling heuristic by which the applicability of the technique is enlarged.

    DOI: 10.4230/LIPIcs.RTA.2010.7

    Web of Science

    researchmap

  • 反証機能付き書き換え帰納法のための補題自動生成法

    嶌津聡志, 青戸等人, 外山 芳人

    コンピュータソフトウェア26 ( 2 ) 41 - 55   2009年

     詳細を見る

    記述言語:日本語   掲載種別:研究論文(学術雑誌)  

    DOI: 10.11309/jssst.26.2_41

    researchmap

  • Proving Confluence of Term Rewriting Systems Automatically. 査読

    Takahito Aoto, Junichi Yoshida, Yoshihito Toyama

    RTA   93 - 102   2009年

     詳細を見る

    記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)  

    DOI: 10.1007/978-3-642-02348-4_7

    researchmap

  • Argument Filterings and Usable Rules for Simply Typed Dependency Pairs. 査読

    Takahito Aoto, Toshiyuki Yamada

    FroCoS   117 - 132   2009年

     詳細を見る

    記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)  

    DOI: 10.1007/978-3-642-04222-5_7

    researchmap

  • 項書き換えシステムの合流性自動判定

    吉田順一, 青戸等人, 外山芳人

    コンピュータソフトウェア26 ( 2 ) 76 - 92   2009年

     詳細を見る

    記述言語:日本語   掲載種別:研究論文(学術雑誌)  

    DOI: 10.11309/jssst.26.2_76

    researchmap

  • Soundness of rewriting induction based on an abstract principle

    Takahito Aoto

    IPSJ Transactions on Programming49 ( SIG 1 ) 28 - 38   2008年

     詳細を見る

  • Sound Lemma Generation for Proving Inductive Validity of Equations. 査読

    Takahito Aoto

    FSTTCS   13 - 24   2008年

     詳細を見る

    記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)  

    DOI: 10.4230/LIPIcs.FSTTCS.2008.1737

    researchmap

  • Automatic construction of program transformation templates

    Yuki Chiba, Takahito Aoto, Yoshihito Toyama

    IPSJ Transactions on Programming49 ( SIG 1 (PRO 35) ) 14 - 27   2008年

     詳細を見る

  • 項書き換えシステムの合流性自動判定

    吉田順一, 青戸等人, 外山芳人

    情報技術レターズ6   31 - 34   2007年

     詳細を見る

  • Program Transformation by Templates: A Rewriting Framework

    Yuki Chiba, Takahito Aoto, Yoshihito Toyama

    IPSJ Transactions on Programming47   52 - 65   2006年

     詳細を見る

  • Dealing with Non-orientable Equations in Rewriting Induction. 査読

    Takahito Aoto

    RTA   242 - 256   2006年

     詳細を見る

    記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)  

    DOI: 10.1007/11805618_18

    researchmap

  • RAPT: A Program Transformation System Based on Term Rewriting. 査読

    Yuki Chiba, Takahito Aoto

    RTA   267 - 276   2006年

     詳細を見る

    記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)  

    DOI: 10.1007/11805618_20

    researchmap

  • パターンに基づくプログラム変換における列変数の導入

    千葉勇輝, 青戸等人, 外山芳人

    情報技術レターズ   5 - 8   2005年

     詳細を見る

  • Dependency Pairs for Simply Typed Term Rewriting. 査読

    Takahito Aoto, Toshiyuki Yamada

    RTA   120 - 134   2005年

     詳細を見る

    記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)  

    DOI: 10.1007/978-3-540-32033-3_10

    researchmap

  • Program transformation by templates based on term rewriting. 査読

    Yuki Chiba, Takahito Aoto, Yoshihito Toyama

    PPDP   59 - 69   2005年

     詳細を見る

    記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)  

    DOI: 10.1145/1069774.1069780

    researchmap

  • Inductive Theorems for Higher-Order Rewriting. 査読

    Takahito Aoto, Toshiyuki Yamada, Yoshihito Toyama

    RTA   269 - 284   2004年

     詳細を見る

    記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)  

    DOI: 10.1007/978-3-540-25979-4_19

    researchmap

  • 高階関数型プログラムにおける帰納的定理証明

    青戸等人, 山田俊行, 外山芳人

    情報技術レターズ2   21 - 22   2003年

     詳細を見る

  • Termination of Simply Typed Term Rewriting by Translation and Labelling. 査読

    Takahito Aoto, Toshiyuki Yamada

    RTA   380 - 394   2003年

     詳細を見る

    記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)  

    DOI: 10.1007/3-540-44881-0_27

    researchmap

  • 単純型付き項書換え系における停止性の自動証明

    青戸等人, 山田俊行

    情報処理学会論文誌:プログラミング44 ( SIG 4 (PRO 17) ) 67 - 77   2003年

     詳細を見る

  • Solution to the Problem of Zantema on a Persistent Property of Term Rewriting Systems. 査読

    Takahito Aoto

    Journal of Functional and Logic Programming2001 ( 11 )   2001年

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)  

    researchmap

  • On the finite model property of intuitionistic modal logics over MIPC 査読

    T Aoto, H Shirasu

    MATHEMATICAL LOGIC QUARTERLY45 ( 4 ) 435 - 448   1999年

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)   出版者・発行元:WILEY-V C H VERLAG GMBH  

    MIPC is a well-known intuitionistic modal logic of Prior (1957) and Bull (1966). It is shown that every normal intuitionistic modal logic L over MIPC has the finite model property whenever L is Kripke-complete and universal.

    DOI: 10.1002/malq.19990450402

    Web of Science

    researchmap

  • Uniqueness of normal proofs in implicational intuitionistic logic 査読

    Takahito Aoto

    Journal of Logic, Language and Information8 ( 2 ) 217 - 242   1999年

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)   出版者・発行元:Springer Netherlands  

    A minimal theorem in a logic L is an L-theorem which is not a non-trivial substitution instance of another L-theorem. Komori (1987) raised the question whether every minimal implicational theorem in intuitionistic logic has a unique normal proof in the natural deduction system NJ. The answer has been known to be partially positive and generally negative. It is shown here that a minimal implicational theorem A in intuitionistic logic has a unique β-normal proof in NJ whenever A is provable without non-prime contraction. The non-prime contraction rule in NJ is the implication introduction rule whose cancelled assumption differs from a propositional variable and appears more than once in the proof. Our result improves the known partial positive solutions to Komori's problem. Also, we present another simple example of a minimal implicational theorem in intuitionistic logic which does not have a unique βη-normal proof in NJ. © 1999 Kluwer Academic Publishers.

    DOI: 10.1023/A:1008254111992

    Scopus

    researchmap

  • Termination Transformation by Tree Lifting Ordering. 査読

    Takahito Aoto, Yoshihito Toyama

    RTA   256 - 270   1998年

     詳細を見る

    記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)  

    DOI: 10.1007/BFb0052375

    researchmap

  • Solution to the Problem of Zantema on a Persistent Property of Term Rewriting Systems. 査読

    Takahito Aoto

    PLILP/ALP   250 - 265   1998年

     詳細を見る

    記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)  

    DOI: 10.1007/BFb0056618

    researchmap

  • Some Characterizations of Implicational Formulas in the Intuitionistic Logic

    Takahito Aoto

        1997年3月

     詳細を見る

    記述言語:英語   掲載種別:学位論文(博士)  

    researchmap

  • On composable properties of term rewriting systems 査読

    Takahito Aoto, Yoshihito Toyama

    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)1298   114 - 128   1997年

     詳細を見る

    記述言語:英語   掲載種別:研究論文(国際会議プロシーディングス)   出版者・発行元:Springer Verlag  

    A property of term rewriting system (TRS, for short) is said to be composable if it is preserved under unions. We present composable properties of TRSs on the base of modularity results for direct sums of TRSs. We propose a decomposition by a naive sort attachment, and show that modular properties for direct sums of TRSs are τ-composable for a naive sort attachment τ. Here, a decomposition of a TRS R is a pair (R 1,R 2) of (not necessary disjoint) subsets of R such that R = R 1 U R 2
    and for a naive sort attachment T a property ø of TRSs is said to be τ-composable if for any TRS R such that τ is consistent withR, ø(R1) Λ φ(R2) implies φ(R) where (R 1, R 2) is the decomposition of R by τ.

    DOI: 10.1007/BFb0027006

    Scopus

    researchmap

  • Persistency of Confluence. 査読

    Takahito Aoto, Yoshihito Toyama

    J. UCS3 ( 11 ) 1134 - 1147   1997年

     詳細を見る

    記述言語:英語   掲載種別:研究論文(学術雑誌)  

    DOI: 10.3217/jucs-003-11-1134

    researchmap

  • Non-uniqueness of normal proofs for minimal formulas in implication-conjunction fragment of BCK

    Takahito Aoto, Hiroakira Ono

    Bulletin of the Section of Logic23 ( 3 ) 104 - 112   1994年

     詳細を見る

▶ 全件表示

MISC

  • Proving confluence of term rewriting systems via persistency and decreasing diagrams

    Takahito Aoto, Sorin Stratulat

    Proceedings of 16th International Symposium on Principles and Practice of Declarative Programming (PPDP 2014),   2014年

     詳細を見る

  • 項書き換えシステムの変換を利用した帰納的定理自動証明

    佐藤洸一, 菊池健太郎, 青戸等人, 外山芳人

    コンピュータソフトウェア   2014年

  • 項書き換えシステムの変換を利用した帰納的定理自動証明

    佐藤洸一, 菊池健太郎, 青戸等人, 外山芳人

    コンピュータソフトウェア   2014年

  • Proving confluence of term rewriting systems via persistency and decreasing diagrams

    Takahito Aoto, Sorin Stratulat

    Proceedings of 16th International Symposium on Principles and Practice of Declarative Programming (PPDP 2014),   2014年

     詳細を見る

  • Proving confluence of term rewriting systems via persistency and decreasing diagrams

    Takahito Aoto, Yoshihito Toyama, Kazumasa Uchida

    Proceedings of Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA 2014)   2014年

     詳細を見る

  • Proving confluence of term rewriting systems via persistency and decreasing diagrams

    Takahito Aoto, Yoshihito Toyama, Kazumasa Uchida

    Proceedings of Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA 2014)   2014年

     詳細を見る

  • Transformations by templates for simply-typed term rewriting

    Takahito Aoto, Yuki Chiba

    Proceedings of the 6th International Workshop on Higher-Order Rewriting (HOR 2012)   2012年

     詳細を見る

  • Rational term rewriting revisited: decidability and confluence

    Takahito Aoto, eoren Ketema

    Proceedings of the 6th International Conference on Graph Transformation (ICGT 2012)   2012年

     詳細を見る

  • Rational term rewriting revisited: decidability and confluence

    Takahito Aoto, eoren Ketema

    Proceedings of the 6th International Conference on Graph Transformation (ICGT 2012)   2012年

     詳細を見る

  • 無限項書き換えシステムにおける強頭部正規化可能性および一般生成性の自動反証

    岩見宗弘, 青戸等人

    コンピュータソフトウェア   2012年

  • 無限項書き換えシステムにおける強頭部正規化可能性および一般生成性の自動反証

    岩見宗弘, 青戸等人

    コンピュータソフトウェア   2012年

  • 多項式サイズ正規形を保証する項書き換えシステムの経路順序

    磯部耕己, 青戸等人, 外山芳人

    コンピュータソフトウェア   2012年

  • A REDUCTION-PRESERVING COMPLETION FOR PROVING CONFLUENCE OF NON-TERMINATING TERM REWRITING SYSTEMS

    Takahito Aoto, Yoshihito Toyama

    LOGICAL METHODS IN COMPUTER SCIENCE8 ( 1 )   2012年

     詳細を見る

    記述言語:英語   出版者・発行元:TECH UNIV BRAUNSCHWEIG  

    We give a method to prove confluence of term rewriting systems that contain non-terminating rewrite rules such as commutativity and associativity. Usually, confluence of term rewriting systems containing such rules is proved by treating them as equational term rewriting systems and considering E-criticalpairs and/or termination modulo E. In contrast, our method is based solely on usual critical pairs and it also(partially) work seven if the system is not terminating modulo E. We first present confluence criteria for term rewriting systems whose rewrite rules can be partitioned into a terminating part and a possibly non-terminating part. We then give a reduction-preserving completion procedure so that the applicability of the criteria is enhanced. In contrast to the well-known Knuth-Bendix completion procedure which preserves the equivalence relation of the system, our completion procedure preserves the reduction relation of the system, by which confluence of the original system is inferred from that of the completed system.

    DOI: 10.2168/LMCS-8(1:31)2012

    Web of Science

    researchmap

  • A REDUCTION-PRESERVING COMPLETION FOR PROVING CONFLUENCE OF NON-TERMINATING TERM REWRITING SYSTEMS

    Takahito Aoto, Yoshihito Toyama

    LOGICAL METHODS IN COMPUTER SCIENCE8 ( 1 )   2012年

     詳細を見る

    記述言語:英語   出版者・発行元:TECH UNIV BRAUNSCHWEIG  

    We give a method to prove confluence of term rewriting systems that contain non-terminating rewrite rules such as commutativity and associativity. Usually, confluence of term rewriting systems containing such rules is proved by treating them as equational term rewriting systems and considering E-criticalpairs and/or termination modulo E. In contrast, our method is based solely on usual critical pairs and it also(partially) work seven if the system is not terminating modulo E. We first present confluence criteria for term rewriting systems whose rewrite rules can be partitioned into a terminating part and a possibly non-terminating part. We then give a reduction-preserving completion procedure so that the applicability of the criteria is enhanced. In contrast to the well-known Knuth-Bendix completion procedure which preserves the equivalence relation of the system, our completion procedure preserves the reduction relation of the system, by which confluence of the original system is inferred from that of the completed system.

    DOI: 10.2168/LMCS-8(1:31)2012

    Web of Science

    researchmap

  • Transformations by templates for simply-typed term rewriting

    Takahito Aoto, Yuki Chiba

    Proceedings of the 6th International Workshop on Higher-Order Rewriting (HOR 2012)   2012年

     詳細を見る

  • 多項式サイズ正規形を保証する項書き換えシステムの経路順序

    磯部耕己, 青戸等人, 外山芳人

    コンピュータソフトウェア   2012年

  • 多項式サイズ正規形を保証する項書き換えシステムの経路順序

    磯部耕己, 青戸等人, 外山芳人

    第13回プログラミングおよびプログラミング言語ワークショップ論文集   99 - 113   2011年

     詳細を見る

  • 多項式サイズ正規形を保証する項書き換えシステムの経路順序

    磯部耕己, 青戸等人, 外山芳人

    第13回プログラミングおよびプログラミング言語ワークショップ論文集   99 - 113   2011年

     詳細を見る

  • 無限項書き換えシステムにおける性質に関する考察

    岩見宗弘, 青戸等人

    「代数と言語のアルゴリズムと計算理論」研究集会報告集, 数理解析研究所講究録   2011年

     詳細を見る

  • 項書き換えシステムの到達可能性自動証明法

    高橋翔大, 青戸等人, 外山芳人

    電気関係学会東北支部連合大会平成23年度 2D19   p.149   2011年

     詳細を見る

  • 等式理論と組み合わせた書き換え帰納法

    椛澤涼, 青戸等人, 外山芳人

    電気関係学会東北支部連合大会平成23年度 2D18   p.148   2011年

     詳細を見る

  • Natural Inductive Theorems for Higher-Order Rewriting

    Takahito Aoto, Toshiyuki Yamada, Yuki Chiba

    22ND INTERNATIONAL CONFERENCE ON REWRITING TECHNIQUES AND APPLICATIONS (RTA'11)10   107 - 121   2011年

     詳細を見る

    記述言語:英語   出版者・発行元:SCHLOSS DAGSTUHL, LEIBNIZ CENTER INFORMATICS  

    The notion of inductive theorems is well-established in first-order term rewriting. In higher-order term rewriting, in contrast, it is not straightforward to extend this notion because of extensionality (Meinke, 1992). When extending the term rewriting based program transformation of Chiba et al. (2005) to higher-order term rewriting, we need extensibility, a property stating that inductive theorems are preserved by adding new functions via macros. In this paper, we propose and study a new notion of inductive theorems for higher-order rewriting, natural inductive theorems. This allows to incorporate properties such as extensionality and extensibility, based on simply typed S-expression rewriting (Yamada, 2001).

    DOI: 10.4230/LIPIcs.RTA.2011.107

    Web of Science

    researchmap

  • 項書き換えシステムの到達可能性自動証明法

    高橋翔大, 青戸等人, 外山芳人

    電気関係学会東北支部連合大会平成23年度 2D19   p.149   2011年

     詳細を見る

  • Natural Inductive Theorems for Higher-Order Rewriting

    Takahito Aoto, Toshiyuki Yamada, Yuki Chiba

    22ND INTERNATIONAL CONFERENCE ON REWRITING TECHNIQUES AND APPLICATIONS (RTA'11)10   107 - 121   2011年

     詳細を見る

    記述言語:英語   出版者・発行元:SCHLOSS DAGSTUHL, LEIBNIZ CENTER INFORMATICS  

    The notion of inductive theorems is well-established in first-order term rewriting. In higher-order term rewriting, in contrast, it is not straightforward to extend this notion because of extensionality (Meinke, 1992). When extending the term rewriting based program transformation of Chiba et al. (2005) to higher-order term rewriting, we need extensibility, a property stating that inductive theorems are preserved by adding new functions via macros. In this paper, we propose and study a new notion of inductive theorems for higher-order rewriting, natural inductive theorems. This allows to incorporate properties such as extensionality and extensibility, based on simply typed S-expression rewriting (Yamada, 2001).

    DOI: 10.4230/LIPIcs.RTA.2011.107

    Web of Science

    researchmap

  • Reduction-preserving completion for proving confluence of non-terminating term rewriting systems

    Takahito Aoto, Yoshihito Toyama

    Proceedings of the 22nd International Conference on Rewriting Techniques and Applications   2011年

  • A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems

    Takahito Aoto, Yoshihito Toyama

    22ND INTERNATIONAL CONFERENCE ON REWRITING TECHNIQUES AND APPLICATIONS (RTA'11)10   91 - 106   2011年

     詳細を見る

    記述言語:英語   出版者・発行元:SCHLOSS DAGSTUHL, LEIBNIZ CENTER INFORMATICS  

    We give a method to prove confluence of term rewriting systems that contain non-terminating rewrite rules such as commutativity and associativity. Usually, confluence of term rewriting systems containing such rules is proved by treating them as equational term rewriting systems and considering E-critical pairs and/or termination modulo E. In contrast, our method is based solely on usual critical pairs and usual termination. We first present confluence criteria for term rewriting systems whose rewrite rules can be partitioned into terminating part and possibly non-terminating part. We then give a reduction-preserving completion procedure so that the applicability of the criteria is enhanced. In contrast to the well-known Knuth-Bendix completion procedure which preserves the equivalence relation of the system, our completion procedure preserves the reduction relation of the system, by which confluence of the original system is inferred from that of the completed system.

    DOI: 10.4230/LIPIcs.RTA.2011.91

    Web of Science

    researchmap

  • 無限項書き換えシステムにおける性質に関する考察

    岩見宗弘, 青戸等人

    「代数と言語のアルゴリズムと計算理論」研究集会報告集, 数理解析研究所講究録   2011年

     詳細を見る

  • 等式理論と組み合わせた書き換え帰納法

    椛澤涼, 青戸等人, 外山芳人

    電気関係学会東北支部連合大会平成23年度 2D18   p.148   2011年

     詳細を見る

  • Program Transformation Templates for Tupling Based on Term Rewriting

    Yuki Chiba, Takahito Aoto, Yoshihito Toyama

    IEICE TRANSACTIONS ON INFORMATION AND SYSTEMSE93D ( 5 ) 963 - 973   2010年5月

     詳細を見る

    記述言語:英語   出版者・発行元:IEICE-INST ELECTRONICS INFORMATION COMMUNICATIONS ENG  

    Chiba et al. (2006) proposed a framework of program transformation of term rewriting systems by developed templates. Contrast to the previous framework of program transformation by templates based on lambda calculus, this framework provides a method to verify the correctness of transformation automatically. Tupling (Bird, 1980) is a well-known technique to eliminate redundant recursive calls for improving efficiency of programs. In Chiba et al's framework, however, one can not use tuple symbols to construct developed templates. Thus their framework is not capable of tupling transformations. In this paper, we propose a more flexible notion of templates so that a wider variety of transformations, including tupling transformations, can be handled.

    DOI: 10.1587/transinf.E93.D.963

    Web of Science

    researchmap

  • Automated confluence proof by decreasing diagrams based on rule-labelling

    Takahito Aoto

    Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA 2010)   7 - 16   2010年

     詳細を見る

  • Automated confluence proof by decreasing diagrams based on rule-labelling

    Takahito Aoto

    Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA 2010)   7 - 16   2010年

     詳細を見る

  • Program transformation templates for tupling based on term rewriting

    Yuki Chiba, Takahito Aoto, Yoshihito Toyama

    IEICE Transactions on Information and SystemsE93-D ( 5 ) 963 - 973   2010年

     詳細を見る

    記述言語:英語   出版者・発行元:Institute of Electronics, Information and Communication, Engineers, IEICE  

    Chiba et al. (2006) proposed a framework of program transformation of term rewriting systems by developed templates. Contrast to the previous framework of program transformation by templates based on lambda calculus, this framework provides a method to verify the correctness of transformation automatically. Tupling (Bird, 1980) is a well-known technique to eliminate redundant recursive calls for improving efficiency of programs. In Chiba et al.'s framework, however, one can not use tuple symbols to construct developed templates. Thus their framework is not capable of tupling transformations. In this paper, we propose a more flexible notion of templates so that a wider variety of transformations, including tupling transformations, can be handled. Copyright © 2010 The Institute of Electronics, Information and Communication Engineers.

    DOI: 10.1587/transinf.E93.D.963

    Scopus

    researchmap

  • 反証機能付き書き換え帰納法のための補題自動生成法

    嶌津聡志, 青戸等人, 外山 芳人

    コンピュータソフトウェア26 ( 2 ) 41 - 55   2009年

     詳細を見る

  • Proving confluence of term rewriting systems automatically

    Takahito Aoto, Junichi Yoshida, Yoshihito Toyama

    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)5595   93 - 102   2009年

     詳細を見る

    記述言語:英語  

    We have developed an automated confluence prover for term rewriting systems (TRSs). This paper presents theoretical and technical ingredients that have been used in our prover. A distinctive feature of our prover is incorporation of several divide-and-conquer criteria such as those for commutative (Toyama, 1988), layer-preserving (Ohlebusch, 1994) and persistent (Aoto &amp
    Toyama, 1997) combinations. For a TRS to which direct confluence criteria do not apply, the prover decomposes it into components and tries to apply direct confluence criteria to each component. Then the prover combines these results to infer the (non-)confluence of the whole system. To the best of our knowledge, an automated confluence prover based on such an approach has been unknown. © 2009 Springer Berlin Heidelberg.

    DOI: 10.1007/978-3-642-02348-4_7

    Scopus

    researchmap

  • 反証機能付き書き換え帰納法のための補題自動生成法

    嶌津聡志, 青戸等人, 外山 芳人

    コンピュータソフトウェア26 ( 2 ) 41 - 55   2009年

     詳細を見る

  • 項書き換えシステムの合流性自動判定

    吉田順一, 青戸等人, 外山 芳人

    コンピュータソフトウェア26 ( 2 ) 76 - 92   2009年

     詳細を見る

  • Argument filterings and usable rules for simply typed dependency pairs

    Takahito Aoto, Toshiyuki Yamada

    Proceedings of the 7th International Symposium on Frontiers of Combining Systems (FroCoS 2009)   117 - 132   2009年

  • Argument filterings and usable rules for simply typed dependency pairs

    Takahito Aoto, Toshiyuki Yamada

    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)5749   117 - 132   2009年

     詳細を見る

    記述言語:英語  

    Simply typed term rewriting (Yamada, 2001) is a framework of higher-order term rewriting without bound variables based on Lisp-like syntax. The dependency pair method for the framework has been obtained by extending the first-order dependency pair method and subterm criterion in (Aoto &amp
    Yamada, 2005). In this paper, we incorporate termination criteria using reduction pairs and related refinements into the simply typed dependency pair framework using recursive path orderings for S-expression rewriting systems (Toyama, 2008). In particular, we incorporate the usable rules criterion with respect to argument filterings, which is a key ingredient to prove the termination in a modular way. The proposed technique has been implemented in a termination prover and an experimental result is reported. © 2009 Springer Berlin Heidelberg.

    DOI: 10.1007/978-3-642-04222-5_7

    Scopus

    researchmap

  • Proving Confluence of Term Rewriting Systems Automatically

    Takahito Aoto, Junichi Yoshida, Yoshihito Toyama

    REWRITING TECHNIQUES AND APPLICATIONS5595   93 - 102   2009年

     詳細を見る

    記述言語:英語   出版者・発行元:SPRINGER-VERLAG BERLIN  

    We have developed an automated confluence prover for term rewriting systems (TRSs). This paper presents theoretical and technical ingredients that have been used in our prover. A distinctive feature of our prover is incorporation of several divide-and-conquer criteria such as those for commutative (Toyama, 1988), laver-preserving (Ohlebusch, 1994) and persistent (Aoto & Toyama, 1997 combinations. For a TRS to which direct confluence criteria do not apply, the prover decomposes it into components and tries to apply direct confluence criteria to each component. Then the prover combines these results to infer the (non)confluence of the whole system. To the best of our knowledge, an automated confluence prover based on Such an approach has been unknown.

    DOI: 10.1007/978-3-642-02348-4_7

    Web of Science

    researchmap

  • 項書き換えシステムの合流性自動判定

    吉田順一, 青戸等人, 外山 芳人

    コンピュータソフトウェア26 ( 2 ) 76 - 92   2009年

     詳細を見る

  • Soundness of rewriting induction based on an abstract principle

    Takahito Aoto

    IPSJ Transactions on Programming49 ( SIG 1 ) 28 - 38   2008年

     詳細を見る

  • Sound lemma generation for proving inductive validity of equations

    Takahito Aoto

    Proceedings of the 28th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2008)   13 - 24   2008年

     詳細を見る

  • Automatic construction of program transformation templates

    Yuki Chiba, Takahito Aoto, Yoshihito Toyama

    IPSJ Transactions on Programming49 ( SIG 1 (PRO 35) ) 14 - 27   2008年

     詳細を見る

  • Soundness of rewriting induction based on an abstract principle

    Takahito Aoto

    IPSJ Transactions on Programming49 ( SIG 1 ) 28 - 38   2008年

     詳細を見る

  • Sound lemma generation for proving inductive validity of equations

    Takahito Aoto

    Proceedings of the 28th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2008)   13 - 24   2008年

     詳細を見る

  • Designing a rewriting induction prover with an increased capability of non-orientable theorems

    Takahito Aoto

    Proceedings of Austrian-Japanese Workshop on Symbolic Computation in Software Science   1 - 15   2008年

     詳細を見る

  • Automatic construction of program transformation templates

    Yuki Chiba, Takahito Aoto, Yoshihito Toyama

    IPSJ Transactions on Programming49 ( SIG 1 (PRO 35) ) 14 - 27   2008年

     詳細を見る

  • Designing a rewriting induction prover with an increased capability of non-orientable theorems

    Takahito Aoto

    Proceedings of Austrian-Japanese Workshop on Symbolic Computation in Software Science   1 - 15   2008年

     詳細を見る

  • 項書き換えシステムの合流性自動判定.

    吉田順一, 青戸等人, 外山芳人

    第6回情報科学技術フォーラム(FIT2007)講演論文集,情報技術レターズ ( Vol.6 ) 31 - 34   2007年

     詳細を見る

  • Argument filterings and usable rules for simply typed dependency pairs (extended abstract)

    Takahito Aoto, Toshiyuki Yamada

    Proceedings of the 4th International Workshop on Higher-Order Rewriting (HOR 2007)   2007年

     詳細を見る

  • 項書き換えシステムの合流性自動判定

    吉田順一, 青戸等人, 外山芳人

    情報技術レターズ6   31 - 34   2007年

     詳細を見る

  • Automating Confluence Check of Term Rewriting Systems

    Junichi Yoshida, Takahito Aoto, Yoshihito Toyama

    情報技術レターズ6   31 - 34   2007年

     詳細を見る

  • Argument filterings and usable rules for simply typed dependency pairs (extended abstract)

    Takahito Aoto, Toshiyuki Yamada

    Proceedings of the 4th International Workshop on Higher-Order Rewriting (HOR 2007)   2007年

     詳細を見る

  • 項書き換えシステムの合流性自動判定.

    吉田順一, 青戸等人, 外山芳人

    第6回情報科学技術フォーラム(FIT2007)講演論文集,情報技術レターズ ( Vol.6 ) 31 - 34   2007年

     詳細を見る

  • RAPT: A Program Transformation System based on Term Rewriting

    Yuki Chiba, Takahito Aoto

    Proceedings of the 17th International Conference on Rewriting Techniques and Applications, LNCS 4098   267 - 276   2006年

     詳細を見る

  • Program Transformation by Templates: A Rewriting Framework

    Yuki Chiba, Takahito Aoto, Yoshihito Toyama

    IPSJ Transactions on Programming47   52 - 65   2006年

     詳細を見る

  • Dealing with non-orientable equations in rewriting induction

    Takahito Aoto

    Proceedings of the 17th International Conference on Rewriting Techniques and Applications   242 - 256   2006年

     詳細を見る

  • RAPT: A Program Transformation System based on Term Rewriting

    Yuki Chiba, Takahito Aoto

    Proceedings of the 17th International Conference on Rewriting Techniques and Applications, LNCS 4098   267 - 276   2006年

     詳細を見る

  • Program Transformation by Templates: A Rewriting Framework

    Yuki Chiba, Takahito Aoto, Yoshihito Toyama

    IPSJ Transactions on Programming47   52 - 65   2006年

     詳細を見る

  • Dealing with non-orientable equations in rewriting induction

    Takahito Aoto

    Proceedings of the 17th International Conference on Rewriting Techniques and Applications   242 - 256   2006年

     詳細を見る

  • Program transformation by templates based on term rewriting

    Yuki Chiba, Takahito Aoto, Yoshihito Toyama

    PPDP'05 - Proceedings of the Seventh ACM SIGPLAN Conference on Principles and Practice of Declarative Programming2005   59 - 69   2005年

     詳細を見る

    記述言語:英語  

    Huet and Lang (1978) presented a framework of automated program transformation based on lambda calculus in which programs are transformed according to a given program transformation template. They introduced a second-order matching algorithm of simply-typed lambda calculus to verify whether the input program matches the template. They also showed how to validate the correctness of the program transformation using the denotational semantics. We propose in this paper a framework of program transformation by templates based on term rewriting. In our new framework, programs are given by term rewriting systems. To automate our program transformation, we introduce a term pattern matching problem and present a sound and complete algorithm that solves this problem. We also discuss how to validate the correctness of program transformation in our framework. We introduce a notion of developed templates and a simple method to construct such templates without explicit use of induction. We then show that in any program transformation by developed templates the correctness of the transformation can be verified automatically. In our framework the correctness of the program transformation is discussed based on the operational semantics. This is a sharp contrast to Huet and Lang's framework. Copyright 2005 ACM.

    DOI: 10.1145/1069774.1069780

    Scopus

    researchmap

  • パターンに基づくプログラム変換における列変数の導入

    千葉勇輝, 青戸等人, 外山芳人

    情報技術レターズ   5 - 8   2005年

     詳細を見る

  • Dependency Pairs for Simply Typed Term Rewriting

    Takahito Aoto, Toshiyuki Yamada

    Rewriting Techniques and Applications   120 - 134   2005年

     詳細を見る

  • パターンに基づくプログラム変換における列変数の導入

    千葉勇輝, 青戸等人, 外山芳人

    情報技術レターズ   5 - 8   2005年

     詳細を見る

  • Dependency pairs for simply typed term rewriting

    T Aoto, T Yamada

    TERM REWRITING AND APPLICATIONS, PROCEEDINGS3467   120 - 134   2005年

     詳細を見る

    記述言語:英語   出版者・発行元:SPRINGER-VERLAG BERLIN  

    Simply typed term rewriting proposed by Yamada (RTA, 2001) is a framework of higher-order term rewriting without bound variables. In this paper, the dependency pair method of first-order term rewriting introduced by Arts and Giesl (TCS, 2000) is extended in order to show termination of simply typed term rewriting systems. Basic concepts such as dependency pairs and estimated dependency graph in the simply typed term rewriting framework are clarified. The subterm criterion introduced by Hirokawa and Middeldorp (RTA, 2004) is successfully extended to the case where terms of function type are allowed. Finally, an experimental result for a collection of simply typed term rewriting systems is presented. Our method is compared with the direct application of the first-order dependency pair method to a first-order encoding of simply typed term rewriting systems.

    Web of Science

    researchmap

  • Program transformation by templates based on term rewriting

    Yuki Chiba, Takahito Aoto, Yoshihito Toyama

    PPDP'05 - Proceedings of the Seventh ACM SIGPLAN Conference on Principles and Practice of Declarative Programming2005   59 - 69   2005年

     詳細を見る

    記述言語:英語  

    Huet and Lang (1978) presented a framework of automated program transformation based on lambda calculus in which programs are transformed according to a given program transformation template. They introduced a second-order matching algorithm of simply-typed lambda calculus to verify whether the input program matches the template. They also showed how to validate the correctness of the program transformation using the denotational semantics. We propose in this paper a framework of program transformation by templates based on term rewriting. In our new framework, programs are given by term rewriting systems. To automate our program transformation, we introduce a term pattern matching problem and present a sound and complete algorithm that solves this problem. We also discuss how to validate the correctness of program transformation in our framework. We introduce a notion of developed templates and a simple method to construct such templates without explicit use of induction. We then show that in any program transformation by developed templates the correctness of the transformation can be verified automatically. In our framework the correctness of the program transformation is discussed based on the operational semantics. This is a sharp contrast to Huet and Lang's framework. Copyright 2005 ACM.

    DOI: 10.1145/1069774.1069780

    Scopus

    researchmap

  • Inductive theorems for higher-order rewriting

    Takahito Aoto, Toshiyuki Yamada, Yoshihito Toyama

    Rewriting Techniques and Applications   269 - 284   2004年

     詳細を見る

  • Inductive theorems for higher-order rewriting

    Takahito Aoto, Toshiyuki Yamada, Yoshihito Toyama

    Rewriting Techniques and Applications   269 - 284   2004年

     詳細を見る

  • Proving termination of simply typed term rewriting systems automatically

    Takahito Aoto, Toshiyuki Yamada

    IPSJ Transactions on Programming44 ( SIG 4 (PRO 17) ) 67 - 77   2003年

     詳細を見る

  • 高階関数型プログラムにおける帰納的定理証明

    青戸等人, 山田俊行, 外山芳人

    情報技術レターズ2   21 - 22   2003年

     詳細を見る

  • 高階関数型プログラムにおける帰納的定理証明

    青戸等人, 山田俊行, 外山芳人

    情報技術レターズ2   21 - 22   2003年

     詳細を見る

  • Termination of simply typed term rewriting systems by translation and labelling

    Takahito Aoto, Toshiyuki Yamada

    Rewriting Techniques and Applications   380 - 394   2003年

     詳細を見る

  • 単純型付き項書換え系における停止性の自動証明

    青戸等人, 山田俊行

    情報処理学会論文誌:プログラミング44 ( SIG 4 (PRO 17) ) 67 - 77   2003年

     詳細を見る

  • Termination of simply typed term rewriting systems by translation and labelling

    Takahito Aoto, Toshiyuki Yamada

    Rewriting Techniques and Applications   380 - 394   2003年

     詳細を見る

  • Solution to the problem of Zantema on a persistent property of term rewriting systems

    Takahito Aoto

    The Journal of Functional and Logic Programming2001 ( 12 )   2001年

     詳細を見る

  • Solution to the problem of Zantema on a persistent property of term rewriting systems

    Takahito Aoto

    The Journal of Functional and Logic Programming2001 ( 12 )   2001年

     詳細を見る

  • On the finite model property of intuitionistic modal logics over MIPC

    Takahito Aoto, Hiroyuki Shirasu

    Mathematical Logic Quarterly45 ( 4 ) 435 - 448   1999年

     詳細を見る

    記述言語:英語   出版者・発行元:Wiley-VCH Verlag  

    MIPC is a well-known intuitionistic modal logic of Prior (1957) and Bull (1966). It is shown that every normal intuitionistic modal logic L over MIPC has the finite model property whenever L is Kripke-complete and universal.

    DOI: 10.1002/malq.19990450402

    Scopus

    researchmap

  • Uniqueness of normal proofs in implicational intuitionistic logic

    Takahito Aoto

    Journal of Logic, Language and Information8 ( 2 ) 217 - 242   1999年

     詳細を見る

  • Uniqueness of normal proofs in implicational intuitionistic logic

    Takahito Aoto

    Journal of Logic, Language and Information8 ( 2 ) 217 - 242   1999年

     詳細を見る

  • On the finite model property of intuitionistic modal logics over MIPC

    T Aoto, H Shirasu

    MATHEMATICAL LOGIC QUARTERLY45 ( 4 ) 435 - 448   1999年

     詳細を見る

    記述言語:英語   出版者・発行元:WILEY-V C H VERLAG GMBH  

    MIPC is a well-known intuitionistic modal logic of Prior (1957) and Bull (1966). It is shown that every normal intuitionistic modal logic L over MIPC has the finite model property whenever L is Kripke-complete and universal.

    Web of Science

    researchmap

  • Solution to the problem of Zantema on a persistent property of term rewriting systems

    Takahito Aoto

    Proceedings of the Joint International Symposium PLILP/ALP'98   250 - 265   1998年

     詳細を見る

  • Termination transformation by tree lifiting ordering

    Takahito Aoto, Yoshihito Toyama

    Proceedings of the 9th International Conference on Rewriting Techniques and Applications (RTA-98)   256 - 270   1998年

     詳細を見る

  • Termination transformation by tree lifting ordering

    T Aoto, Y Toyama

    REWRITING TECHNIQUES AND APPLICATIONS1379   256 - 270   1998年

     詳細を見る

    記述言語:英語   出版者・発行元:SPRINGER-VERLAG BERLIN  

    An extension of a modular termination result for term rewriting systems (TRSs, for short) by A. Middeldorp (1989) is presented. We intended to obtain this by adapting the dummy elimination transformation by M. C. F. Ferreira and H. Zantema (1995) under the presence of a non-collapsing non-duplicating terminating TRS whose function symbols are all to be eliminated. We propose a tree Lifting ordering induced from a reduction order and a set G of function symbols, and use this ordering to transform a TRS R into R'; termination of R' implies that of RUS for any non-collapsing non-duplicating terminating TRS S whose function symbols are contained in G, provided that for any l --> r in R (1) the root symbol of r is in G whenever that of l is in G; and (2) no variable appears directly below a symbol from G in l when G contains a constant. Because of conditions (1) and (2), our technique covers only a part of the dummy elimination technique; however, even when S is empty, there are cases that our technique has an advantage over the dummy elimination technique.

    DOI: 10.1007/BFb0052375

    Web of Science

    researchmap

  • Solution to the problem of Zantema on a persistent property of term rewriting systems

    Takahito Aoto

    Proceedings of the Joint International Symposium PLILP/ALP'98   250 - 265   1998年

     詳細を見る

  • On composable properties of term rewriting systems

    Takahito Aoto, Yoshihito Toyama

    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)1298   114 - 128   1997年

     詳細を見る

    記述言語:英語   出版者・発行元:Springer Verlag  

    A property of term rewriting system (TRS, for short) is said to be composable if it is preserved under unions. We present composable properties of TRSs on the base of modularity results for direct sums of TRSs. We propose a decomposition by a naive sort attachment, and show that modular properties for direct sums of TRSs are τ-composable for a naive sort attachment τ. Here, a decomposition of a TRS R is a pair (R 1,R 2) of (not necessary disjoint) subsets of R such that R = R 1 U R 2
    and for a naive sort attachment T a property ø of TRSs is said to be τ-composable if for any TRS R such that τ is consistent withR, ø(R1) Λ φ(R2) implies φ(R) where (R 1, R 2) is the decomposition of R by τ.

    DOI: 10.1007/BFb0027006

    Scopus

    researchmap

  • On composable properties of term rewriting systems

    Takahito Aoto, Yoshihito Toyama

    Proceedings of the 6th International Conference on Algebraic and Logic Programming (ALP'97)   114 - 128   1997年

     詳細を見る

  • Persistency of confluence

    Takahito Aoto, Yoshihito Toyama

    Journal of Universal Computer Science3 ( 11 ) 1134 - 1147   1997年

     詳細を見る

  • Persistency of confluence

    Takahito Aoto, Yoshihito Toyama

    Journal of Universal Computer Science3 ( 11 ) 1134 - 1147   1997年

     詳細を見る

  • Non-uniqueness of normal proofs for minimal formulas in implication-conjunction fragment of BCK

    Takahito Aoto, Hiroakira Ono

    Bulletin of the Section of Logic23 ( 3 ) 104 - 112   1994年

     詳細を見る

  • Non-uniqueness of normal proofs for minimal formulas in implication-conjunction fragment of BCK

    Takahito Aoto, Hiroakira Ono

    Bulletin of the Section of Logic23 ( 3 ) 104 - 112   1994年

     詳細を見る

▶ 全件表示

受賞

  • ソフトウェア科学会 研究論文賞

    2017年   ソフトウェア科学会   項書き換えシステムの変換を利用した帰納的定理自動証明

    佐藤洸一, 菊池健太郎, 青戸等人, 外山芳人

     詳細を見る

    受賞区分:国内学会・会議・シンポジウム等の賞  受賞国:日本国

    researchmap

  • 第12回プログラミングおよびプログラミング言語ワークショップ論文賞

    2012年3月   第12回プログラミングおよびプログラミング言語ワークショッププログラム委員会  

    鈴木翼, 青戸等人, 外山芳人

     詳細を見る

    受賞区分:国内学会・会議・シンポジウム等の賞  受賞国:日本国

    researchmap

  • 第2回情報科学技術フォーラム論文賞

    2003年9月   情報処理学会  

    青戸等人, 山田俊行, 外山芳人

     詳細を見る

    受賞区分:国内学会・会議・シンポジウム等の賞  受賞国:日本国

    researchmap

共同研究・競争的資金等の研究

  • 自動定理証明

    1998年

      詳細を見る

    資金種別:競争的資金

    researchmap

  • ソフトウェア基礎

    1998年

      詳細を見る

    資金種別:競争的資金

    researchmap

  • Foundations of Software

    1998年

      詳細を見る

    資金種別:競争的資金

    researchmap

  • プログラム理論

    1998年

      詳細を見る

    資金種別:競争的資金

    researchmap