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

Fundamental properties of rewriting systems and automated theorem proving

重写系统和自动定理证明的基本属性

基本信息

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

来源：
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-12680344/
关键词：
Term Rewriting Systems Church-Rosser nonlinear TRS completion procedure unification automated theorem proving normal TRS completion of extended critical pairs 定理の自働証明深さ保存性

项目摘要

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 problems for confluence (CR) of TRS's which may be nonterminating. Using new proof techniques we have succeeded in extending the previous results and generalizing the previous sufficient conditions for ensuring CR of left-linear TRS's. Next, we have shown that there exists a subclass S of TRS's satisfying the following conditions (a)〜(c).(a) There exists a transformation procedure which takes an arbitrary TRS and produces an equivalent TRS in S,(b) S is computationally universal, and(c) a sufficient condition for ensuring CR of any TRS in S which enables us to construct a completion procedure can be obtained.Moreover, we have constructed a new completion procedure using the above sufficient condition for CR of the class S and established the theoretical foundation of automated theorem proving based on this completion procedure. We have implemented a new theorem proving system based on these results and proved its usefulness.In this research project we have also investigated the unification problem of TRS's which is one of the most important ones. We have shown that the unification problem for confluent right-ground TRS's is decidable. By extending this proof technique we have proven that the unification problem is decidable for confluent simple TRS's, but it has been shown to be undecidable for confluent monadic TRS's.

术语重写系统（TRS）近年来受到广泛关注，因为它们是对一组方程进行推理和重写（计算）的重要计算模型，并用于自动定理证明和软件验证等各种应用。然而，许多关于可能是非终止或非线性的TRS的重要问题仍然悬而未决。在这个研究项目中，我们首先研究了一些可能是非终止的TRS汇合（CR）的未解决问题。使用新的证明技术，我们成功地扩展了先前的结果并推广了先前确保左线性 TRS 的 CR 的充分条件。接下来，我们证明存在满足以下条件（a）〜（c）的TRS的子类S。（a）存在一个变换过程，它采用任意TRS并在S中产生等效的TRS，（b）S在计算上是通用的，以及（c）确保S中任何TRS的CR的充分条件，使我们能够构造一个完成过程。此外，我们构造了一个新的完成过程利用上述S类CR的充分条件，建立了基于该完成过程的自动定理证明的理论基础。我们基于这些结果实现了一个新的定理证明系统，并证明了它的有效性。在这个研究项目中，我们还研究了TRS的统一问题，这是最重要的问题之一。我们已经证明，汇合右地面 TRS 的统一问题是可判定的。通过扩展这种证明技术，我们已经证明统一问题对于汇合简单 TRS 是可判定的，但对于汇合单子 TRS 来说是不可判定的。