Automated Theorem Provers (ATP) are software programs which carry out inferences over logico-mathematical systems, often with the goal of finding proofs to some given theorem. ATP systems are enormously powerful computer programs, capable of solving immensely difficult problems. Currently, many automated theorem provers exist like E, vampire, SPASS, ACL2, Coq etc. However, all the available theorem provers have some common problems: (1) Current ATP systems tend not to try to find proofs entirely on their own. They need help from human experts to supply lemmas, guide the proof, etc. (2) There is not a single proof system available which provides fully automated platforms for both First Order Logic (FOL) and other Higher Order Logic (HOL). (3) Finally, current proof systems do not have an easy way to quickly deploy and reason over new logical systems, which a logic researcher may want to test. In response to these problems, I introduce the MATR framework. MATR is a platform-independent, codelet-based (independently operating processes) proof system with an easy-to-use Graphical User Interface (GUI), where multiple codelets can be selected based on the formal system desired. MATR provides a platform for different proof strategies like deduction and backward reasoning, along with different formal systems such as non-classical logics. It enables users to design their own proof system by selecting from the list of codelets without needing to write an ATP from scratch.

Dans cette thèse, on s'intéresse aux automates cellulaires en tant que modèle de calcul permettant de reconnaître des langages. Dans un tel domaine, il est toujours difficile d'établir des résultats négatifs, typiquement de prouver qu'un langage donné n'est pas reconnu en une certaine fonction de temps par une certaine classe d'automates. On se focalisera en particulier sur les classes de faible complexité comme le temps réel, au sujet desquelles de nombreuses questions restent ouvertes.Dans une première partie, on propose plusieurs manières d'affaiblir encore les classes de langages étudiées, permettant ainsi d'obtenir des exemples de résultats négatifs. Dans une seconde partie, on montre un théorème d'accélération par automate cellulaire d'un modèle séquentiel, les automates finis oublieux. Ce modèle est une version a priori affaiblie, mais non triviale, des automates finis à plusieurs têtes de lecture. / This document deals with cellular automata as a model of computation used to recognise languages. In such a domain, it is always difficult to provide negative results, that is, typically, to prove that a given language is not recognised in some function of time by some class of automata. The document focuses in particular on the low-complexity classes such as real time, about which a lot of questions remain open since several decades.In a first part, several techniques to weaken further still these classes of languages are investigated, thereby bringing examples of negative results. A second part is dedicated to the comparison of cellular automata with another model language recognition, namely multi-head finite automata. This leads to speed-up theorem when finite automata are oblivious, which makes them a priori weaker than in the general case but leaves them a nontrivial power.