Solving polynomial systems is an important part of Computer Algebra since a lot of practical problems (cryptography, robotics, error correcting codes, signal theory and so on ) can be solved using this technique. Among all available methods for solving polynomial systems, computation of Gr?bner bases remains one of the most powerful tools in practice. In 1965, Buchberger has proposed the first algorithm to compute Gr?bner bases. Since 90 percent of the time to compute a Gr?bner basis by Buchberger algorithm is spent for computing the reductions to zero (useless computation), then it is a very challenging question to have a criterion to remove useless critical pairs. In 2002, Faugère could design a new and more efficient algorithm; F5, which computes no reductions to zero in almost all cases. In fact, if the input system of this algorithm is a regular sequence, then F5 computes a Gr?bner basis without any reduction to zero. The criteria used in F5 algorithm are called F5 and IsRewritten criterion. It is worth noting that there is no proof for the correctness of IsRewritten criterion in the related paper. In this thesis, we study the theory behind the F5 algorithm, its correctness and its termination. First, we state a proof for IsRewritten criterion. We show then by a counterexample that the original proof of F5 criterion by Faugère is false and we propose a new and correct proof for it. After this, we discuss about termination of F5 algorithm and we explain that the original proof of F5 termination in the related paper is false and so it remains as an open problem. Furthermore, we apply IsRewritten criterion on improved Buchberger algorithm in a non trivial way, to have a new algorithm simpler than F5 and more efficient and more stable than Buchberger algorithm. At the end, we study some new applications of Gr?bner bases. We propose first a new algorithm for factoring polynomials over algebraic extension fields. After this, we introduce a new and efficient method for computing minimal polynomial of matrices which is more efficient than the corresponding procedure in Maple, and we develop it to compute minimal polynomial of matrices over algebraic extension fields. For the third application, we use the last idea to propose an algorithm to compute minimal polynomial of parametric matrices, using Gr?bner bases of parametric polynomial ideals.