权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Research in fundamental properties of rewriting systems and advanced theorem proving systems

重写系统的基本性质和高级定理证明系统的研究

基本信息

批准号：
15500009
负责人：
OYAMAGUCHI Michio
金额：
$ 1.98万
依托单位：
Mie University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (C)
财政年份：
2003
资助国家：
日本
起止时间：
2003 至 2005
项目状态：
已结题

项目摘要

Term rewriting systems (TRS) have received much attention in recent years, for they are an important computation model for reasoning and rewriting (computing) over a set of equations, and used in various applications such as automated theorem proving and software verification. However, many significant problems concerning TRS's which may be nonterminating or nonlinear remain open.In this research project we have first investigated some unsolved important problems for TRS's which may be nonterminating or nonlinear. Using new proof techniques we have succeeded in extending the previous results and obtaining new results on fundamental decision problems for non-right-linear TRSs of which sufficient conditions ensuring the decidability have not been known so far. That is, we have shown that for the class of semi-constructor TRSs, almost all problems remain undecidable even if we assume that these TRSs are monadic or linear, but the joinability, word and unification problems are decidable for confluent semi-constructor TRSs, although the reachability problem remains undecidable. We have also obtained sufficient conditions for ensuring the decidability of reachability. Next, we have pointed out that the proofs of undecidability of reachability and confluence for flat TRSs given by F.Jacqumard are incorrect and succeeded in obtaining repaired and significantly simpler proofs of these undecidability. These are negative answers to the open problems posed by G.Godoy et al.In this research project concerning automate theorem proving, we has established the theoretical foundation which is based on the final algebra approach and applicable to equations with higher-order function symbols. We have implemented an advanced theorem proving system based on this thory and our research results whose usefulness has been proven by applications to cryptographic protocol verification.

近年来，项重写系统（Term rewrite system， TRS）作为一种重要的对一组方程进行推理和重写（计算）的计算模型受到了广泛的关注，并被广泛应用于自动化定理证明和软件验证等领域。然而，关于非终止或非线性TRS的许多重大问题仍然没有解决。在本研究项目中，我们首先研究了非终止或非线性TRS的一些尚未解决的重要问题。利用新的证明技术，我们成功地推广了以前的结果，并获得了关于非右线性trs的基本决策问题的新结果。也就是说，我们证明了对于半构造类trs，即使我们假设这些trs是一元或线性的，几乎所有问题仍然是不可判定的，但是对于合流半构造类trs，可接合性、词和统一问题是可判定的，尽管可达性问题仍然是不可判定的。我们还得到了保证可达性可判定性的充分条件。其次，我们指出了F.Jacqumard给出的平面trs的可达性和合流性的不可判定性证明是不正确的，并成功地获得了这些不可判定性的修正的和明显更简单的证明。这些是G.Godoy等人提出的开放问题的否定答案。在这个关于自动定理证明的研究项目中，我们建立了基于最终代数方法的理论基础，并适用于具有高阶函数符号的方程。基于这一理论和研究成果，我们实现了一个先进的定理证明系统，其有效性已被应用于加密协议验证。

项目成果

期刊论文数量（35）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

The unification problem for confluent right-ground term rewriting systems

DOI：
10.1016/s0890-5401(03)00022-1
发表时间：
2001-05
期刊：
Inf. Comput.
影响因子：
0
作者：
M. Oyamaguchi;Yoshikatsu Ohta
通讯作者：
M. Oyamaguchi;Yoshikatsu Ohta

The Joinability and Related Decision Problems for Semi-Constructor TRSs

半构造器 TRS 的可连接性及相关决策问题

DOI：
发表时间：
2006
期刊：
Transactions of IPS Japan (in print) 47・5
影响因子：
0
作者：
M.Arimura;H.Nagaoka;I.Mitsuhashi
通讯作者：
I.Mitsuhashi

The Joinability and UnificationProblems for Confluent Semi-Constructor TRSs

汇合半构造器 TRS 的可连接性和统一性问题

DOI：
发表时间：
2004
期刊：
Proceedings of the 15th International Conference on Rewriting Techniques and Applications (RTA 2004) LNCS 3091
影响因子：
0
作者：
M.Hayashi;H.Nagaoka;K.Kusakari;Toshiya Mashima;斎藤拓;H.Yamamoto;I.Mitsuhashi
通讯作者：
I.Mitsuhashi

On the open Problems Concerning Church-Rosser of Left-Linear Term Rewriting Systems

关于左线性项重写系统 Church-Rosser 的开放问题