Dans ce travail de recherche, nous nous intéressons à une étude didactique des objets équation, inéquation et fonction en faisant référence à la théorie sémantique de la vérité introduite par Frege et Russell et développée par Tarski et Quine, en particulier les notions de phrase ouverte ; satisfaction d'une phrase ouverte par un élément ; quantification, qui permettent de mieux expliciter les notions d'égalité et d'inégalité d'une part, le statut des lettres d'autre part.<br />Notre recherche s'inscrit dans la continuité des travaux de recherche de Durand-Guerrier et nous soutenons la thèse selon laquelle la logique des prédicats est pertinente pour l'analyse des questions liées l'articulation des deux points de vue sémantique et syntaxique dans l'enseignement et l'apprentissage des équations, inéquations et fonctions au secondaire.<br />Pour compléter les éclairages apportés par la sémantique logique, nous avons conduit une étude historique circonscrite des relations entre ces concepts mathématiques. Nous avons ainsi croisé cette étude avec notre perspective logique en vue de repérer la dyade sémantique/ syntaxe au moment de la formation de ces concepts.<br />La question principale étudiée dans l'exploration didactique concerne la possibilité de repérer, dans le développement des concepts d'équation, d'inéquation et de fonction, des phénomènes liés à la dialectique sémantique / syntaxe. Pour cela, nous avons conduit une analyse des programmes et des manuels de l'enseignement secondaire tunisien ; soumis un questionnaire à des élèves du secondaire et des étudiants de classes préparatoires ; proposé une situation d'apprentissage à quelques élèves volontaires et réalisé quelques entretiens avec des enseignants. Nos travaux montrent un recul du point de vue sémantique dès que les techniques syntaxiques sont disponibles, et une quasi absence d'articulation entre syntaxe et sémantique.

La confiance formelle en une propriété abstraite provient de l'existence d'une preuve de sa correction, qu'il s'agisse d'un théorème mathématique ou d'une qualité du comportement d'un logiciel ou processeur. Il existe de nombreuses définitions différentes de ce qu'est une preuve, selon par exemple qu'elle est écrite soit par des humains soit par des machines, mais ces définitions sont toutes concernées par le problème d'établir qu'un document représente en fait une preuve correcte. Le cadre des Certificats de Preuve Fondamentaux (Foundational Proof Certificates, FPC) est une approche proposée récemment pour étudier ce problème, fondée sur des progrès de la théorie de la démonstration pour définir la sémantique des formats de preuve. Les preuves ainsi définies peuvent être vérifiées indépendamment par un noyau vérificateur de confiance codé dans un langage de programmation logique. Cette thèse étend des résultats initiaux sur la certification de preuves du premier ordre en explorant plusieurs dimensions logiques essentielles, organisées en combinaisons correspondant à leur usage en pratique: d'abord, la logique classique sans points fixes, dont les preuves sont générées par des démonstrateurs automatiques de théorème; ensuite, la logique intuitionniste avec points fixes et égalité,dont les preuves sont générées par des assistants de preuve. Les certificats de preuve ne se limitent pas comme précédemment à servir de représentation des preuves complètes pour les vérifier indépendamment. Leur rôle s'étend pour englober des transformations de preuve qui peuvent enrichir ou compacter leur représentation. Ces transformations peuvent rendre des certificats plus simples opérationnellement, ce qui motive la construction d'une suite de vérificateurs de preuve de plus en plus fiables et performants. Une autre nouvelle fonction des certificats de preuve est l'écriture d'aperçus de preuve de haut niveau, qui expriment des schémas de preuve tels qu'ils sont employés dans la pratique des mathématiciens, ou dans des techniques automatiques comme le property-based testing. Ces développements s'appliquent à la certification intégrale de résultats générés par deux familles majeures de démonstrateurs automatiques de théorème, utilisant techniques de résolution et satisfaisabilité, ainsi qu'à la création de langages programmables de description de preuve pour un assistant de preuve. / Formal trust in an abstract property, be it a mathematical result or a quality of the behavior of a computer program or a piece of hardware, is founded on the existence of a proof of its correctness. Many different kinds of proofs are written by mathematicians or generated by theorem provers, with the common problem of ascertaining whether those claimed proofs are themselves correct. The recently proposed Foundational Proof Certificate (FPC) framework harnesses advances in proof theory to define the semantics of proof formats, which can be verified by an independent and trusted proof checking kernel written in a logic programming language. This thesis extends initial results in certification of first-order proofs in several directions. It covers various essential logical axes grouped in meaningful combinations as they occur in practice: first,classical logic without fixed points and proofs generated by automated theorem provers; later, intuitionistic logic with fixed points and equality as logical connectives and proofs generated by proof assistants. The role of proof certificates is no longer limited to representing complete proofs to enable independent checking, but is extended to model proof transformations where details can be added to or subtracted from a certificate. These transformations yield operationally simpler certificates, around which increasingly trustworthy and performant proof checkers are constructed. Another new role of proof certificates is writing high-level proof outlines, which can be used to represent standard proof patterns as written by mathematicians, as well as automated techniques like property-based testing. We apply these developments to fully certify results produced by two families of standard automated theorem provers: resolution- and satisfiability-based. Another application is the design of programmable proof description languages for a proof assistant.