Les systèmes dynamiques permettent de modéliser des phénomènes évoluant dans le temps selon certaines lois (par exemple physiques), mais n'admettent généralement pas de solution explicite. Ces systèmes peuvent tout de même être (partiellement) résolus lorsqu'ils admettent des intégrales premières, fonctions qui restent constantes pour toute solution du système. Plusieurs classes importantes d'intégrales premières sont construites en combinant suffisamment de polynômes, dits de Darboux. On peut alors montrer la non-existence de telles intégrales premières en énumérant exhaustivement tous ces polynômes, ce qu'on ne sait faire que jusqu'à une borne sur leur degré. Cette thèse présente des algorithmes qui génèrent des preuves qu'un système n'admet pas de polynômes de Darboux. Nous proposons ainsi une nouvelle preuve, entièrement automatisée, que l'oscillateur de Van der Pol ne possède pas de polynôme de Darboux. Notre approche n'est pas limitée par la dimension du système : nous montrons que le système physique de Shimizu-Morioka, de dimension 3, n'admet pas de polynômes de Darboux pour toute valuation de ses paramètres, répondant à une conjecture ouverte. Enfin, nous montrons comment accélérer les procédures existantes de génération de polynômes de Darboux de degré borné. On montre expérimentalement que notre stratégie réduit la dépendance au choix de l'ordre monomial utilisé et permet de générer des polynômes de plus haut degré pour des systèmes de dimension 3.