Fundamental properties of rewriting systems and automated theorem proving
| Project/Area Number |
12680344
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Mie University |
|---|
Principal Investigator |
OYAMAGUCHI Michio Mie Univ., Faculty of Engineering, Professor, 工学部, 教授 (50111828)
|
|---|
| Project Period (FY) |
2000 – 2002
|
| Project Status |
Completed (Fiscal Year 2002)
|
| Budget Amount *help |
¥2,700,000 (Direct Cost: ¥2,700,000)
Fiscal Year 2002: ¥700,000 (Direct Cost: ¥700,000)
Fiscal Year 2001: ¥900,000 (Direct Cost: ¥900,000)
Fiscal Year 2000: ¥1,100,000 (Direct Cost: ¥1,100,000)
|
|---|
| Keywords | Term Rewriting Systems / Church-Rosser / nonlinear TRS / completion procedure / unification / automated theorem proving / normal TRS / completion of extended critical pairs / 定理の自働証明 / 深さ保存性 |
|---|
| Research Abstract |
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.
|
Report
(4 results)
Research Products
(21 results)
