2011 Fiscal Year Final Research Report
Automation of inductive theorem proving in equational logic with multi-context reasoning
| Project/Area Number |
22700021
|
|---|
| Research Category |
Grant-in-Aid for Young Scientists (B)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Hokkaido University |
|---|
Principal Investigator |
SATO Haruhiko 北海道大学, 大学院・情報科学研究科, 助教 (30543178)
|
|---|
| Project Period (FY) |
2010 – 2011
|
| Keywords | 定理自動証明 / 項書換え系 / 帰納的定理証明 |
|---|
| Research Abstract |
We have studied on the efficient procedure and reasoning strategy for automating inductive theorem proving, which is an important technique for verifying correctness of software systems. First, we proposed a proof method with multi-context reasoning, which can perform inferences commonly appearing in some different reasoning strategies simultaneously. Second, we proposed a principle for generating correct lemmas which are often required in inductive theorem proving.
|
