Résumé
Cette thèse décrit la conception et l'implémentation de Goéland, un prouveur automatique de théorèmes basé sur la méthode des tableaux. Il repose sur une procédure concurrente (prouvée complète) qui permet une gestion élégante des problèmes d’équité dans la recherche de preuve. Sa principale caractéristique est le traitement en parallèle des branches afin de faciliter l’échange d’informations. En complément de cette base solide, le prouveur est équipé pour raisonner à l’intérieur de théories, avec la prise en charge de l’égalité et un module de déduction modulo théorie. Goéland permet également la génération des preuves vérifiables (des extensions ont notamment été créées vers Coq et Lambdapi), et le traitement de problèmes polymorphes. Ces améliorations contribuent à l'efficacité et à la fiabilité de Goéland en tant qu'outil prometteur dans le domaine du raisonnement automatique.