Nous présentons une méthode originale de recherche de preuve par récurrence utilisant la surréduction. Elle a la particularité d'être fondée sur la déduction modulo et d'utiliser la surréduction pour sélectionner à la fois les variables de récurrence et les schémas d'instanciation. Elle donne également la possibilité de traduire directement toute dérivation effectuée avec succès en une preuve dans le calcul des séquents modulo. La correction et la complétude réfutationnelle de la méthode sont démontrées en théorie de la preuve. Nous étendons ensuite cette première approche aux théories de réécriture équationnelles constituées d'un système de réécriture R et d'un ensemble E d'égalités. A partir du moment où le système de réécriture équationnel (R,E) possède de bonnes propriétés de terminaison et de complétude suffisante, et si on suppose également que E préserve les constructeurs, la surréduction au niveau des positions les plus profondes où apparaît un symbole défini s'effectue uniquement à l'aide d'unificateurs qui sont également des substitutions constructeurs. Ceci est particulièrement intéressant dans le cas des théories associatives, ou associatives commutatives, pour lesquelles notre système de recherche de preuve a été raffiné. / We are presenting an original narrowing-based proof search method for inductive theorems. It has the specificity to be grounded on deduction modulo and to rely on narrowing to provide both induction variables and instantiation schemes. It also yields a direct translation from a successful proof search derivation to a proof in the sequent calculus. The method is shown to be correct and refutationally complete in a proof theoretical way. We are extending this first approach to equational rewrite theories given by a rewrite system R and a set E of equalities. Whenever the equational rewrite system (R,E) has good properties of termination, sufficient completeness, and whenever E is constructor preserving, narrowing at defined-innermost positions is performed with unifiers which are constructor substitutions. This is especially interesting for associative and associative-commutative theories for which the general proof search system is refined.

Il s’est agi, à travers l’analyse des concepts de genèse et de construction, de cerner le sens et l’intention de la démarche philosophique de Fichte. Construire, c’est montrer génétiquement, c’est-à-dire indiquer dans l’esprit les actes nécessaires de la raison par lesquels s’engendre un terme. Il y a deux termes, fondamentalement, à construire. Si la construction suit un mouvement « descendant », le terme à construire est déduit, c’est la conscience empirique ; si la construction suit un mouvement « ascendant », le terme à construire, qui est non déductible, non génétisable, c’est l’absolu. Nous avons voulu montrer que le point de départ de la déduction (de la construction descendante) – le moi absolu –, n’est pas identique au point d’arrivée de la construction ascendante – l’absolu. Car c’est cette distinction entre moi absolu et absolu, affirmée dans la XIIIème conférence de la WL 1804/II comme étant à l’oeuvre depuis la Grundlage de 1794, qui nous est apparue seule capable, une fois remise au centre du système de Fichte, de résoudre deux problèmes majeurs posés par sa philosophie : 1) comment l’auto-position du moi (identique au moi absolu) peut-elle conditionner les actes (aboutissant à poser le monde) sans lesquels il ne pourrait pas non plus avoir lieu, c’est-à-dire comment peut-il, en tant qu’absolument inconditionné, être conditionné à son tour par ce qu’il conditionne ? 2) comment atteindre l’absolu, comment remonter génétiquement jusqu’à lui, si le « point de départ de la WL » ne peut, suivant l’avertissement de 1801, être « dépassé », soit, en d’autres termes : comment construire l’inconstructible ? / This thesis, through the analysis of the concepts of genesis and construction, is about defining the meaning and the intention of Fichte’s philosophical doctrine. Constructing, means showing genetically, that is to say highlighting in the mind the acts needed by reason through which a term comes to existence. There are, fundamentally, two terms to construct. If the construction runs on a “downgoing” movement, the term to be built is the empiric conscience ; if the construction runs on a “upgoing” movement, the term to be built is the absolute. We aimed to demonstrate that the starting point of the deduction (the downgoing construction) – the absolute I – is not identical to the final stage of the “upgoing” construction – the absolute. Since it is this distinction between absolute I and absolute, stated in the XIII th conference of the WL 1804/II as being valid since the Grundlage of 1794, which appeared to us as the only one capable, once recentered at the corse of Fichte’s system, to solve two of the major problems inherent to his philosophy :1) how can the auto-position of the I (identical to the absolute I) condition the acts (putting up the world in the end) without which it couldn’t take place either ; that is to say how can it, as absolutely unconditioned, be conditioned in its turn by what it conditions ?2) how can one reach for the absolute, how is it possible to climb back genetically up to it, if the “WL starting point” can’t be, according to the warning of 1801, “exceeded”, or, in other words : how to construct the inconstructible ?

