We have studied auomated deduction procedures for Lukasiewicz infinite valued logic, which has recently attracted a great interest for its application in the logical treatment of partially erroneuous information and foundations of fuzzy systems. This research is carried on together with Prof. D. Mundici of the University of Milan in connection with the European COST action on many-valued logic. More precisely, we have developed a resolution calculus for a fragment of Lukasiewics logic which has a natural characterization in terms of McNaughton functions [24]. We have determined subclasses of clauses which are respectively analogous to the Horn class and the Krom class in the classical case, and for which the decision problem has a polynomial complexity. We have also studied efficient model-building algorithms for satisfiable sets of clauses.