Research in fundamental properties of rewriting systems and advanced theorem proving systems
| Project/Area Number |
15500009
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Fundamental theory of informatics
|
|---|
| Research Institution | Mie University |
|---|
Principal Investigator |
OYAMAGUCHI Michio Mie University, Faculty of Engineering, Professor, 工学部, 教授 (50111828)
|
|---|
| Project Period (FY) |
2003 – 2005
|
| Project Status |
Completed (Fiscal Year 2005)
|
| Budget Amount *help |
¥3,100,000 (Direct Cost: ¥3,100,000)
Fiscal Year 2005: ¥900,000 (Direct Cost: ¥900,000)
Fiscal Year 2004: ¥1,000,000 (Direct Cost: ¥1,000,000)
Fiscal Year 2003: ¥1,200,000 (Direct Cost: ¥1,200,000)
|
|---|
| Keywords | Term Rewriting Systems / Church-Rosser(confluence) / nonlinear TRS / completion procedure / automated theorem proving / unification / word problem / joinability / 右非線形TRS |
|---|
| 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 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.
|
Report
(4 results)
Research Products
(20 results)
