Abstract FR:

Nous nous intéressons à découvrir de nouvelles méthodes, plus efficaces, que celles connues à l'heure actuelle, de recherche de preuves dans les logiques classiques, principalement au premier ordre. Le fondement de notre approche est une étude en termes de classes de complexité de la recherche de preuves a ressources bornées. L'existence d'une preuve in abstracto est indécidable, mais nous nous intéressons aux preuves évidentes a l'aune humaine. Dans ce but, nous approchons la notion d'évidence par diverses mesures de difficulté de théorèmes, et analysons la complexité de la recherche de preuves simples pour ces mesures. Ces résultats nous guident ensuite dans la recherche de nouvelles méthodes de preuves. Nous présentons une méthode pour la logique classique du premier ordre, fondée sur une structure de bdd (binary decision diagram) et l'application d'un principe de contrôle de l'information (au sens de Shannon) dans les algorithmes branchants. Nous généralisons ensuite la méthode à l'intégration de la relation d'égalité (dans le style de Gallier et al. ) Et au traitement de l'ordre supérieur (dans le style de Dougherty et Johann)