Research of Automated Deduction System for Linear Logic
| Project/Area Number |
14580375
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Kobe University |
|---|
Principal Investigator |
TAMURA Naoyuki Kobe University, Information Science and Technology Center, Professor, 学術情報基盤センター, 教授 (60207248)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
BANBARA Mutsunori Kobe University, Information Science and Technology Center, Lecturer, 学術情報基盤センター, 講師 (80290774)
|
|---|
| Project Period (FY) |
2002 – 2004
|
| Project Status |
Completed (Fiscal Year 2004)
|
| Budget Amount *help |
¥4,000,000 (Direct Cost: ¥4,000,000)
Fiscal Year 2004: ¥1,300,000 (Direct Cost: ¥1,300,000)
Fiscal Year 2003: ¥1,300,000 (Direct Cost: ¥1,300,000)
Fiscal Year 2002: ¥1,400,000 (Direct Cost: ¥1,400,000)
|
|---|
| Keywords | Linear Logic / Automated Deduction / Automated Reasoning / Theorem Proving |
|---|
| Research Abstract |
The following software development and research have been done during 2002〜2005 years.
●LLPTTP (LLP Technology Theorem Prover)
LLPTTP is a theorem prover for clausal forms of classical logic (REFERENCE 1). This system translates a given clausal form formula into a program of LLP Linear Logic Programming Language, then compiles/executes the program by using the LLP compiler system.
The evaluation shows LLPTTP has a better performance for TPTP problem set compared with PTTP (Prolog Technology Theorem Prover) and lolliCoP.
●LL2LLP (Linear Logic to LLP)
LL2LLP is a theorem prover for classical propositional linear logic (REFERENCE 2,6). This system translates a given classical linear logic formula into a program of LLP Linear Logic Programming Language, then compiles/executes the program by using the LLP compiler system.
The evaluation shows LL2LLP has a much better performance for most of the benchmark problems compared with other linear logic theorem provers, such as linres, linseq, and linTAP.
●Application to a verification system
Joint research on a verification of a real-time specification system has been done with Prof. Okada of Keio University. We developed a prototype of the verification system based on linear logic, and presented/demonstrated the accomplishment at international workshops (REFERENCE 4,5).
|
Report
(4 results)
Research Products
(22 results)
