Automatic translation between formal languages
I think you are asking this from a stand point of specific tools so let me answer this in two parts.

Theory Part (ideal view):

There is a notion of languages and a notion of computational systems that except these different classes of languages. Finite Automata can accept regular languages, Pushdown Automata can accept context-free languages. If we go all the way up in the Chomsky hierarchy we get recursively enumerable languages which are accepted by turing machines.

As long as the class of languages define by a certain syntax is less than or equal in power to the target syntax's class of languages then this is possible (at least in principal). Parser generators typically compile context-free grammars to turing machines (or turing complete systems rather) which is just jumping rather far in Chomsky hierarchy. Nicely however this allows us to use context-free grammars in settings where we need recursive enumerability like interpreters. I could in principal compile a context-free grammar to a context-free grammar but defined using a different syntax; this is just an issue of the syntax being used to define context-free grammars. What I could not however do is compile a context-free grammar to a regular expression. No semantic rules need apply in this ideal view.

Practical part:

Real parser generators don't just generate code that accepts a given context free language however. They add in bits of your code to produce abstract syntax trees for your programs to use. I think the details of translating something like Antlr 3 (LL grammars) to Bison (LR grammars which are more general) or some other parser generator would be a bit tricky; I wouldn't want to try it. They probably use slightly different template systems for your code for starters. It could be that they execute your code in different orders so unless your code was pure there would really be no hope of translating the code properly.

So I think the answer to "would semantic rules for the grammars also have to formally specified" would be yes. The code that generates the ASTs would need to be functional and pure or something like that. The substitution principal needs to apply I think which is not something that generally applies except in languages like Haskell where even their effectual code has the substitution property.

My bet is that something like this is possible between the right tools but I think it is a very tricky thing.