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".

De nombreuses recherches ont mis en évidence la difficulté des élèves quant au passage de la géométrie pratique à la géométrie théorique entre l'enseignement primaire et secondaire. Néanmoins, peu de celles-ci se sont penchées sur les solutions à mettre de l'avant afin d'atténuer cette rupture. C'est ce point qui retient notre attention dans le cadre de cette étude. Plusieurs possibilités sont envisageables pour diminuer la rupture entre les deux géométries. Pour notre part, nous avons choisi de nous concentrer sur des activités de géométrie pouvant mener graduellement les élèves de la géométrie pratique à la géométrie déductive. Notre hypothèse étant que les élèves de troisième cycle de l'école primaire sont en mesure de faire de la déduction et d'être initiés à la géométrie théorique. Cette hypothèse est d'ailleurs soutenue par les travaux de Lester (1975) et Douaire (1999). Afin de bien cerner les éléments qui distinguent la géométrie pratique de la géométrie théorique, nous avons fait appel aux travaux de Parzysz (2002) basés sur ceux de van Riele (1984) et de Houdement et Kuzniak (1999). Les outils qu'ils ont développés nous permettent de distinguer plusieurs paradigmes géométriques ainsi que les éléments clés qui les différencient. En nous basant sur ces précédentes études, nous avons mis sur pied une séquence d'activités mettant en lumière les limites de la démarche instrumentée (utilisation de la règle graduée et rapporteur d'angle) tout en souhaitant mettre à profit le développement du raisonnement déductif. Pour la construction de ces activités, nous avons utilisé une démarche de Design Research (Edelson 2002). De plus, nous avons fait appel aux travaux de Coppé et coll. (2005) quant aux différents types de dessin que l'élève rencontre en classe de géométrie. La séquence de neuf activités bâties a été expérimentée dans deux classes de 6e année sur une durée d'environ 4 mois. Les analyses découlant de ces expérimentations ont mis en évidence dans quelle mesure il est possible de favoriser le développement du raisonnement déductif chez les élèves en utilisant des activités d'initiation à la géométrie déductive. De plus, les analyses nous ont aussi permis d'identifier quelles étaient les tâches pouvant mener l'élève à délaisser la mesure au profit de la déduction, tâches qui étaient construites dans l'objectif que l'élève fasse le passage de la géométrie pratique vers la géométrie déductive. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : didactique des mathématiques, raisonnement déductif, paradigmes géométriques, niveaux de van Hiele.

Cette thèse porte sur la vérification des règles ajoutées de l'Atelier B en utilisant une plate-forme appelée BCARe qui repose sur un plongement de la théorie sous-jacente à la méthode B (théorie de B) dans l'assistant à la preuve Coq. En particulier, nous proposons trois approches pour prouver la validité d'une règle, ce qui revient à prouver une formule exprimée dans la théorie de B. Ces trois approches ont été évaluées sur les règles de la base de règles de SIEMENS IC-MOL. La première approche dite autarcique est développée avec le langage de tactiques de Coq Ltac. Elle repose sur une première étape qui consiste à déplier tous les opérateurs ensemblistes pour obtenir une formule de la logique du premier ordre. Puis nous appliquons une procédure de décision qui met en oeuvre une heuristique naïve en ce qui concerne les instanciations. La deuxième approche, dite sceptique,appelle le prouveur automatique de théorèmes Zenon après avoir effectué l'étape de normalisation précédente. Nous vérifions ensuite les preuves trouvées par Zenon dans le plongement profond de B en Coq. La troisième approche évite l'étape de normalisation précédente grâce à une extension de Zenon utilisant des règles d'inférence spécifiques à la théorie de B. Ces règles sont obtenues grâce à la technique de superdéduction. Cette dernière approche est généralisée en une extension de Zenon à toute théorie grâce à un calcul dynamique des règles de superdéduction. Ce nouvel outil, appelé Super Zenon, peut par exemple prouver des problèmes issus de la bibliothèque de problèmes TPTP.

