Binary resolution over complete residuated Stone lattices

This paper extends previous results obtained for binary resolution proof method over complete Boolean lattices. We shall assume that truth values form a complete residuated Stone lattice. In addition, we investigate binary resolution over residuated lattices with strict negation. The refutational soundness and completeness of the generalised resolution proof method will be proved. Finally, we discuss the boundaries of the refutational completeness over arbitrary residuated lattices.