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

Proving confluence of higher-order term rewriting systems automatically

Research Project

Project/Area Number 21700017
Research Category

Grant-in-Aid for Young Scientists (B)

Allocation TypeSingle-year Grants
Research Field Fundamental theory of informatics
Research InstitutionShimane University

Principal Investigator

IWAMI Munehiro  島根大学, 総合理工学部, 講師 (70314614)

Project Period (FY) 2009 – 2011
Project Status Completed (Fiscal Year 2011)
Budget Amount *help
¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000)
Fiscal Year 2011: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2010: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2009: ¥2,470,000 (Direct Cost: ¥1,900,000、Indirect Cost: ¥570,000)
Keywords項書換えシステム / 高階項書換えシステム / 無限項書換えシステム / 合流性 / 強頭部正規化可能性 / 強収束性 / 生成性 / 一般生成性
Research Abstract

We studied several rewriting systems for proving confluence of higher-order term rewriting systems automatically. In this project, we showed many term rewriting systems of combinators do not have strong head normalization. Furthermore, we presented procedures for disproving two properties of infinitary term rewriting systems. the strong head normalization and the productivity. The correctness of our procedures is proved. And we implemented our procedures.

Report

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

    (11 results)

All 2012 2011 2010 2009 Other

All Journal Article (7 results) (of which Peer Reviewed: 2 results) Remarks (4 results)

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

    • Author(s)
      岩見宗弘, 青戸等人
    • Journal Title

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

      Volume: Vol.29, No.1 Pages: 211-239

    • NAID

      130004549258

    • URL

      https://www.jstage.jst.go.jp/article/jssst/29/1/29_1_1_211/_pdf

    • Related Report
      2011 Annual Research Report 2011 Final Research Report
    • Peer Reviewed
  • [Journal Article] 無限項書き換えシステムにおける性質に関する考察2011

    • Author(s)
      岩見宗弘, 青戸等人
    • Journal Title

      京都大学数理解析研究所講究録

      Volume: No.1769 Pages: 153-157

    • Related Report
      2011 Final Research Report
  • [Journal Article] 無限項書き換えシステムにおける性質に関する考察2011

    • Author(s)
      岩見宗弘, 青戸等人
    • Journal Title

      数理解析研究所講究録

      Volume: 1769 Pages: 153-157

    • Related Report
      2011 Annual Research Report
  • [Journal Article] 左線形かつK-開発閉包な項書換えシステムの合流性に関する考察2010

    • Author(s)
      岩見宗弘
    • Journal Title

      京都大学数理解析研究所講究録

      Volume: No.1712 Pages: 156-161

    • Related Report
      2011 Final Research Report
  • [Journal Article] 無限項書換えシステムにおける強頭部正規化可能性の反証手続き2010

    • Author(s)
      岩見宗弘, 青戸等人
    • Journal Title

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

      Pages: 261-273

    • Related Report
      2011 Final Research Report 2009 Annual Research Report
    • Peer Reviewed
  • [Journal Article] 左線形かつK-開発閉包な項書換えシステムの合流性に関する考察2010

    • Author(s)
      岩見宗弘
    • Journal Title

      数理解析研究所講究録

      Volume: 1712 Pages: 156-161

    • Related Report
      2010 Annual Research Report
  • [Journal Article] 組合せ子の強収束性2009

    • Author(s)
      岩見宗弘
    • Journal Title

      第8回情報科学技術フォーラム講演論文集

      Pages: 251-258

    • Related Report
      2011 Final Research Report 2009 Annual Research Report
  • [Remarks]

    • URL

      http://www.cis.shimane-u.ac.jp/~munehiro/

    • Related Report
      2011 Final Research Report
  • [Remarks]

    • URL

      http://www.cis.shimane-u.ac.jp/~munehiro/

    • Related Report
      2011 Annual Research Report
  • [Remarks]

    • URL

      http://www.cis.shimane-u.ac.jp/~munehiro/

    • Related Report
      2010 Annual Research Report
  • [Remarks]

    • URL

      http://www.cis.shimane-u.ac.jp/~munehiro/

    • Related Report
      2009 Annual Research Report

URL: 

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

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi