Integrating resolution—like procedures with Lukasiewicz implication