| Project/Area Number |
12680364
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Intelligent informatics
|
|---|
| Research Institution | Hokkaido University |
|---|
Principal Investigator |
YAMAMOTO Akihiro Hokkaido University, Graduate School of Engineering, Associate Professor, 大学院・工学研究科, 助教授 (30230535)
|
|---|
| Project Period (FY) |
2000 – 2002
|
| Project Status |
Completed (Fiscal Year 2002)
|
| Budget Amount *help |
¥3,500,000 (Direct Cost: ¥3,500,000)
Fiscal Year 2002: ¥900,000 (Direct Cost: ¥900,000)
Fiscal Year 2001: ¥800,000 (Direct Cost: ¥800,000)
Fiscal Year 2000: ¥1,800,000 (Direct Cost: ¥1,800,000)
|
|---|
| Keywords | Proof Completion / Hypothesis Finding / Inductive Ligic / Relevant Ligic / Machine Learning / Abduction / 定理自動証明 / 連結証明 / 残余仮説 / 帰納学習 |
|---|
| Research Abstract |
Hypothesis finding is an activity common to various types of inference investigated in AI. In this research project we developed logical inference methods for hypothesis finding based on our original idea "proof completion". In inferences formalized with logic, such as abduction, and machine learning, hypotheses are needed when observed facts cannot logically derived from background knowledge. This means that no proof from background knowledge successfully achieves the facts. Our idea "proof completion" is that hypotheses should be generated by observing such unsuccessful proofs and by completing one of such proofs.
In this project we realized proof completion as logical inference rules in two proof systems the resolution principle and the connection method. At first we formalized proof completion with the resolution principle. Since a proof is a refutation in the resolution principle, an incomplete proof there means a derivation of conjunction of clauses. All that we have to do in orde
… More
r to make the derivation become a refutation is to ground one of the derived conjunctions of clauses, to negate the grounded set, and transform the negation into a conjunction of clauses. We call the obtained conjunction of clauses a residue hypothesis. We showed that any correct hypothesis with which facts become inferable from background theory must be obtained by generalizing a residue hypothesis. This means that proof completion is generalization of residue hypotheses. We also showed that the hypothesis finding methods is abduction and some types of machine learning are obtained by giving some constraint to our proof completion method.
Secondly we formalized proof completion with the connection method. Since a derivation and a proof is represented as a graph in the connection method, we developed a rule which derives a residue hypothesis from an incomplete derivation. By analyzing the graph for the proof obtained by adding the residue hypothesis to the incomplete derivation, facts can be proved from background theory and the residue hypothesis in relevant logic. This result is quite natural because we give no information about the hypothesis except the facts and the background theory. The result also suggests a new criterion in choosing appropriate generalization of the residue hypothesis. The criterion is in which proof system facts can be proved from background theory and the hypothesis. Less
|
