Automated Proofs in Lukasiewicz Logic

In this paper we present some mechanical proofs in the many-valued logic dened by Lukasiewicz. The main result is the rst mechanical proof of the fth Lukasiewicz conjecture. All the presented proofs are obtained by the (AC-)Unfailing Knuth-Bendix completion method in the theorem prover SBR3. However, a proof of the conjecture cannot be obtained by a brute-force application of completion. We introduce auxil-iary functions and reformulate the theorem in terms of the new auxiliary functions. No manual addition of lemmas is needed. These transformations are customary in mathematics and we feel they are useful in automated reasoning too. The paper is organized as follows: in section 1 we present the fth Lukasiewicz con-jecture, in section 2 we brie y present the prover SBR3 and in section 3 we present the proofs. 1 A problem in many-valued logic Many-valued propositional logic was rst introduced by Jan Lukasiewicz in the 1920's. All the following results about early work on many-valued logic are reported in [8]. The original denition of many-valued logic is purely semantical. No axioms and no inference rules are given. Lukasiewicz denes rst a model and then the logic is dened as the set of all sentences in propositional calculus which are true on that model. More precisely, the n-valued logic Ln is dened as the set of all sentences satised by the structure Ln =< f k n 1 j0 k n 1g; g; f> where An = f k n1 j0 k n 1g is the domain, g: An! An is the unary function g(x) = 1 x and f: An An! An is the binary function f(x; y) = min(1 x + y; 1). L1 is the set of all legal propositional sentences, L2 is classical two-valued propositional logic with model L2 =< f0; 1g; g; f&gt