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

二元决策图完成流程自动化研究及其集成环境构建

• 批准号: 11780184
• 负责人: 近藤 久
• 金额: $ 1.34万
• 依托单位: Ibaraki University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Encouragement of Young Scientists (A)
• 财政年份: 1999
• 资助国家: 日本
• 起止时间: 1999 至 2000
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-11780184/
• 关键词: 二分決定グラフ; プログラム検証; 停止性; 項書換え系; 完備化手続き; 遺伝的プログラミング

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

This year's annual study was conducted to determine the use of integrated environmental protection. A summary of the following is provided. 1. The order of reduction and the semi-order (precedence order) of the set of related symbols are examined. 2.1. The result is complete. 3. Integrated environmental construction is now being implemented. In 2011, the research and deduction rules were implemented in the original way, and now they are implemented in many ways. Small-scale problems are generated automatically in semi-order (priority order), and large-scale problems are generated in semi-order. Future issues: how to deal with large-scale problems The research of derivative and genetic transformation is based on the automatic synthesis of the transformation system. GP is the most important part of the genetic engineering. The present study is concerned with the synthesis of basic operating parameters, the future, the suitability of operating parameters, and the application of large-scale book conversion systems. The achievements of the conference, the national conference of the affiliated society in China, and the international conference were presented.

项目成果

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

M.Kurihara：“多重归约排序的完成”J.of 自动推理。

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)

M.Kurihara：“软件验证领域专家系统布尔函数的 BDD 表示的启发式和实验”Proc.of 12th Australian Joint Conf.on Artificial Intelligence，AI99。

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)

M.Kurihara：“偏序约束的 BDD 编码及其在软件验证中的应用”Proc.of 2000 IEEE International Conf.

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

Hisashi Kondo：“使用 BDD 表示处理多个优先级的术语重写系统的完整推理规则”第 58 届（1999 年上半年）日本信息处理学会全国会议 2. 241-242（1999 年）。

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

Hisashi Kondo：“使用 BDD 表示处理多个优先级的术语重写系统的完整推理规则”第 58 届（1999 年上半年）日本信息处理学会全国会议 2. 241-242（1999 年）。