An important class of algorithms which both make use of many fundamental algorithms already appearing in your list and contain significant ideas not reflected yet in your list are algorithms for computation with semialgebraic sets (i.e., algorithms in real algebraic geometry).  These algorithms have a very different* flavour than their `counterparts' over algebraically closed fields such as Buchberger's algorithm and related techniques used for Groebner basis computation, Wu's method and other techniques in elimination theory, etc.

Quantifier elimination (effective semialgebraic projection) has always been a central concern in algorithmic real algebraic geometry, so there is perhaps some feeling that these algorithms should be placed under your bullet point (9).  But, the wealth of techniques developed in the context of real quantifier elimination are independently interesting and useful outside of the goal of automated proof.

Important algorithms include those which compute:
<ul>
 <li> Cylindrical Algebraic Decompositions (Collins et al),
 <li> Signed subresultants (Collins et al),
 <li> Betti numbers and Euler-Poincar\`e Characteristic (Basu, Basu-Pollack-Roy),
 <li> Connected component sampling (Basu-Pollack-Roy),
 <li> Roadmaps and Connectedness (Canny, Grigor'ev-Vorobjnov, Heintz-Roy-Solerno, Gournay-Risler),
 <li> Positivstellensatz witnesses via Semidefinite programming (Parrilo, Choi, Harrison, Lam, Powers, Woermann et al) [perhaps this is partially covered by your bullet point (4)].
 </ul>


In a certain sense, the properties Collins exploited in defining cylindrical algebraic  decompositions have been generalised to what are now called `o-minimal structures,' which has led to a rich and very active research area at the intersection of model theory and semialgebraic and subanalytic geometry (see L. van den Dries' ``Tame Topology and O-minimal Structures'').

(* Though it should be mentioned that fundamental algorithms in real algebraic geometry often make use of fundamental algorithms in classical algebraic geometry. )