I know that proving context free grammars equivalent is undecidable. I also know that proving if a context free grammar recognizes a regular language is undecidable. Here is my question: is proving that two regular grammars recognize the same language decidable?
Yes, this is decidable. There's a rather direct conversion from a regular grammar to an NFA. From there, run the subset construction to turn the NFAs into DFAs. Run minimization algorithms to convert each DFA to a canonical minimum DFA, then decide whether the two DFAs are equivalent. Each transformation preserves the language represented, so this ultimately decides whether the two grammars have the same language.