In the paper, we consider the problem of supporting automated reasoning in a large class of knowledge representation formalisms, including terminological and epistemic logics, whose distinctive feature is the ability of representing and reasoning about finite quantities. Each member of this class can be represented using graded modalities, and thus the considered problem can be reduced to the problem of executing graded modal logics. We solve this problem using a set-theoretic approach that first transforms graded modal logics into poly modal logics with infinitely many modalities, and then reduces derivability in such polymodal logics to derivability in a suitable first-order set theory.