Supporting automated deduction in first-order modal logics