No description available.

Les protocoles de sécurité sont des programmes informatiques qui définissent des règles d'échange entre les points d'un réseau et permettent de sécuriser les communications. Ils sont utilisés par exemple dans les distributeurs de billets, les abonnements aux chaînes de télévision payantes, la téléphonie mobile, le commerce électronique. Leur objectif est de garantir le secret d'une donnée, d'authentifier un des participants, de garantir l'anonymat ou la non-répudiation, etc. Ces programmes sont exécutés sur des réseaux ouverts facilement accessibles (comme internet). Aussi, pour démontrer qu'ils remplissent bien leurs objectifs, il est nécessaire de prendre en compte les attaques dont ils peuvent faire l'objet. L'objet de mon mémoire d'habilitation à diriger des recherches est de montrer que les méthodes formelles peuvent être utilisées avec succès pour entreprendre une analyse fine des protocoles cryptographiques, à travers une palette variée d'outils. Nous présentons des procédures pour déterminer de façon automatique si un protocole est sûr. Nous avons proposés différents algorithmes en fonction des propriétés de sécurité considérées ainsi que des primitives cryptographiques utilisées (chiffrement, signature, hachage, ou exclusif, etc.). D'autre part, nous caractérisons des conditions qui permettent de combiner les résultats précédents et de concevoir les protocoles de façon modulaire. Ces résultats se basent sur des modèles symboliques, très différents de ceux utilisés en cryptographie où la notion de sécurité est basée sur la théorie de la complexité. Cette notion de sécurité est mieux adaptée pour identifier toutes les attaques possibles dans la réalité mais, en contrepartie, les (lourdes) preuves de sécurité sont effectuées à la main et semblent difficilement automatisables. Nous avons identifié des hypothèses cryptographiques qui permettent de relier les approches cryptographiques et symboliques. Il est alors possible d'obtenir des preuves de sécurité à un niveau cryptographique, directement à partir des preuves établies (automatiquement) dans un cadre symbolique.

Étude de la représentation, la structuration et l'utilisation de connaissances dans le cadre d'un projet de recherche en synthèse déductive de programmes. Les connaissances sont considérées comme des sous ensembles finis d'une théorie du premier ordre. Une attention particulière est prêtée au problème du guidage de l'utilisation des connaissances en synthèse de programmes

La présente recherche porte en bonne partie sur le premier chapitre de l'Analytique des concepts, également désigné par Kant comme étant la déduction métaphysique. Pour l'essentiel, ce chapitre présente deux tables, celle des formes logiques du jugement et celle des concepts purs de l'entendement. Notre objectif est de tenter de voir en quoi les formes logiques du jugement peuvent nous amener à déduire les concepts purs de l'entendement, ce qui est la prétention de Kant. Notre hypothèse est qu'un rapport déductif peut être envisagé entre les deux tables dans la mesure où on tient compte du type de jugement impliqué et des diverses significations qu'on peut donner à «déduction métaphysique». Au premier chapitre, nous analysons les types de logique chez Kant pour comprendre la nature exacte de la logique formelle et son rôle dans la déduction mètaphysique. Nous concluons que celui-ci consiste à clarifier les règles fondamentales de l'entendement et que, ce faisant, l'analyse de ces «lois» peut certainement fournir des indications sur les concepts purs. Notre étude des types de jugement nous amène par ailleurs à conclure que, selon toute vraisemblance, il ne peut s'agir dans la déduction métaphysique que du jugement déterminant. Le deuxième chapitre est d'ailleurs consacré à la structure interne du jugement déterminant et à ses diverses fonctions. La première partie conclut que l'acte de détermination temporelle est au coeur de notre problème et la seconde partie qu'il existe des liens inéquivoques entre le jugement et le concept en général. Si les deux premiers chapitres sont surtout analytiques et explicatifs, le troisième chapitre est plutôt évaluatif. Il propose une évaluation des critiques de Strawson, Heidegger et Longuenesse. Cette dernière étape permet de prendre du recul sur la signification de la déduction métaphysique et de considérer notre question en dehors de son cadre strict. Au terme de notre recherche, nous concluons qu'il semble impossible de parvenir à déduire les concepts purs des simples formes logiques du jugement, sans l'éclairage de la déduction transcendantale et du schématisme. En ce sens, il faut plutôt considérer le premier chapitre de l'Analytique des concepts comme le début d'une explication qui trouve son achèvement au terme de l'Analytique transcendantale. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : Kant, Jugement, Logique, Formes, Catégories, Déduction.

