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
|
| Project Status |
Completed (Fiscal Year 2011)
|
| Budget Amount *help |
¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2011: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Fiscal Year 2010: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
|
|---|
| 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.
|
Report
(3 results)
Research Products
(5 results)
-
-
-
-
[Presentation] Optimizing mkbTT (System Description)2010
Author(s)
Sarah Winkler, Haruhiko Sato, Aart Middeldorp, Masahito Kurihara
Organizer
21st International Conference on Rewriting Techniques and Applications
Place of Presentation
エジンバラ大学,エジンバラ,イギリス
Year and Date
2010-07-13
Related Report
-
