An Experiment of Randomized Hints on an Axiom of Infinite-Valued Lukasiewicz Logic
Logic in Computer Science
2022-04-20 v1
Abstract
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.
Keywords
Cite
@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}
}