Resolution and model building in the infinite-valued calculus of Lukasiewicz

We discuss resolution and its complexity in the infinite-valued sentential calculus of Łukasiewicz, with special emphasis on model building algorithms for satisfiable sets of clauses. We prove that resolution and model building are polynomially tractable in the fragments given by Horn clauses and by Krom clauses, i.e., clauses with at most two literals. Generalizing the pre-existing literature on resolution in infinite-valued logic, by a positive literal we mean a negationless formula in one variable, built only from the connectives ⊕, ⊙, ∨, ∧. We prove that the expressive power of our literals encompasses all monotone McNaughton functions of one variable.