Project/Area Number |
14380164
|
Research Category |
Grant-in-Aid for Scientific Research (B)
|
Allocation Type | Single-year Grants |
Section | 一般 |
Research Field |
Intelligent informatics
|
Research Institution | National Institute of Informatics (2004) Kobe University (2002-2003) |
Principal Investigator |
INOUE Katsumi NII, Foundations of Informatics Research Division, Professor, 情報学基礎研究系, 教授 (10252321)
|
Co-Investigator(Kenkyū-buntansha) |
IWANUMA Koji Yamanashi Univ., Dept.Computer and Media Eng, Professor, 大学院・医学工学総合研究部, 教授 (30176557)
NABESHIMA Hidetomo Yamanashi Univ., Dept. Computer and Media Eng., Assistant Professor, 大学院・医学工学総合研究部, 助手 (10334848)
田川 聖治 神戸大学, 工学部, 助手 (50252789)
羽根田 博正 神戸大学, 工学部, 教授 (10031113)
|
Project Period (FY) |
2002 – 2004
|
Project Status |
Completed (Fiscal Year 2004)
|
Budget Amount *help |
¥6,300,000 (Direct Cost: ¥6,300,000)
Fiscal Year 2004: ¥1,900,000 (Direct Cost: ¥1,900,000)
Fiscal Year 2003: ¥1,800,000 (Direct Cost: ¥1,800,000)
Fiscal Year 2002: ¥2,600,000 (Direct Cost: ¥2,600,000)
|
Keywords | consequence finding / consequence finding procedure / SOL resolution / knowledge discovery / induction / abduction / automated deduction / tableaux method / 結論発見問題 |
Research Abstract |
In this research, we developed new methods of knowledge discovery under incomplete knowledge. The proposed systems compute abductive and inductive hypotheses based on consequence-finding procedures. Research results can be summarized as the following three items. 1. Efficient computation for consequence finding We adopted SOL resolution by Inoue as a consequence-finding procedure and made it more efficient. In particular, we developed SOL-S(Г) tableaux for efficient speculative computation in multi-agent systems and default reasoning. Moreover, we re-implemented SOL tableaux in Java, and developed a faster consequence-finding procedure SOLAR (SOL for Advanced Reasoning). 2. Basic theories for consequence finding and knowledge discovery We proved that SOL resolution is complete for answer extraction in first-order clausal theories. This is a solution of an open problem for answer completeness in a connection tableaux format. We also considered a hypothesis-finding procedure based on consequence finding (called CF-induction), and found a complete method for generalization in CF-induction. Moreover, we established a unified theory for induction, which combines explanatory induction and descriptive induction. This inductive formalization is based on circumscription, and uses SOL resolution and CF-induction for computing hypotheses. 3. Evaluation and applications of hvpothesis-finding procedures We applied SOL resolution to bioinformatics, and considers the use of extended abduction, which enables us to remove hypotheses as well as addition of them.
|