Resolution and model building in the infinite-valued calculus of Łukasiewicz (Q1276262)

The paper presents a resolution procedure for the infinite-valued calculus of Łukasiewicz. Problems of resolution, model building and their complexity are discussed. The notion of \(\Theta\)-satisfiability is introduced. Then the authors prove that the \(\Theta\)-satisfiability problem is NP-complete. In the particular case of a finite set of Horn-clauses the authors provide decision and model building algorithms that are polynomial. The same is proved for a finite set of Krom-clauses.