Dans une première partie, nous montrons qu'il est possible d'établir une correspondance naturelle entre les preuves en déduction naturelle de la validité d'une formule et les réfutations par resolution d'un ensemble de clauses obtenues en appliquant a la négation de cette formule une mise sous forme clausale non standard utilisant une technique de renommage. En particulier, nous montrons qu'il est possible de simuler le fonctionnement d'un calcul des sequents proche de celui de Gentzen par la resolution et nous montrons comment traduire des réfutations par resolution en preuve en déduction naturelle. De plus, nous proposons plusieurs ameliorations de cette mise sous forme clausale avec renommage permettant de faciliter la recherche d'une réfutation par resolution. Dans une deuxième partie, nous décrivons en détail des techniques permettant une mise en œuvre efficace de la resolution avec sortes ordonnées ainsi qu'un principe d'indexation des clauses permettant de résoudre efficacement de nombreux problèmes-clés (tels ceux poses par la subsomption, l'utilisation de systèmes de réécriture...). Ces algorithmes ont ete utilises dans l'implémentation d'un démonstrateur par resolution que nous avons réalisé dans le cadre d'atinf

La Méthode B est une méthode formelle de spécification et de développement de logiciels critiques largement utilisée dans l'industrie ferroviaire. Elle permet le développement de programmes dit corrects par construction, grâce à une procédure de raffinements successifs d'une spécification abstraite jusqu'à une implantation déterministe du programme. La correction des étapes de raffinement est garantie par la vérification de la correction de formules mathématiques appelées obligations de preuve et exprimées dans la théorie des ensembles de la Méthode B. Les projets industriels utilisant la Méthode B génèrent généralement des milliers d'obligation de preuve. La faisabilité et la rapidité du développement dépendent donc fortement d'outils automatiques pour prouver ces formules mathématiques. Un outil logiciel, appelé Atelier B, spécialement développé pour aider au développement de projet avec la Méthode B, aide les utilisateurs a se décharger des obligations de preuve, automatiquement ou interactivement. Améliorer la vérification automatique des obligations de preuve est donc une tache importante. La solution que nous proposons est d'utiliser Zenon, un outils de déduction automatique pour la logique du premier ordre et qui implémente la méthode des tableaux. La particularité de Zenon est de générer des certificats de preuve, des preuves écrites dans un certain format et qui permettent leur vérification automatique par un outil tiers. La théorie des ensembles de la Méthode B est une théorie des ensembles en logique du premier ordre qui fait appel à des schémas d'axiomes polymorphes. Pour améliorer la preuve automatique avec celle-ci, nous avons étendu l'algorithme de recherche de preuve de Zenon au polymorphisme et à la déduction modulo théorie. Ce nouvel outil, qui constitue le cœur de notre contribution, est appelé Zenon Modulo. L'extension de Zenon au polymorphisme nous a permis de traiter, efficacement et sans encodage, les problèmes utilisant en même temps plusieurs types, par exemple les booléens et les entiers, et des axiomes génériques, tels ceux de la théorie des ensembles de B. La déduction modulo théorie est une extension de la logique du premier ordre à la réécriture des termes et des propositions. Cette méthode est parfaitement adaptée à la recherche de preuve dans les théories axiomatiques puisqu'elle permet de transformer des axiomes en règles de réécriture. Par ce moyen, nous passons d'une recherche de preuve dans des axiomes à du calcul, réduisant ainsi l'explosion combinatoire de la recherche de preuve en présence d'axiomes et compressant la taille des preuves en ne gardant que les étapes intéressantes. La certification des preuves de Zenon Modulo, une autre originalité de nos travaux, est faite à l'aide de Dedukti, un vérificateur universel de preuve qui permet de certifier les preuves provenant de nombreux outils différents, et basé sur la déduction modulo théorie. Ce travail fait parti d'un projet plus large appelé BWare, qui réunit des organismes de recherche académique et des industriels autour de la démonstration automatique d'obligations de preuve dans l'Atelier B. Les partenaires industriels ont fournit à BWare un ensemble d'obligation de preuve venant de vrais projets industriels utilisant la Méthode B, nous permettant ainsi de tester notre outil Zenon Modulo.Les résultats expérimentaux obtenus sur cet ensemble de référence sont particulièrement convaincant puisque Zenon Modulo prouve plus d'obligation de preuve que les outils de déduction automatique de référence au premier ordre. De plus, tous les certificats de preuve produits par Zenon Modulo ont été validés par Dedukti, nous permettant ainsi d'être très confiant dans la correction de notre travail. / The B Method is a formal method heavily used in the railway industry to specify and develop safety-critical software. It allows the development of correct-by-construction programs, thanks to a refinement process from an abstract specification to a deterministic implementation of the program. The soundness of the refinement steps depends on the validity of logical formulas called proof obligations, expressed in a specific typed set theory. Typical industrial projects using the B Method generate thousands of proof obligations, thereby relying on automated tools to discharge as many as possible proof obligations. A specific tool, called Atelier B, designed to implement the B Method and provided with a theorem prover, helps users verify the validity of proof obligations, automatically or interactively. Improving the automated verification of proof obligations is a crucial task for the speed and ease of development. The solution developed in our work is to use Zenon, a first-orderlogic automated theorem prover based on the tableaux method. The particular feature of Zenon is to generate proof certificates, i.e. proof objects that can be verified by external tools. The B Method is based on first-order logic and a specific typed set theory. To improve automated theorem proving in this theory, we extend the proof-search algorithm of Zenon to polymorphism and deduction modulo theory, leading to a new tool called Zenon Modulo which is the main contribution of our work. The extension to polymorphism allows us to deal with problems combining several sorts, like booleans and integers, and generic axioms, like B set theory axioms, without relying on encodings. Deduction modulo theory is an extension of first-order logic with rewriting both on terms and propositions. It is well suited for proof search in axiomatic theories, as it turns axioms into rewrite rules. This way, we turn proof search among axioms into computations, avoiding unnecessary combinatorial explosion, and reducing the size of proofs by recording only their meaningful steps. To certify Zenon Modulo proofs, we choose to rely on Dedukti, a proof-checker used as a universal backend to verify proofs coming from different theorem provers,and based on deduction modulo theory. This work is part of a larger project called BWare, which gathers academic entities and industrial companies around automated theorem proving for the B Method. These industrial partners provide to BWare a large benchmark of proof obligations coming from real industrial projects using the B Method and allowing us to test our tool Zenon Modulo. The experimental results obtained on this benchmark are particularly conclusive since Zenon Modulo proves more proof obligations than state-of-the-art first-order provers. In addition, all the proof certificates produced by Zenon Modulo on this benchmark are well checked by Dedukti, increasing our confidence in the soundness of our work.

