An Experiment of Randomized Hints on an Axiom of Infinite-Valued Lukasiewicz Logic

TL;DR

This paper explores a randomized hints strategy to improve automated reasoning in Infinite-Valued Lukasiewicz Logic, successfully identifying effective hints and revealing non-linear effects on clause generation.

Contribution

It introduces a novel randomized hints approach for guiding theorem proving in Lukasiewicz Logic and demonstrates its effectiveness through experimental results.

Findings

Successfully identified the most useful hints list of 30 clauses

Observed a non-linear increase in generated clauses during proof search

Enhanced automated reasoning efficiency in Lukasiewicz Logic

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.