• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

Combining Rippling and Rewriting Induction for Inductive Theorm Proving

Research Project

Project/Area Number 20500002
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeSingle-year Grants
Section一般
Research Field Fundamental theory of informatics
Research InstitutionTohoku University

Principal Investigator

AOTO Takahito  東北大学, 電気通信研究所, 准教授 (00293390)

Co-Investigator(Kenkyū-buntansha) TOYAMA Yoshihito  東北大学, 電気通信研究所, 教授 (00251968)
Project Period (FY) 2008 – 2010
Project Status Completed (Fiscal Year 2010)
Budget Amount *help
¥3,640,000 (Direct Cost: ¥2,800,000、Indirect Cost: ¥840,000)
Fiscal Year 2010: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2009: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2008: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Keywords定理自動証明 / 書き換えシステム / リップリング / 書き換え帰納法 / 潜在帰納法 / 健全一般化法 / 発散鑑定法 / 合流性
Research Abstract

Our focus in this project is inductive theorem proving based on term rewriting systems. We are, in particular, interested in rewriting induction methods. We extended rewriting induction to enhance provability of non-orientable conjectures, and we implemented an inductive theorem prover based on our extension. Lemma discovery is an important aspect of inductive theorem proving and we generalized a sound generalization technique and gave sound divergence critic, which are useful when the rewriting induction is equipped with the disproving mechanism. We propose rewriting induction framework to incorporate different lemma generation methods. We also investigate automated confluence proving, as it is a necessary property to extend rewriting induction with the disproving mechanism. We gave new techniques to prove confluence and implemented a confluence prover.

Report

(4 results)
  • 2010 Annual Research Report   Final Research Report ( PDF )
  • 2009 Annual Research Report
  • 2008 Annual Research Report
  • Research Products

    (28 results)

All 2011 2010 2009 2008 Other

