We know that $\mathbf A$ is symmetric and positive-definite. We know that $\mathbf B$ is orthogonal:Question: is $\mathbf B \cdot\mathbf A \cdot\mathbf B^\top$ symmetric and positive-definite? Answer: Yes.Question: Could a computer have told us this?Answer: Probably.Are there any symbolic algebra systems (like Mathematica) that handle and propagate known facts about matrices?Edit: To be clear I'm asking this question about abstractly defined matrices. I.e. I don't have explicit entries for $A$ and $B$, I just know that they are both matrices and have particular attribues like symetric, positive definite, etc.... 
Symbolic software packages for Matrix expressions?
matrices;symbolic computation
Edit: This is now in SymPy$ isympyIn [1]: A = MatrixSymbol('A', n, n)In [2]: B = MatrixSymbol('B', n, n)In [3]: context = Q.symmetric(A) & Q.positive_definite(A) & Q.orthogonal(B)In [4]: ask(Q.symmetric(B*A*B.T) & Q.positive_definite(B*A*B.T), context)Out[4]: TrueOlder answer that shows other workSo 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