Quels sont les principes applicables pour la déduction fiscale des charges de l'entreprise en France et en Turquie? Tel est le thème de cette étude comparative qui a été menée afin de mettre en lumière la mise en pratique de ces principes tout en essayant d'apporter une réponse à la question « comment les entreprises françaises et turques appliquent ces principes aux charges effectuées durant l'exercice de leurs activités ?, et en traitant les sujets inhérents à ces charges déductibles. Elle révèle que le contenu de ces principes est le même dans les deux pays, mais qu'il est toutefois possible de rencontrer des divergences dans leur application et, parfois aussi, dans les décisions des juridictions administratives. La bonne application de ces principes relatifs à la déductibilité des charges en fiscalité des entreprises est essentielle pour déterminer la base d'imposition de l'entreprise. Cette dernière doit supporter les conséquences fiscales et pénales, en cas de non-respect de ces principes. Les entreprises sont libres dans leur gestion. L'administration ne peut s'y immiscer que dans les cas où sont constatés des actes anormaux de gestion ou des abus de droit. En comparant les deux systèmes, cette étude met également en exergue l'absence de certaines dispositions qui constitue la cause principale des contradictions relevées entre les jurisprudences. / What are the tax deductibility rules of costs incurred by a company in France and in Turkey? Here is the main theme of the present comparative study carried out in order to highlight the practical application of those rules. The study also aims to answer the question: "How do French and Turkish companies deal with the tax deductibility rules of their costs incurred during in the course of their economic activity?" We also aim to explain other topics related to tax deductibility of business costs. The dissertation shows that the content of tax deductibility rules is quite similar in both countries. However, the practical application of those rules and their interpretation provided by Administrative Courts in their respective case law shows differences. This being said, the correct application of tax deductibility rules related to business cost is essential in order to determine the taxable basis of a company. This later could face tax reassessments and penalties in case it would be non-compliant with the tax deductibility rules. Companies are free to manage their company in the way they want to. Tax Administration may not interfere in the management of a company unless it found out an abnormal management action or an abuse of law. The present comparative study also highlights the fact that both French and Turkish rules show a lack of specific provisions or measures which constitutes the principal cause of contradictions revealed between the two countries case laws.

Dans les Règles pour la direction de l’esprit, Descartes fonde sa première théorie de la science sur deux « actes de l’intellect » : intuitus et deductio. Au moment de définir le concept d’intuition, Descartes précise qu’il en fait un « usage nouveau », qui ne doit pas être confonduavec la signification courante qu’on lui a donnée dans les Écoles. L’exposition de ses premières découvertes scientifiques impliquerait donc une noétique différente de celle que lui ont enseignée ses maîtres jésuites. Reprenant un mot ancien, Descartes lui donne une signification neuve et un rôle inédit dans l’édifice de la connaissance humaine. Mais on n’a pas toujours compris le sens historique et philosophique de cette démarcation : de qui et de quoi Descartes entend-il se démarquer ? Et qu’y avait-il au juste de nouveau dans l’usage qu’il proposait ? Notre enquête propose de retracer l’histoire de cette idée d’intuition intellectuelle au cours de l’âge classique, chez les premiers lecteurs des Regulae, Malebranche, Locke, dans les entrées des dictionnaires et des encyclopédies du XVIIIe siècle,dans les nouveaux manuels de logique inspirés de Locke. Nous retraçons cette histoire jusqu’à ce que Kant, en 1770, semble y mettre le point final, en affirmant qu’il n’y a pas en l’homme de connaissance intuitive intellectuelle. Pourtant, et c’est tout le paradoxe, lorsque Kant formule ce constat d’échec, le mot même d’intuition s’est enfin, et pour la première fois,imposé dans le vocabulaire philosophique européen. / In the Rules for the Direction of the Mind, Descartes grounds his first theory of knowledge upon two "acts of the understanding" : intuitus and deductio. When he explains what he means by intuition, he warns the reader that he intends to make a "new use" of this word, which shall not be confused with the way the "schoolmen" understood it in the past. Descartes' first scientific discoveries seem to imply a new noetic, different from the one his Jesuit masters taught him while he was a student at La Fleche. But what, exactly, was new about the way Descartes used this ancient word ? The present inquiry is an attempt to give this question an answer, and also to trace this concept of intuition through the whole early modern period; in the works of the first readers of the Regulae (Baillet, Port-Royal, Malebranche), in the theory of knowledge of John Locke, in the dictionaries, lexicons and encyclopedias of the 18th century, in the new textbooks of Logic, inspired by Locken in some theological discussions over the nature of beatific vision.Our inquiry ends in 1770 when Kant declares that there's no such thing as "intellectual intuition" in man's mind, and that the only kind of intuition man's capable of is a sensitive one. Kant seems to put an endpoint to this chapter of European philosophy. But, on the other hand, when Kant writes this sentence, the word" intuition" has fully entered the European philosophical vocabulary, for the first time with its new meaning.

