A Set-Theoretic Approach to Automated Deduction in Graded Modal Logics