权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Hypothesis Finding Methods based on Proof Completion

基于证明完成的假设发现方法

基本信息

批准号：
12680364
负责人：
YAMAMOTO Akihiro
金额：
$ 2.24万
依托单位：
Hokkaido University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (C)
财政年份：
2000
资助国家：
日本
起止时间：
2000 至 2002
项目状态：
已结题

项目摘要

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

假设发现是人工智能研究的各种类型推理的常见活动。在这个研究项目中，我们基于我们最初的想法“证明完成”开发了用于假设发现的逻辑推理方法。在用逻辑形式化的推论中，例如溯因和机器学习，当观察到的事实无法从背景知识中逻辑推导出来时，就需要假设。这意味着背景知识中的任何证据都无法成功地实现事实。我们的“证明完成”的想法是，应该通过观察这些不成功的证明并完成其中一个证明来生成假设。在这个项目中，我们将证明完成实现为两个证明系统中的逻辑推理规则：解析原理和连接方法。首先，我们用解析原则将证明完成形式化。由于证明是解决原则中的反驳，因此不完整的证明意味着子句合取的推导。为了使推导成为反驳，我们所要做的就是将一个从句的派生连词建立基础，否定扎根集，并将否定转换为从句的连词。我们将获得的子句合取称为残差假设。我们表明，任何可以从背景理论中推断出事实的正确假设都必须通过推广残差假设来获得。这意味着证明完成是残差假设的推广。我们还表明，假设发现方法是溯因，某些类型的机器学习是通过对我们的证明完成方法给予一些约束来获得的。其次，我们用连接方法形式化了证明完成。由于推导和证明在连接方法中被表示为图形，因此我们开发了一种从不完全推导中推导出残差假设的规则。通过分析不完全推导中加入留数假设得到的证明图，可以从背景理论和相关逻辑中的留数假设来证明事实。这个结果是很自然的，因为除了事实和背景理论之外，我们没有提供有关假设的任何信息。结果还提出了选择残差假设的适当概括的新标准。标准是证明系统事实能够从背景理论和假设中得到证明。较少的