Nous nous intéressons à des formules de la logique du premier ordre où certaines constantes sont interprétées dans un domaine défini inductivement, comme les entiers. Le problème de la validité n'est pas semi-décidable pour ces formules. Le but de cette thèse est donc d'accroître les capacités des procédures de preuve les plus efficaces pour la logique du premier ordre (fondées sur le calcul de résolution et de superposition) afin de tenir compte de ces constantes particulières. Pour cela, nous adaptons le calcul de superposition en ajoutant notamment un mécanisme de détection de cycles qui simule une forme d'induction mathématique. Nous étudions dans un premier temps le cas particulier des entiers, puis nous généralisons certains des résultats obtenus au cas où les constantes inductives sont définies à l'aide de constructeurs monadiques (des mots). Nous présentons des classes syntaxiques pour lesquelles nous pouvons assurer la complétude et/ou la décidabilité. Nous décrivons un outil appelé SuperInd, fondé sur le démonstrateur Prover9, implémentant les résultats précédents. Enfin, nous décrivons certaines expérimentations et procédons à des comparaisons avec d'autres approches. / We consider first order formulas where some constant symbols are defined in an inductive domain. The validity problem is not semi-decidable for these formulas. This work aims to increase the capabilities of the usual first order proof procedures (usually based on superposition and resolution calculus) to handle these particular constant symbols. Thus, we adapt the superposition calculus using a loop detection mechanism encoding a form of mathematical induction. We first consider the particular case of natural numbers, then we generalize some of these results to the case where the inductive constant symbols are defined with monadic constructors (words). We present some syntactic classes for which we can ensure completeness and/or decidability. We describe a new tool named SuperInd, based on the theorem prover Prover9, implementing our previous results. Finally we describe some experimentations and some comparisons with other approaches.

La Critique de la raison pure est traversée de part en part par une analogie juridique dont l’étude peut enrichir la compréhension de l’œuvre. Il est ainsi question, dès la préface, d’une raison qui se juge elle-même devant son propre tribunal, ce qui constituera le point de départ de notre analyse. Or, ce tribunal très particulier doit se fonder sur une connaissance de soi approfondie de la raison. Cette entreprise est de fait réalisée au fil des développements de la Critique. Le rôle bien particulier joué à cet égard par les trois déductions présentes dans l’œuvre sera dûment examiné. On verra par ailleurs que la déduction doit elle-même être considérée plutôt comme procédure d’inspiration juridique que comme inférence, tout en conservant pourtant un statut de preuve philosophique. Les nombreuses allusions juridiques effectuées par Kant au fil de l’œuvre seront ainsi mises à profit dans le cadre de cette interprétation. / A legal analogy runs through the Critique of Pure Reason, and studying it can shed light on the work. The metaphor of the “tribunal of reason”, first introduced in the Preface, will thus be the starting-point for our analysis. Due to its very nature, this tribunal must be based upon reason’s in-depth self-knowledge – a task to be accomplished over the course of the Critique. The special part played in this regard by the book’s three deductions will be thoroughly examined. In addition, we will see that a deduction itself has more to do with a legally inspired procedure than with an inference, while it nevertheless remains a legitimate philosophical proof. Kant’s frequent legal allusions throughout the text will therefore constitute the basis for our interpretation.

