The categorization in that list is certainly still current.
Perhaps one new category has emerged, namely, dependently-typed programming languages. These are essentially automated theorem provers where the primary goal is not proving theorems, but programming. Due to the <PERSON>-Howard correspondence, these two concepts are strongly intertwined. The ultimate goal of such programming languages is to write programs that have much stronger guarantees than regular typed programming languages. People also use these for theorem proving. Some new systems falling into this category include Agda and Epigram. One of the key characteristics of such languages is that they put a lot of effort into making it easier for programmers to define inductive families of datatypes. 904
A simple example is a vector, which depends upon natural numbers (defined inductively).
Regarding which ones are still very active, I think they all are. Coq, Isabelle, Twelf, and PVS are used a lot in the programming languages community. Maude is used extensively in modelling systems. (Personally, I've used Coq and <PERSON>.)
I'd never heard of a few of them. In the pdf you link to, there are links to the theorem provers. Some links are current, some are broken. <PERSON> now seems to be some sort of bearded wizard.
The theorem provers mentioned in “A Review of Theorem Provers” are:
* ALF: subsumbed by ALFA, Coq, and Agda.
* ALFA: seems to no longer unsupported.
* COQ: actively supported.
* MetaPRL: seems to be no longer supported.
* NuPRL: actively supported.
* HOL: actively supported.
* PVS: actively supported.
* Isabelle: actively supported.
* TWELF: actively supported.
* ACL2: actively supported.
* INKA: seems to be no longer supported.
* GANDALF: seems to be no longer supported.
* TPS: may still be active, but has only a small following.
* OTTER: may no longer be supported.
* SETHEO: replaced by E-SETHEO, which seems to no longer be supported.
* SPASS: seems to be still active.
* EQP: seems to be no longer supported.
* MAUDE: very actively supported.
* OMEGA: seems to be no longer supported.
* Mizar: actively supported.
There are undoubtedly many new automated theorem provers that have not been mentioned in this list.
For completeness, as suggested by <PERSON>, there are site archiving proofs made using various tools. For example:
* The Archive of Formal Proofs for Isabelle
* Formalized Mathematics for Mizar
* The Constructive Coq Repository 904