All Journal Article (13 results) (of which Peer Reviewed: 6 results) Presentation (13 results) Remarks (2 results)

  • [Journal Article] Program transformation templates for tupling based on term rewriting2010

    • Author(s)
      Yuki Chiba, Takahito Aoto and Yoshihito Toyama
    • Journal Title

      IEICE Transactions on Information and Systems, , Review existence

      Volume: Vol.E93-D, No.5 Pages: 963-973

    • NAID

      10026815249

    • Related Report
      2010 Final Research Report
  • [Journal Article] Automated confluence proof by decreasing diagrams based on rule-labelling2010

    • Author(s)
      Takahito Aoto
    • Journal Title

      Proceedings of the 21st International Conference on Rewriting

      Volume: Vol.6 Pages: 7-16

    • Related Report
      2010 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Program transformation templates for tupling based on term rewriting2010

    • Author(s)
      Yuki Chiba, Takahito Aoto, Yoshihito Toyama
    • Journal Title

      IEICE Transactions on Information and Systems

      Volume: Vol.E93-D Pages: 963-973

    • NAID

      10026815249

    • Related Report
      2010 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Argument filterings and usable rules for simply typed dependency pairs, In Proceedings of the 7th International Symposium on Frontiers of Combining Systems (FroCoS 2009)2009

    • Author(s)
      Takahito Aoto and Toshiyuki Yamada
    • Journal Title

      Trento, Italy, Review existence

      Volume: LNAI5749 Pages: 117-132

    • Related Report
      2010 Final Research Report
  • [Journal Article] Proving confluence of term rewriting systems automatically, In Proceedings of the 20th International Conference on Rewriting Techniques and Applications (RTA 2009)2009

    • Author(s)
      Takahito Aoto, Junichi Yoshida and Yoshihito Toyama
    • Journal Title

      Brasilia, Brazil, Review existence

      Volume: LNCS5595 Pages: 93-102

    • Related Report
      2010 Final Research Report
  • [Journal Article] 項書き換えシステムの合流性自動判定2009

    • Author(s)
      吉田順一, 青戸等人, 外山芳人
    • Journal Title

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

      Volume: Vol.26, No.2 Pages: 76-92

    • NAID

      10025982412

    • Related Report
      2010 Final Research Report
    • Peer Reviewed
  • [Journal Article] 反証機能付き書き換え帰納法のための補題自動生成法2009

    • Author(s)
      嶌津聡志, 青戸等人, 外山芳人
    • Journal Title

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

      Volume: Vol.26, No.2 Pages: 41-55

    • NAID

      10025982372

    • Related Report
      2010 Final Research Report
    • Peer Reviewed
  • [Journal Article] 項書き換えシステムの合流性自動判定2009

    • Author(s)
      吉田順一, 青戸等人, 外山芳人
    • Journal Title

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

      Pages: 76-92

    • NAID

      10025982412

    • Related Report
      2009 Annual Research Report
    • Peer Reviewed
  • [Journal Article] 反証機能付き書き換え帰納法のための補題自動生成法2009

    • Author(s)
      嶌津聡志, 青戸等人, 外山芳人
    • Journal Title

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

      Pages: 41-55

    • NAID

      10025982372

    • Related Report
      2009 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Sound lemma generation for proving inductive validity of equations, In Proceedings of the 28th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2008)2008

    • Author(s)
      Takahito Aoto
    • Journal Title

      Bangalore, India, Dagstuhl Seminar Proceedings, Review existence

      Volume: Vol.08004 Pages: 13-24

    • Related Report
      2010 Final Research Report
  • [Journal Article] Modular Church-Rosser Modulo : The Complete Picture, International Journal of Software and Informatics2008

    • Author(s)
      Jean-Pierre Jouannaud and Yoshihito Toyama
    • Journal Title

      Review existence

      Volume: Vol.2, No.1 Pages: 61-75

    • Related Report
      2010 Final Research Report
  • [Journal Article] Termination proof of S-expression rewriting systems with recursive path relations, In Proceedings of the 19th International Conference on Rewriting Techniques and Applications (RTA 2008)2008

    • Author(s)
      Yoshihito Toyama
    • Journal Title

      Hagenberg, Austria, Review existence

      Volume: LNCS5117 Pages: 381-391

    • Related Report
      2010 Final Research Report
  • [Journal Article] Designing a rewriting induction prover with an increased capability of non-orientable theorems, In Proceedings of Austrian-Japanese Workshop on Symbolic Computation in Software Science (SCSS 2008)2008

    • Author(s)
      Takahito Aoto
    • Journal Title

      Hagenberg, Austria, Review existence

      Volume: 200 Pages: 1-15

    • Related Report
      2010 Final Research Report
  • [Presentation] 多項式サイズ正規形を保証する項書き換えシステムの経路順序2011

    • Author(s)
      磯部耕己, 青戸等人, 外山芳人
    • Organizer
      第13回プログラミングおよびプログラミング言語ワークショップ
    • Place of Presentation
      北海道札幌市
    • Related Report
      2010 Final Research Report
  • [Presentation] 基底項書き換え系の多項式時間合流性判定法の改良2011

    • Author(s)
      村井正勝, 青戸等人, 外山芳人
    • Organizer
      第13回プログラミングおよびプログラミング言語ワークショップ
    • Place of Presentation
      北海道札幌市
    • Related Report
      2010 Final Research Report
  • [Presentation] SMTソルバを用いた項書き換えシステムの合流性自動判定2010

    • Author(s)
      的場正樹, 青戸等人, 外山芳人
    • Organizer
      電気関係学会東北支部連合大会
    • Place of Presentation
      青森県八戸市
    • Related Report
      2010 Final Research Report
  • [Presentation] 文脈移動法による項書き換えシステムの変換2010

    • Author(s)
      鈴木翼, 青戸等人, 外山芳人
    • Organizer
      電気関係学会東北支部連合大会
    • Place of Presentation
      青森県八戸市
    • Related Report
      2010 Final Research Report
  • [Presentation] 拡大手法に基づく項書き換え系の合流性自動証明2010

    • Author(s)
      道又淳一, 青戸等人, 外山芳人
    • Organizer
      第12回プログラミングおよびプログラミング言語ワークショップ
    • Place of Presentation
      香川県琴平町
    • Related Report
      2010 Final Research Report
  • [Presentation] 無限項書き換えシステムにおける強頭部正規化可能性の反証手続き2010

    • Author(s)
      岩見宗弘, 青戸等人
    • Organizer
      第12回プログラミングおよびプログラミング言語ワークショップ
    • Place of Presentation
      香川県琴平町
    • Related Report
      2010 Final Research Report
  • [Presentation] 反証機能付き書き換え帰納法のための補題自動生成法2009

    • Author(s)
      青戸等人
    • Organizer
      書き換え技法および応用に関する国際会議
    • Place of Presentation
      ブラジリア(ブラジル)
    • Year and Date
      2009-06-29
    • Related Report
      2009 Annual Research Report
  • [Presentation] 基底項書き換え系の合流性自動判定2009

    • Author(s)
      村井正勝, 青戸等人, 外山芳人
    • Organizer
      第8回情報科学技術フォーラム(FIT2009)
    • Place of Presentation
      宮城県仙台市
    • Related Report
      2010 Final Research Report
  • [Presentation] S式書き換えシステムの停止性を保証するカリー化について2009

    • Author(s)
      磯部耕己, 青戸等人, 外山芳人
    • Organizer
      第8回情報科学技術フォーラム(FIT2009)
    • Place of Presentation
      宮城県仙台市
    • Related Report
      2010 Final Research Report
  • [Presentation] 多重Knuth-Bendix完備化における危険対除去手法の導入2009

    • Author(s)
      道又淳一, 青戸等人, 外山芳人
    • Organizer
      第8回情報科学技術フォーラム(FIT2009)
    • Place of Presentation
      宮城県仙台市
    • Related Report
      2010 Final Research Report
  • [Presentation] S式書換え系の停止性を保証するカリー化について2009

    • Author(s)
      磯部耕己, 青戸等人, 外山芳人
    • Organizer
      第11回プログラミングおよびプログラミング言語ワークショップ
    • Place of Presentation
      岐阜県高山市
    • Related Report
      2010 Final Research Report
  • [Presentation] 多重Knuth-Bendix完備化における効率化手法の導入2009

    • Author(s)
      道又淳一, 青戸等人, 外山芳人
    • Organizer
      第11回プログラミングおよびプログラミング言語ワークショップ
    • Place of Presentation
      岐阜県高山市
    • Related Report
      2010 Final Research Report
  • [Presentation] 基底項書換え系の合流性判定手続きの効率化2009

    • Author(s)
      村井正勝, 青戸等人, 外山芳人
    • Organizer
      第11回プログラミングおよびプログラミング言語ワークショップ
    • Place of Presentation
      岐阜県高山市
    • Related Report
      2010 Final Research Report
  • [Remarks]

    • Related Report
      2010 Final Research Report
  • [Remarks]

    • URL

      http://www.nue.riec.tohoku.ac.jp/index-j.html

    • Related Report
      2010 Annual Research Report

URL: 

Published: 2008-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi