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

二分決定グラフを利用した完備化手続きの自動化とその統合環境構築に関する研究

Research Project

Project/Area Number 11780184
Research Category

Grant-in-Aid for Encouragement of Young Scientists (A)

Allocation TypeSingle-year Grants
Research Field 計算機科学
Research InstitutionIbaraki University

Principal Investigator

近藤 久  茨城大学, 工学部, 助手 (40261739)

Project Period (FY) 1999 – 2000
Project Status Completed (Fiscal Year 2000)
Budget Amount *help
¥2,100,000 (Direct Cost: ¥2,100,000)
Fiscal Year 2000: ¥700,000 (Direct Cost: ¥700,000)
Fiscal Year 1999: ¥1,400,000 (Direct Cost: ¥1,400,000)
Keywords二分決定グラフ / プログラム検証 / 停止性 / 項書換え系 / 完備化手続き / 遺伝的プログラミング
Research Abstract

今年度は前年度に行なった研究をもとに二分決定グラフを利用した完備化手続きの実現とその統合環境構築に関する研究を行なった。その概要は以下のようにまとめられる。
1.簡約順序として関数記号の集合上の(厳格)半順序(優先順位)に基づく経路順序を用いて、ある条件を満たす優先順位を自動的に(複数)生成する完備化推論規則を考案した。
2.1.で得られた結果をもとに完備化手続きの実現をおこなった。
3.統合環境構築の実現を現在も遂行中である。
平成11年度に考案した推論規則を元に実現した完備化手続きを用いて、現在も多くの実験を行なっている。小規模な問題に対しては、自動的に半順序(優先順位)を生成することが可能であるが、大規模な問題に対しては、効率的な問題が生じる。今後の課題として、大規模問題に如何にして対応するかが残されている。派生した研究として、遺伝的プログラミング(GP)による項書換え系の自動合成というテーマにも取り組んでいる。GPは遺伝的操作によって木構造で表されるプログラムの合成を行なう手法である。現在までの研究で基本的なリスト操作関数を合成することに成功しており、今後、適合度関数、遺伝的操作の工夫などを検討し、大規模な項書換え系の合成に適用する予定である。これらの成果を、国内所属学会全国大会、国際会議等で発表した。

Report

(2 results)
  • 2000 Annual Research Report
  • 1999 Annual Research Report
  • Research Products

    (10 results)

All Other

All Publications (10 results)

  • [Publications] M.Kurihara: "Completion for Multiple Reduction orderings"J.of Automated Reasoning. 23. 25-42 (1999)

    • Related Report
      2000 Annual Research Report
  • [Publications] H.Kondo: "Design and Heuristics for BDD-based Automated Termination Verification System for Rule-based Programs"Proc.of 1999 IEEE International Conf. on Systems, Man and Cybernetics. V. 738-743 (1999)

    • Related Report
      2000 Annual Research Report
  • [Publications] M.Kurihara: "Heuristics and Experiments on BDD Representation of Boolean Functions for Expert Systems in Software Verification Domains"Proc.of 12th Australian Joint Conf.on Artificial Intelligence,AI'99. 353-364 (1999)

    • Related Report
      2000 Annual Research Report
  • [Publications] 近藤久: "BDD表現を用いた複数優先順位を扱う項書換え系完備化推論規則"第58回(平成11年前期)情報処理学会全国大会. 2. 241-242 (1999)

    • Related Report
      2000 Annual Research Report
  • [Publications] M.Kurihara: "BDD Encoding for Partial Order Constraints and Its Application to Software Verification"Proc.of 2000 IEEE International Conf. on Systems,Man and Cybernetics. 2062-2067 (2000)

    • Related Report
      2000 Annual Research Report
  • [Publications] 近藤久: "遺伝的プログラミングを用いた項書換え系の合成"第62回(平成13年前期)情報処理学会全国大会. 2. (2001)

    • Related Report
      2000 Annual Research Report
  • [Publications] M.Kurihara: "Completion for Multiple Reduction orderings"J.of Automated Reasoning. 23. 25-42 (1999)

    • Related Report
      1999 Annual Research Report
  • [Publications] H.Kondo: "Design and Heuristics for BDD-based Automated Termination Verification System for Rule-based Programs"Proc.of 1999 IEEE International Conf.on Systems,Man and Cybernetics. V. 738-743 (1999)

    • Related Report
      1999 Annual Research Report
  • [Publications] M.Kurihara: "Heuristics and Experiments on BDD Representation of Boolean Functions for Expert Systems in Software Verification Domains"Proc.of 12th Australian Joint Conf.on Artificial Intelligence,AI'99. 353-364 (1999)

    • Related Report
      1999 Annual Research Report
  • [Publications] 近藤 久: "BDD表現を用いた複数優先順位を扱う項書換え系完備化推論規則"第58回(平成11年前期)情報処理学会全国大会. 2. 241-242 (1999)

    • Related Report
      1999 Annual Research Report

URL: 

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

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi