Anyone interested in automated reasoning based on nonclassical logics should take a look at this paper. It adapts the resolution principle to first-order modal logic in a particularly clean way. While others have developed resolution methods for modal logics (cited in the paper), the approach presented here does not depend on Kripke semantics as the others do. The key idea here is that when formulas are Skolemized, all quantified variables and Skolem function symbols acquire a number indicating their modal levels, that is, the number of modal operators that contain them within their scopes. Unification is then modified to permit a term t to be substituted for a variable x only if the levels of all the symbols in t are less than or equal to the level of x. The paper includes resolution rules based on this form of unification for modal systems D, T, and S4, and outlines the proofs of soundness and completeness in the case of system D.