Schémas de formules et de preuves en logique propositionnelle

This thesis lies in the field of automated deduction, i.e. the development of algorithms aiming at proving automatically some mathematical conjectures. In this thesis, the conjectures that we want to prove belong to an extension of propositional logic called ``formula schemas''. Those objects allow to represent infinitely many propositional formulae in a finite way (similarly to the way that regular languages finitely represent infinitely many words). Proving a formula schema amounts to prove (at once) all the formulae that it represents. We show that the problem of proving formula schemas is undecidable in general. The remaining part of the thesis presents algorithms that still try to prove schemas (event though, of course, they do not terminate in general). Those algorithms allow to identify decidable classes of schemas, i.e. classes for which there exists an algorithm that always terminates for any entry by answering if the schema is valid or not. One of those algorithms have been implemented. Proof methods that are presented here mix classical procedures for propositional logic (DPLL or semantic tableaux) and inductive reasoning. Inductive reasoning is achieved by the use of ``cyclic proofs'', i.e. infinite proofs in which cycles are automatically detected. In such a case, we can turn those infinite proofs into finite objects, which we can call ``proofs schemas''.Le domaine de cette thèse est la déduction automatique, c.-à-d. le développement d'algorithmes dont le but est de prouver automatiquement des conjectures mathématiques. Dans cette thèse, les conjectures que nous voulons prouver appartiennent à une extension de la logique propositionnelle, appelée "schémas de formules". Ces objets permettent de représenter de façon finie une infinité de formules propositionnelles (de même que, p.ex., les langages réguliers permettent de représenter de façon finie des ensembles infinis de mots). Démontrer un schéma de formules revient alors à démontrer (en une fois) l'infinité de formules qu'il représente. Nous montrons que le problème de démontrer des schémas de formules est indécidable en général. La suite de la thèse s'articule autour de la définition d'algorithmes essayant tout de même de prouver automatiquement des schémas (mais, bien sûr, qui ne terminent pas en général). Ces algorithmes nous permettent d'identifier des classes décidables de schémas, c.-à-d. des classes pour lesquelles il existe un algorithme qui termine sur n'importe quelle entrée en répondant si le schéma est vrai ou pas. L'un de ces algorithmes a donné lieu à l'implémentation d'un prototype. Les méthodes de preuves présentées mélangent méthodes de preuve classiques en logique propositionnelle (DPLL ou tableaux sémantiques) et raisonnement par récurrence. Le raisonnement par récurrence est effectuée par l'utilisation de "preuves cycliques", c.-à-d. des preuves infinies dans lesquelles nous détectons des cycles. Dans ce cas, nous pouvons ramener les preuves infinies à des objets finis, ce que nous pouvons appeler des "schémas de preuves"