Edit: This is now in SymPy
In : A = MatrixSymbol('A', n, n)
In : B = MatrixSymbol('B', n, n)
In : context = Q.symmetric(A) & Q.positive_definite(A) & Q.orthogonal(B)
In : ask(Q.symmetric(B*A*B.T) & Q.positive_definite(B*A*B.T), context)
Older answer that shows other work
So after looking into this for a while this is what I've found.
The current answer to my specific question is "No, there is no current system that can answer this question." There are however a few things that seem to come close.
First, Matt Knepley and Lagerbaer both pointed to work by Diego Fabregat and Paolo Bientinesi. This work shows both the potential importance and the feasibility of this problem. It's a good read. Unfortunately I'm not certain exactly how his system works or what it is capable of (if anyone knows of other public material on this topic do let me know).
Second, there is a tensor algebra library written for Mathematica called xAct which handles symmetries and such symbolically. It does some things very well but is not tailored to the special case of linear algebra.
Third, these rules are written down formally in a couple of libraries for Coq, an automated theorem proving assistant (Google search for coq linear/matrix algebra to find a few). This is a powerful system which unfortunately seems to require human interaction.
After talking with some theorem prover people they suggest looking into logic programming (i.e. Prolog, which Lagerbaer also suggested) for this sort of thing. To my knowledge this hasn't yet been done - I may play with it in the future.
Update: I've implemented this using the Maude system. My code is hosted on github