文章基本信息

标题：A Generalized Hyperparamodulation Strategy Based on a Forward Reasoning for the Equality Relation ; RHU- resolution*
本地全文：下载
作者：Lee, Jin-Hyeong ; Im, Yeong-Hwan ; O, Gil-Rok 等
期刊名称：ETRI Journal
印刷版ISSN：1225-6463
电子版ISSN：2233-7326
出版年度：1987
卷号：9
期号：1
页码：84-96
语种：Korean
出版社：Electronics and Telecommunications Research Institute
摘要：The equality relation is very important in mechanical theorem proving procedures. A proposed inference rule called RHU-resolution is intended to extend the hyperparamodulation[23, 9] by introducing a bidirectional proof search that simultaneously employs a forward reasoning and a backward reasoning, and generalize it by incorporating beneflts of extended hyper steps with a preprocessing process, that includes a subsumption check in an equality graph and a high level planning. The forward reasoning in RHU-resolution may replace the role of the function substitution link.[9] That is, RHU-deduction without the function substitution link gets a proof. In order to control explosive generation of positive equalities by the forward reasoning, we haue put some restrictions on input clauses and k-pd links, and also have included a control strategy for a positive-positive linkage, like the set-of-support concept, A linking path between two end terms can be found by simple checking of linked unifiability using the concept of a linked unification. We tried to prevent redundant resolvents from generating by preprocessing using a subsumption check in the subsumption based eauality graph(SPD-Graph)so that the search space for possible RHU-resolution may be reduced.