In this paper, we present an experiment of our randomized hints strategy of automated reasoning for yielding Axiom(5) from Axiom(1)(2)(3)(4) of Infinite-Valued Lukasiewicz Logic. In the experiment, we randomly generated a set of hints with size ranging from 30 to 60 for guiding hyper-resolution based search by the theorem prover OTTER. We have successfully found the most useful hints list (with 30 clauses) among 150 * 6 hints lists. Also, we discuss a curious non-linear increase of generated clauses in deducing Axiom(5) by applying our randomized hints strategy.
翻译：在本文中,我们展示了一种实验,我们随机随机的提示策略,即自动推理策略,从无穷无穷的卢卡西维茨逻辑的Axiom(1)(2)(3)(4)中产生Axiom(5)。在实验中,我们随机生成了一套尺寸在30至60之间、用于指导理论证明者OTER的超分辨率搜索的提示。我们成功地在150 * 6提示列表中找到了最有用的提示列表(30个条款)。此外,我们还通过应用随机推理策略,讨论了在解出Axiom(5)时产生的条款的奇特的非线性增加。
相关内容
微信扫码咨询专知VIP会员