An application of automated equational reasoning to many-valued logic

In this paper we present the theorem prover SBR3 for equational logic and itsapplication in the many-valued logic of Lukasiewicz. We give a new equational axiomatization of many-valued logic and we prove by SBR3 that it is equivalent to the classical equational presentation of such logic given by Wajsberg. We feel that our equational axiomatization of Wajsberg algebras is better suited for automated reasoning than the classical one. Indeed, it has allowed us to obtain a fast mechanical proof of the so called "fifth Lukasiewicz conjecture'', which is regarded as a challenge problem for theorem provers.