Hypothesis Finding Methods based on Proof Completion

假设发现是人工智能中研究的各种类型的推理所共有的活动。在本研究计画中，我们发展了逻辑推论的方法来寻找假设，其基础是我们的原始想法“证明完成”。在用逻辑形式化的推理中，如溯因推理和机器学习，当观察到的事实不能从背景知识中逻辑推导出来时，就需要假设。这意味着没有任何来自背景知识的证明成功地实现了事实。我们的“证明完备化”思想是通过观察这些不成功的证明并完成其中一个证明来生成假设，在本项目中我们将证明完备化作为逻辑推理规则在归结原理和连接方法两个证明系统中实现。首先，我们形式化证明完成归结原则。由于证明是归结原理中的反驳，因此不完全的证明意味着子句的合取推导。我们要做的就是 ...更多信息 使推导成为反驳是将一个从句的推导连词作为基础，否定这个基础集合，并将这个否定转化为从句的连词。我们把得到的子句的合取称为剩余假设。我们表明，任何正确的假设，事实成为推断的背景理论必须得到推广的剩余假设。这意味着证明完备化是剩余假设的推广。我们还证明了假设发现方法是溯因的，并且通过对证明完备化方法施加一定的约束可以得到一些类型的机器学习。其次，我们用连接方法形式化了证明完备化。由于推导和证明在连接方法中被表示为图，因此我们开发了一个规则，该规则从不完全推导中推导出剩余假设。通过对在不完全推导中加入剩余假设所得到的证明图进行分析，可以从相关逻辑的背景理论和剩余假设中证明事实。这个结果是很自然的，因为除了事实和背景理论，我们没有给出关于假设的任何信息。这一结果也为剩余假设的推广提供了一个新的准则。证明标准是证明系统中的事实能够从背景理论和假设中得到证明。少

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