RESOLUTION AND MODEL-BUILDING IN THE INFINITE-VALUED CALCULUS OF LUKASIEWICZ

We discuss resolution and its complexity in the infinite-valued senten tial calculus of Lukasiewicz, with special emphasis on model building algorithms for satisfiable sets of clauses. We prove that resolution a nd model building are polynomially tractable in the fragments given by Horn clauses and by Krom clauses, i.e., clauses with at most two lite rals. Generalizing the pre-existing literature on resolution in infini te-valued logic, by a positive literal we mean a negationless formula in one variable, built only from the connectives +,.,boolean OR,boolea n AND. We prove that the expressive power of our literals encompasses all monotone McNaughton functions of one variable. (C) 1998-Elsevier S cience B.V. All rights reserved.