Contexte : malgré les particularités de l’environnement de pratique de la médecine d’urgence, il n’existe pas de recherches spécifiquement menées sur la thématique du raisonnement clinique dans cette spécialité. Nous avons souhaité mieux comprendre comment les médecins urgentologues raisonnent dans le cadre de la prise en charge initiale des patients. Méthode : une posture épistémologique interprétative a été adoptée à travers un devis de recherche qualitatif de type ethnographique. Des entretiens ont été réalisés auprès de médecins urgentologues experts, à l’issue de la prise en charge d’un patient réel. Ces entretiens reposaient notamment sur la visualisation de l’enregistrement vidéo en perspective subjective située, obtenu grâce à l'usage d'une microcaméra fixée sur la tempe ou la branche de lunettes des praticiens. Résultats : les hypothèses diagnostiques sont générées très précocement par les médecins, parfois même avant la rencontre avec le patient, sur la base de la prise en compte d’un nombre très limité d’informations, pour certaines contextuelles. Cinq hypothèses étaient en moyenne générées lors de la rencontre initiale et au moins une était une hypothèse de gravité. Aucune n’était formellement éliminée ou validée sans résultats d’examens complémentaires. Un jugement précoce quant à la gravité de la situation permettait également aux médecins d’orienter leurs intentions initiales vers des buts diagnostiques ou thérapeutiques. Les experts raisonnaient le plus souvent de manière intuitive. Ils prenaient en compte les spécificités de leur environnement professionnel en étant, par exemple, vigilants au temps, au caractère potentiellement évolutif de l’état clinique du malade et au devenir d’aval de celui-ci. Conclusion : l’identification du raisonnement clinique des médecins urgentologues offre des perspectives importantes en matière de pratique de la médecine d’urgence, et de formation des résidents dans cette discipline. La méthode originale de recueil des données pourrait en outre être réexploitée dans le cadre de travaux ultérieurs.

Thèse numérisée par la Direction des bibliothèques de l'Université de Montréal.