无限值 Lukasiewicz 逻辑一条公理的随机提示实验
计算机科学中的逻辑
2022-04-20 v1
摘要
在本文中,我们展示了一项随机提示自动推理策略的实验,用于从无限值 Lukasiewicz 逻辑的公理(1)(2)(3)(4) 导出公理(5)。在实验中,我们随机生成了规模从 30 到 60 的提示集,以引导定理证明器 OTTER 基于超分辨率的搜索。我们已在 150 * 6 个提示列表中成功找到了最有用的提示列表(含 30 个子句)。此外,我们讨论了应用我们的随机提示策略推导公理(5) 时生成子句数一种奇特的非线性增长。
引用
@article{arxiv.2204.08512,
title = {An Experiment of Randomized Hints on an Axiom of Infinite-Valued Lukasiewicz Logic},
author = {Ruo Ando and Yoshiyasu Takefuji},
journal= {arXiv preprint arXiv:2204.08512},
year = {2022}
}