Proving formulas through reduction to decidable classes