论文标题
在无限值Lukasiewicz逻辑的公理上的随机提示的实验
An Experiment of Randomized Hints on an Axiom of Infinite-Valued Lukasiewicz Logic
论文作者
论文摘要
在本文中，我们提出了一个实验的实验，我们的随机提示策略是自动推理，从公理（1）（2）（2）（3）（4）的Infinite Varued Lukasiewicz逻辑中产生公理（5）。在实验中，我们随机生成了一组提示，大小范围从30到60，用于通过定理prover otter指导基于高分辨率的搜索。在150 * 6个提示列表中，我们成功找到了最有用的提示列表（有30个条款）。另外，我们通过应用我们的随机提示策略来讨论在推导公理（5）中，生成的子句的奇怪非线性增加。
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.
