The complexity of McNaughton functions of one variable (Q1271879)

In a paper jointly written by the present reviewer with \textit{N. Olivetti}, entitled ``Resolution and model building in the infinite-valued calculus of Łukasiewicz'' [Theor. Comput. Sci. 200, 335-366 (1998)], appropriate generalizations of the classical notions of literal, clause, and resolution are introduced, in view of applications to infinite-valued automated deduction. Literals are defined as nonconstant monotone univariate McNaughton functions, and it is asked whether positive literals coincide with functions represented by formulas in one variable, only using Łukasiewicz conjunction and disjunction. In the paper under review a positive answer is given to this problem, by means of a deep analysis of the subtleties of McNaughton functions. Among others, the author defines a procedure to build univariate McNaughton functions much more quickly than is done by \textit{A. Rose} and \textit{J. B. Rosser} in their paper ``Fragments of many-valued statement calculi'' [Trans. Am. Math. Soc. 87, 1-53 (1958; Zbl 0085.24303)].