Il existe de nombreux démonstrateurs automatiques qui effectuent des raisonnements modulo une théorie équationnelle, c'est-à-dire enconsidérant non pas des termes, mais des classes d'équivalence de termes. En général, les travaux accomplis dans ce domaine ont pour but de concevoir des techniques pour faire de la déduction modulo une théorie particulière. Dans [Avenhaus & Plaisted, 2001], Jürgen Avenhaus et David Plaisted ont cherché à déterminer des techniques qui pourraient être employées dans le traitement non plus d'une théorie particulière, mais de toute une classe de théories équationnelles: les théories permutatives. Les auteurs ont introduit les notions de terme stratifié et d'ensemble stratifié, et décrit les procédures qui devraient être implémentées dans un démonstrateur automatique basé sur ces termes stratifiés. Les propriétés de régularité de ces théories font qu'il est possible d'employer des techniques efficaces de théorie algorithmique des groupes pour les traiter. Les auteurs espéraient que l'efficacité de ces techniques contrebalancerait le nombre élevé de clauses qui pourraient être générées dans un démonstrateur automatique basé sur ces termes stratifiés. Cependant, les algorithmes proposés pour faire de la déduction avec des termes stratifiés sont basés sur une énumération explicite des éléments des groupes, et sont donc exponentiels. Dans ce mémoire, nous développons les travaux d'Avenhaus et Plaisted, et modifions leur formalisme pour pouvoir faire l'usage le plus intensif possible des techniques de théorie algorithmique des groupes.

Nous étudions des méthodes de recherche simultanée de refutation et de modèle. Nous proposons une méthode pour la construction de modèles finis réduisant de façon importante l'espace de recherche des approches existantes. Nous nous intéressons ensuite à la recherche de modèles infinis. Nous étendons les méthodes RAMC (Refutation And Model Construction) et RAMCET (Refutation And Model Construction with Equational Tableaux) définie par R. Caferra et N. Zabel en introduisant de nouvelles règles et stratégies. Ces extensions augmentent strictement les capacités de la méthode, à la fois pour la recherche de preuve et de contre-exemple. Nous montrons que les méthodes proposées sont des procédures de décision uniforme pour une large clase de formules logiques. Ensuite, nous proposons et étudions de nouveaux formalismes pour représenter les modèles: les termes avec exposants entiers et les automates d'arbres. Nous prouvons la décidabilité de la théorie du premier ordre sur les termes avec exposants. Nous proposons également une nouvelle approche pour la découverte et l'utilisation de l'analogie en recherche simultanée de preuve et de contre-exemple et nous montrons comment utiliser la méthode RAMC en Programmation Logique (pour étendre les capacités des interpréteurs, détecter, voire corriger des erreurs dans les programmes etc.). Enfin, nous décrivons le système RAMC-ATINF implémentant certaines des idées proposées et nous donnons quelques résultats expérimentaux.

Les logiques modales sont des logiques permettant la représentation et l'inférence de connaissances. La logique hybride est une extension de la logique modale de base contenant des nominaux, permettant de faire référence à un unique individu ou monde du modèle. Dans cette thèse nous présentons plusieurs algorithmes de tableaux pour logiques hybrides expressives. Nous présentons aussi une implémentation de ces calculs, et nous décrivons les tests de correction et de performance que nous avons effectués, ainsi que les outils les permettant. De plus, nous étudions en détail une famille particulière de logiques liée aux logiques hybrides : les logiques avec opérateurs de comptage. Nous étudions la complexité et la décidabilité de certains de ces langages.