Dissertations / Theses: 'Preuve de théorème'

1

Mzali, Jalel. "Méthodes de filtrage équationnel et de preuve automatique de théorèmes." Nancy 1, 1986. http://www.theses.fr/1986NAN10387.

Full text

Abstract:

Implantation de différentes méthodes de démonstration automatique basées sur un algorithme de completion rapide appelé SKB et un algorithme de complétion qui privilégie la règle de simplification par rapport à celle de superposition, nous étudions cet algorithme et son implantation. Étude du filtrage pour la simplification et la réécriture des termes

APA, Harvard, Vancouver, ISO, and other styles

2

Larchey-Wendling, Dominique. "Preuves, réfutations et contre-modèles dans des logiques intuitionnistes." Nancy 1, 2000. http://www.theses.fr/2000NAN10158.

Full text

Abstract:

Les logiques sont de puissants outils qui permettent la spécification de systèmes informatiques et la preuve de l'adéquation de leurs implantations avec ces spécifications. Dans le cadre des logiques sous-structurelles, nous mettons en place des outils de démonstration automatique et de construction de contre-modèles. Ces logiques intègrent la notion de ressource ; au niveau de la recherche de preuve, la gestion des ressources permet la mise en place de procédures plus efficaces ; au niveau de l'interprétation sémantique, la notion de ressource permet de construire des modèles fidèles et complets. Nous établissons un lien entre la notion syntaxique de réfutation et la notion sémantique de contre-modèle. Nous en déduisons des méthodes de démonstration de la propriété des modèles finis ainsi que des algorithmes de construction de contre-modèles. En logique intuitionniste propositionnelle, la gestion fine de ressources permet d'en déduire une implantation efficace de la recherche de preuves. En logique intuitionniste linéaire, les modèles à base de ressources permettent une preuve élégante de la propriété des modèles finis. Nous établissons un lien entre la sémantique des ressources et la sémantique à base de réseaux de Petri, ce qui permet de raffiner les résultats de complétude partiels connus jusqu'alors
Logics can be used as powerful tools for specifying computer systems and proving the soundness of their implementations with respect to these specifications. In the field of substructural logics, we develop tools and methods for automated deduction and counter-model generation. These logics involve the notion of resource : at the level of proof-search, the management of resources enables more efficient procedures : at the semantic level, resource models provide sound and complete interpretations. We develop a link between the syntactic notion of refutation and the semantic notion of counter-model. We deduce methods for proving the finite model property and algorithms for implementation of a proof-search procedure, based on a fine management of resources. In intuitionistic linear logic, resource based models constitute the core of an elegant proof of the finite model property. Furthermore, we establish a link between resource models and Petri net based models, from which we improve the proeceding partial completness results

APA, Harvard, Vancouver, ISO, and other styles

3

Herment, Michel. "GLEF ATINF, un cadre générique pour la connexion d'outils d'inférence et l'édition graphique de preuves." Phd thesis, Grenoble INPG, 1994. http://tel.archives-ouvertes.fr/tel-00344974.

Full text

Abstract:

Après un historique bref et général de la déduction automatique, on analyse les tendances actuelles et les besoins en présentation de preuves et communication d'outils d'inférence. Les notions théoriques concernées sont présentées et étudiées en détail. On donne ensuite une synthèse comparative critique et exhaustive de l'état de l'art. Cette synthèse manquait dans la littérature. L'analyse des notions fondamentales en logique et la synthèse sur l'état de l'art permettent d'établir les caractéristiques retenues pour le système GLEF (Graphical & Logical Edition Framework). La conception et la réalisation de deux langages ont permis de rendre GLEF générique (c'est à dire paramétrable par le système formel employé et par la présentation de ses preuves). Un formalisme de définition, fondé sur le Calcul des Construction (dû à Coquand et Huet), sert à représenter et à vérifier les systèmes formels et les preuves dans ses systèmes formels. Un langage de présentation, fondé sur la notion de «boîte», sert à décrire leur présentation. En annexe nous donnons un algorithme original pour l'opération d'effacement, particulièrement difficile en lambda-calcul typé, qui sert à réaliser la commande «couper» de GLEF. GLEF a été développé au sein du projet ATINF (ATelier d'INFérence). Un manuel utilisateur rudimentaire et de nombreux exemples d'utilisation en sont donnés. Certains exemples montrent comment, après avoir spécifié la définition et la présentation d'un système formel objet, un utilisateur de GLEF peut construire ou visualiser des preuves en manipulant directement les objets (formules, preuves partielles, etc.) à l'écran, avec la souris. D'autres illustrent comment GLEF présente les preuves produites par les démonstrateurs d'ATINF ou extérieurs à ATINF. Les principales lignes de recherche future concluent ce travail

APA, Harvard, Vancouver, ISO, and other styles

4

Mohand, Oussaïd Linda. "Conception et vérification formelles des interfaces homme-machine multimodales : applications à la multimodalité en sortie." Thesis, Chasseneuil-du-Poitou, Ecole nationale supérieure de mécanique et d'aérotechnique, 2014. http://www.theses.fr/2014ESMA0022/document.

Full text

Abstract:

Les interfaces homme-machine (IHM) multimodales offrent à l’utilisateur la possibilité de combiner les modalités d’interaction afin d’augmenter la robustesse et l’utilisabilité de l’interface utilisateur d’un système. Plus particulièrement, en sortie, les IHM multimodales permettent au système de restituer à l’utilisateur, l’information produite par le noyau fonctionnel en combinant sémantiquement plusieurs modalités. Dans l’optique de concevoir de telles interfaces pour des systèmes critiques, nous avons proposé un modèle formel de conception des interfaces multimodales en sortie. Le modèle proposé se décompose en deux modèles : le modèle de fission sémantique qui décrit la décomposition de l’information à restituer en informations élémentaires, et le modèle d’allocation qui spécifie l’allocation des modalités et médias aux informations élémentaires. Nous avons également développé une formalisation B Événementiel détaillée des deux modèles : fission sémantique et allocation. Cette formalisation a été instanciée sur des études de cas puis généralisée dans un processus de développement B Événementiel cadre dans lequel s’inscrivent les modèles de fission sémantique et d’allocation. Cette formalisation a permis de procéder à la vérification de propriétés de sûreté, de vivacité et d’utilisabilité
Multimodal Human-Computer Interfaces (HCI) offer to users the possibility to combine interaction modalities in order to increase user interface robustness and usability. Specifically, output multimodal HCI allow system to return to the user, the information generated by the functional core by combining semantically different modalities. In order to design such interfaces for critical systems, we proposed a formal model for the design of output multimodal interfaces. The proposed model consists of two models: the semantic fission model describes the decomposition of the information to return into elementary information and the allocation model specifies the allocation of the elementary information with modalities and media. We have also developed a detailed Event B formalization for the two models: semantic fission and allocation. This formalization has been instantiated on case studies and generalized in an Event B development process framework including semantic fission and allocation models. This formalization allows to carry out safety, liveness and usability properties verification

APA, Harvard, Vancouver, ISO, and other styles

5

Curien, Régis. "Outils pour la preuve." Nancy 1, 1995. http://docnum.univ-lorraine.fr/public/SCD_T_1995_0007_CURIEN.pdf.

Full text

Abstract:

Le but de cette thèse est de fournir des outils permettant à la déduction automatique de réutiliser les résultats déjà obtenus. En effet, la preuve par analogie consiste à construire de nouvelles preuves à partir de preuves existantes. Il faut dans un premier temps reconnaître que le problème à résoudre est semblable à un problème déjà résolu, puis, transformer la solution existante, pour obtenir une solution du nouveau problème. L'approche adoptée consiste à définir formellement des relations liant deux formules logiques du premier ordre - celle dont nous possédons une preuve est appelée référence - pour en déduire une méthode automatique de transformation de la preuve de référence en une preuve de la nouvelle formule. Le concept d'analogie est très puissant, mais aussi très intuitif. Ainsi, pour le formaliser, nous l'avons réduit à des concepts plus simples afin de les automatiser. Nous avons défini quatre relations liant les formules, que nous appelons similitudes. Ces similitudes considèrent les propriétés de la logique propositionnelle, les propriétés des quantificateurs, le renommage des fonctions et prédicats et les propriétés associatives-commutatives des connecteurs logiques. Un outil fondamental pour la reconnaissance de ces similitudes est un algorithme de filtrage du second ordre modulo AC. La complétude et la terminaison de cet algorithme montrent la décidabilité du problème de filtrage AC du second ordre. Les transformations de preuves correspondant à ces similitudes sont données pour les preuves par expansion introduites par Miller et Pfenning. Cette représentation possède des propriétés très intéressantes pour l'analogie. Pour dépasser le stade des similitudes, nous utilisons le calcul de différence, qui utilise les échecs du filtrage. Nous montrons que lorsque la différence entre les deux formules considérées est simple, nous pouvons espérer une méthode complète d'analogie. Enfin, nous montrons, dans le cas général, et à partir d'exemples, comment l'analogie peut être envisagée par l'étude de la différence.

APA, Harvard, Vancouver, ISO, and other styles

6

Viard, Louis. "Méthodes et outils pour la programmation des systèmes cyber-physiques." Electronic Thesis or Diss., Université de Lorraine, 2021. http://www.theses.fr/2021LORR0105.

Full text

Abstract:

La conception de systèmes cyber-physiques est une discipline émergente à l'interface de nombreux domaines d'ingénierie. Ces systèmes se caractérisent notamment par une identité double, liant le monde des contrôleurs, discret, à celui du matériel, continu. Les errements d'un contrôleur, qu'ils soient dus à un programme erroné ou à la manifestation d'un aléa de l'environnement, sont susceptibles de produire des conséquences désastreuses. Une attention particulière doit donc être apportée à leur programmation. Le travail présenté dans cet ouvrage est une réponse à ce défi. Nous proposons un langage dédié à la programmation des systèmes cyber-physiques, Sophrosyne, ainsi qu'une méthode formelle de vérification des missions résultantes. Le langage repose sur des structures de supervision, permettant au système d'adapter son comportement selon la survenance d'aléas. Il présente de plus un volet de modélisation continue du système au moyen d'équations différentielles, duquel dérive la vérification formelle des missions exprimée en logique dynamique différentielle. Divers outils ont été développés autour de Sophrosyne pour assurer la planification, la compilation, l'analyse, et l'exécution de missions. Ils constituent une chaîne logicielle complète allant d'une interface graphique assistant la conception de mission jusqu'à son exécution sur le système réel. Ces outils ont été mis en œuvre sur des projets d'inspections aériennes d'infrastructures par drone. Les travaux présentés sont illustrés par ces applications drones
Building cyber-physical systems is an up-and-coming discipline which involves many engineering domains. Cyber-physical systems have a controller monitoring their physical behaviour, resulting in intertwined discrete and continuous evolution. Faulty programs or environmental hazards might lead to unwanted control and disastrous consequences. Safe operation of cyber-physical systems requires to pay dedicated attention to their programming. Our work attempts to provide a solution to this challenge. We present a domain specific language for programming cyber-physical systems, Sophrosyne, as well as a formal method to verify the correction of the resulting missions. The language is based on monitoring control structures, which provide reactive behaviours to the system. It furthermore includes continuous modelling of the system with differential equations to enable verification of missions using differential dynamic logic. Various softwares have been built to provide Sophrosyne with mission planification, compilation, analysis, and execution. Together they form a complete toolchain from a graphical user interface supporting the definition of a mission to its execution on the real system. These tools have been used to define aerial inspections of infrastructure with unmanned aircraft. We demonstrate our contribution on such applications

APA, Harvard, Vancouver, ISO, and other styles

7

Deplagne, Eric. "Système de preuve modulo récurrence." Nancy 1, 2002. http://docnum.univ-lorraine.fr/public/SCD_T_2002_0240_DEPLAGNE.pdf.

Full text

Abstract:

Les méthodes et systèmes de preuve par récurrence sont très diverses. Les méthodes les plus générales sont difficiles à automatiser. Les systèmes automatiques parfois difficiles à justifier. Cette thèse établit au niveau des preuves un lien entre récurrence noethérienne et récurrence par réécriture, ce qui permettra la coopération de systèmes dans un mode sceptique où la preuve est vérifiée grâce à l'isomorphisme de Curry-Howard. Le formalisme de la déduction modulo est étendu au traitement de congruences conditionnelles dont l'évaluation tient compte du contexte. De plus, l'ordre de récurrence qui ne peut pas être compatible avec la congruence, est rendu protecteur, c'est-à-dire qu'il bloque l'application de la congruence. La preuve par récurrence par réécriture est vue comme le résultat de l'internalisation en déduction modulo des hypothèses de récurrence, ce qui permet d'expliquer certains comportements de la méthode de récurrence par réécriture
Methods and systems for proof by induction are very different. The most general methods are difficult to automatize. Automated systems are sometimes difficult to justify. This thesis establishes at proof level a link between noetherian induction and induction bt rewriting, which will enable systems to cooperate in a skeptical mode in which the proof is verified thanks to the Curry-Howard isomorphism. The formalism of deduction modulo is extended to conditional congruences which are evaluated with respect to a context. Moreover,the induction ordering, which cannot be compatible with the congruence, is made protective, which means that it blocks the application of the congruence. Proof by induction by rewriting is seen as the result of the internalization of induction hypotheses in deduction modulo, which enables to explain some of the behavior of the induction by rewriting method

APA, Harvard, Vancouver, ISO, and other styles

8

Selhab, Sohame. "Logiques et réécriture." Nancy 1, 1998. http://www.theses.fr/1998NAN10207.

Full text

Abstract:

La première partie de notre thèse est dédiée à l'étude de l'élimination de coupures dans le calcul de séquents classique en s'appuyant sur le théorème de Gentzen (1934). Ce dernier stipule que toute preuve en calcul de séquents classique peut être transformée en une preuve normale ne faisant pas intervenir la règle de coupure. Gentzen a démontré ce résultat en décrivant une procédure de normalisation. Mais sa démonstration ainsi que celles de Tait et de Girard prouvent la terminaison de cette procédure seulement pour une stratégie particulière. La question que nous nous sommes posée est : comment montrer que la procédure d'élimination de coupures termine quelque soit la stratégie employée (une forme forte du théorème de Gentzen) ? L’approche que nous avons alors adoptée consiste à utiliser des techniques standards de réécriture. Plus précisément, nous représentons les preuves par des termes puis nous construisons un système de réécriture réalisant l'élimination de coupures. La définition de ces règles de réécriture fait abstraction de toute stratégie. La preuve de terminaison du système de réécriture construit établit alors une forme forte d'élimination de coupures pour le calcul de séquents considéré. Cette nouvelle approche produit une démonstration générique. En effet nous avons appliqué avec succès cette méthode aux calculs de séquents classique (LK), intuitionniste (LJ1) et linéaires (MALL1 et CLL). En plus de la palette de techniques de preuve de terminaison purement syntaxiques, nous avons employé des méthodes sémantiques pour la preuve de terminaison de la procédure d'élimination de coupures dans le cas des calculs MALL1 et CLL. L’avantage de cette seconde méthode est l'extraction aisée de bornes sur la longueur des séquences de réécriture. En fin de cette thèse, nous nous sommes intéressés aux travaux récents de de Groote et Kfoury & Wells qui s'apparentent à notre travail. En effet ils utilisent des méthodes à caractère syntaxique pour établir la forte normalisation de divers lambda-calculs typés. En combinant un cas particulier de la preuve de de Groote et une version modifiée de la preuve de Kfoury et Wells, nous obtenons une preuve alternative de la forte normalisation du lambda-calcul simplement typé. Cette dernière syntaxique et plus constructive utilise en partie des techniques relevant de la théorie de la réécriture.

APA, Harvard, Vancouver, ISO, and other styles

9

Noyer, Yves. "Trois études sur l'implantation des matrices en FoCaL, les preuves quantitatives et la réutilisation des preuves." Paris 6, 2010. http://www.theses.fr/2010PA066495.

Full text

Abstract:

Cette thèse part de la volonté d'implanter une bibliothèque de matrices dans l'environnement de développement sûr FoCaLize. Nous donnons une spécification dans laquelle toutes les matrices sur un même anneau commutatif unitaire sont vues comme des éléments d'une algèbre unitaire unique. Dans un tel contexte, les opérateurs d'addition et de multiplication sont des fonctions totales. Cela permet de les coder par des méthodes récursives dans un type de données ne tenant pas compte de la dimension des matrices. Nous recherchons ensuite des spécifications dans la bibliothèque FoCaLize vue comme une base de données de formules du premier ordre. La recherche d'une spécification aboutit s'il existe une formule de la bibliothèque dont l'information cherchée soit une conséquence dans le fragment de la logique du premier ordre des preuves ``quantitatives''. Celles-ci n'utilisent que les règles de quantification du calcul des séquents et se terminent par la règle axiome. Nous établissons un critère nécessaire et suffisant pour la réussite de notre recherche, retrouvant ainsi un résultat connu que nous affinons cependant. Nous donnons deux formalisations équivalentes de notre critère. Nous caractérisons l'admissibilité de la règle de coupure dans notre fragment par une méthode que nous pensons originale. Nous mettons en évidence une condition pour qu'une modification des symboles fonctionnels et relationnels dans un séquent du premier ordre permette d'obtenir un nouveau séquent possédant une preuve quantitative. Nous utilisons ce résultat pour proposer une méthode de réutilisation de preuve par analogie. Nous décrivons comment utiliser ces résultats dans le cadre de FoCaLiZe.

APA, Harvard, Vancouver, ISO, and other styles

10

Chouraqui, Jérôme. "Théorie juridique de la preuve électronique." Paris 12, 2002. http://www.theses.fr/2002PA122004.

Full text

Abstract:

Le travail traite de l'impact des nouvelles technologies au regard de la preuve. La preuve électronique, pour devenir équivalente à la preuve traditionnelle, se doit de remplir de nombreuses conditions dont : l'authenticité, l'intégrité, la non-répudiation et la fiabilité. C'est pourtant le secret qui a constitué la motivation des premières méthodes de cryptologie. Les technologies récentes ont mis en oeuvre des méthodes mathématiques complexes autour d'algorithmes tels que DES, RSA ou MD-5 pour que l'écrit électronique crypté se rapproche des qualités nécessaires de la preuve. L'enjeu de la fiablité de ces procédés se révèle essentiel dans les échanges contemporains qui tendent à se dématérialiser et dont la forme la plus courante se trouve être le commerce électronique. C'est la maturité de ces technomogies qui a été reconnue progressivement par la jurisprudence française et la Communauté européenne par le biais de la Directive du 13 décembre 1999 sur le commerce électronique. Cette dernière met en oeuvre la notion de tiers certificateur, jugée essentielle pour assurer la fiabilité des échanges virtuels. Le législateur français a consacré cette évolution dans la loi du 13 mars 2000 en reconnaissant à la signature électronique la même valeur qu'une signature manuscrite, n'en faisant qu'une. Cet événement va poser de nombreux nouveaux problèmes. Le régime de l'acte authentique, la latitude d'interprétation conférée au juge et surtout la création du prestataire de services de certification rendent l'application de la nouvelle loi complexe. Elle nécessitait donc l'adoption de plusieurs décrets d'application qui allaient notamment préciser le régime encadrant la création d'une signature électronique et les nouveaux prestataires. Le décret du 31 mars 2001, complété par celui du 18 avril 2002, décrit les processus de création d'une signature électronique et précisent les conditions dans lesquels un certificat peut être délivré de manière valable.

APA, Harvard, Vancouver, ISO, and other styles

11

Garillot, François. "Outils génériques de preuve et théorie des groupes finis." Phd thesis, Ecole Polytechnique X, 2011. http://pastel.archives-ouvertes.fr/pastel-00649586.

Full text

Abstract:

Cette thèse présente des avancées dans l'utilisation des Structures Canoniques, un mécanisme du langage de programmation de l'assistant de preuve Coq, équivalent à la notion de classes de types. Elle fournit un nouveau modèle pour le développement de hiérarchies mathématiques à l'aide d'enregistrements dépendants, et, en guise d'illustration, fournit une reformulation de la preuve formelle de correction du cryptosystème RSA, offrant des méthodes de raisonnement algébrique ainsi que la représentation en théorie des types des notions mathématiques nécessaires (incluant les groupes cycliques, les groupes d'automorphisme, les isomorphismes de groupe). Nous produisons une extension du mécanisme d'inférence de Structures Canoniques à l'aide de types fantômes, et l'appliquons au traitement de fonctions partielles. Ensuite, nous considérons un traitement générique de plusieurs formes de définitions de sous-groupes rencontrées au long de la preuve du théorème de Feit-Thomspon, une large librairie d'algèbre formelle développée au sein de l'équipe Mathematical Components au laboratoire commun MSR-INRIA. Nous montrons qu'un traitement unifié de ces 16 sous-groupes nous permet de raccourcir la preuve de leur propriétés élémentaires, et d'obtenir des définitions offrant une meilleure compositionnalité. Nous formalisons une correspondance entre l'étude de ces fonctorielles, et des propriété de théorie des groupes usuelles, telles que représentées par la classe des groupes qui les vérifie. Nous concluons en explorant les possibilités d'analyse de la fonctorialité de ces définitions par l'inspection de leur type, et suggérons une voie d'approche vers l'obtention d'instances d'un résultat de paramétricité en Coq.

APA, Harvard, Vancouver, ISO, and other styles

12

Méry, Daniel. "Preuves et sémantiques dans des logiques de ressources." Nancy 1, 2004. http://www.theses.fr/2004NAN10160.

Full text

Abstract:

Les logiques de ressources sont de puissants outils de spécification de propriétés. Dans le cadre d'une théorie mathématique des ressources, nous élaborons des méthodes de preuve qui capturent l'interaction entre les ressources par l'intermédiaire de labels et de contraintes. Nous présentons la logique BI qui, avec son interprétation en termes de partage de ressources, est un noyau commun à beaucoup de logiques de ressources. Nous développons des méthodes de preuve par tableaux et par connexions, avec construction de contre-modèles, pour le fragment cohérent de BI. Nous étendons nos méthodes de preuve à la totalité du fragment propositionnel de BI, dont nous montrons la décidabilité ainsi que la propriété des modèles finis. Nous proposons de nouvelles sémantiques complètes pour BI et spécialisons nos méthodes à la logique intuitionniste et intuitionniste linéaire multiplicative. Nous étudions les variantes affines et booléennes de BI ainsi que la logique des pointeurs
Resource-aware logics are powerful tools for specifying properties. In the context of a mathematical theory of resources, we build proof-search methods which capture the dynamic interactions between resources by means of labels and constraints. We present the BI-logic which, due to its resource-sharing interpretation, appears as the logical kernel of a wide range of resource logics. We develop tableau-based and connection-based proof-search methods, with counter-model generation facilities, for the consistent fragment of BI. We extend our proof methods to the whole fragment of propositional BI, showing that it is decidable and has the finite model property. We propose new complete semantics for BI and specialize ou methods to intuitionistic logic and intuitionistic multiplicative linear logic. We study the affine and boolean variants of BI and their links with the pointer logic

APA, Harvard, Vancouver, ISO, and other styles

13

Lagarde, Xavier. "Recevabilité et fond dans la théorie du droit de la preuve." Paris 1, 1992. http://www.theses.fr/1992PA010290.

Full text

Abstract:

Le droit de la preuve est généralement défini comme un ensemble de règles dont l'application permet la découverte de la vérité judiciaire. Pourtant une analyse approfondie, au moyen des notions de recevabilité et de fond, des mécanismes du droit de la preuve (charge de la preuve, procédés de preuve), obligé à une remise en cause de cette définition. L'objectif réel du droit de la preuve est d'accroitre la légitimité des décisions de justice, en recherchant l'assentiment des destinataires de ce droit
The law of evidence is usually defined as a body of rules providing for the discovery of judicial truth. This work analyzes in depth the mechanisms at play in the law of evidence (burden of proof, rules governing admissibility), using as a tool, the distinction between showings to be made against dismissal and showings required to win a case on the merits. The results yielded by this analysis challenge the traditional definition mentioned above and mandate that another be considered : the actual purpose of the law of evidence is to increase the legitimacy of judicial decisions, by seeking adherence thereto from those whom this body of rules addresses

APA, Harvard, Vancouver, ISO, and other styles

14

Keller, Chantal. "A Matter of Trust : Skeptical Communication between Coq and External Provers." Palaiseau, Ecole polytechnique, 2013. http://pastel.archives-ouvertes.fr/docs/00/83/83/22/PDF/thesis-keller.pdf.

Full text

Abstract:

Cette thèse présente une coopération entre l'assistant de preuve Coq et certains prouveurs externes basée sur l'utilisation de traces de preuves. Nous étudions plus particulièrement deux types de prouveurs pouvant renvoyer des certicats : d'une part, les réponses des prouveurs SAT et SMT peuvent être vériées en Coq afin d'augmenter à la fois la confiance qu'on peut leur porter et l'automatisation de Coq ; d'autre part, les théorèmes établis dans des assistants de preuves basés sur la Logique d'Ordre Supérieur peuvent être exportés en Coq et re-vérifiés, ce qui permet d'établir des preuves formelles mêlant ces deux paradigmes logiques. Cette étude a abouti à deux logiciels : SMTCoq, une coopération bi-directionnelle entre Coq et des prouveurs SAT/SMT, et HOLLIGHTCOQ, un outil important les théorèmes de HOL Light en Coq. L'architecture de chacun de ces deux développements a été pensée de manière modulaire et efficace, en établissant une séparation claire entre trois composants: un encodage en Coq du formalisme de l'outil externe qui est ensuite traduit avec soin vers des termes Coq, un vérificateur certifié pour établir les preuves, et un pré-processeur écrit en Ocaml traduisant les traces venant de prouveurs différents dans le même format de certicat. Grâce à cette séparation, un changement dans le format de traces n'affecte que le pré-processeur, sans qu'il soit besoin de modier du code ou des preuves Coq. Un autre composant essentiel pour l'efficacité et la modularité est la réflexion calculatoire, qui utilise les capacités de calcul de Coq pour établir des preuves à la fois courtes et génériques à partir des certificats
This thesis studies the cooperation between the Coq proof assistant and external provers through proof witnesses. We concentrate on two different kinds of provers that can return certicates: first, answers coming from SAT and SMT solvers can be checked in Coq to increase both the confidence in these solvers and Coq's automation; second, theorems established in interactive provers based on Higher-Order Logic can be exported to Coq and checked again, in order to offer the possibility to produce formal developments which mix these two dierent logical paradigms. It ended up in two software: SMTCoq, a bi-directional cooperation between Coq and SAT/SMT solvers, and HOLLIGHTCOQ, a tool importing HOL Light theorems into Coq. For both tools, we took great care to define a modular and efficient architecture, based on three clearly separated ingredients: an embedding of the formalism of the external tool inside Coq which is carefully translated into Coq terms, a certified checker to establish the proofs using the certicates, and an Ocaml preprocessor to transform proof witnesses coming from different provers into a generic certificate. This division allows that a change in the format of proof witnesses only affects the preprocessor, but no proved Coq code. Another fundamental component for efficiency and modularity is computational reflection, which exploits the computational power of Coq to establish generic and small proofs based on the certicates

APA, Harvard, Vancouver, ISO, and other styles

15

Espinasse, Franck. "Théorie générale des perquisitions." Nice, 1997. http://www.theses.fr/1997NICE0022.

Full text

Abstract:

La perquisition est une mesure d'investigation permettant de saisir certains éléments susceptibles de faciliter la manifestation de la vérité. Un tel résultat ne peut être obtenu qu'au moyen de règles contraignantes à l'égard de l'individu et par une limitation des droits et libertés qui lui sont pourtant conférés. Ces règles s'appliquent enfin dans le domaine réservé jusqu'alors à la visite domicilaire, puisque les pouvoirs dont sont investis certains agents spéciaux annihilent désormais cette ancienne distinction. En conséquence, une perquisition, issue en grande partie de règles dérogatoires, cohabite aux côtés de la perquisition de droit commun. La perquisition envisagée dans sa diversité, au plan national et communautaire, obéit à un certain nombre de règles protectrices, qui parviennent difficilement à concilier le nécessaire respect de l'ordre public avec la protection de l'individu dans sa vie privée. Ainsi, la perquisition exprime un déséquilibre qui fait primer la contrainte dans la manifestation de la vérité au détriment de la protection des individus. Les juges judiciaires, constitutionnels, communautaires et européens usent alors de leurs prérogatives afin qu'un équilique respectueux de ces objectifs soit obtenu. Toutefois, cette thèse met en relief les difficultés auxquelles les juges sont confrontés dans le développement de la protection recherchée. Le seul moyen d'atteindre un tel résultat passe par une unification des sources de la perquisition au plan communautaire, et la création d'un mandat de perquisition intégrant les règles protectrices de la convention européenne des droits de l'Homme.

APA, Harvard, Vancouver, ISO, and other styles

16

Houtmann, Clément. "Représentation et interaction des preuves en superdéduction modulo." Electronic Thesis or Diss., Nancy 1, 2010. http://www.theses.fr/2010NAN10026.

Full text

Abstract:

Cette thèse propose et étudie de nouveaux systèmes déductifs mêlant calculs et déductions. La déduction modulo est un premier formalisme qui traduit un pouvoir calculatoire grâce à un système de réécriture. Nous présentons un paradigme dual appelé superdéduction qui traduit un pouvoir déductif par de nouvelles inférences. Ces pouvoirs calculatoires et déductifs modifient la représentation des preuves et leur interaction par les processus d'élimination des coupures. La normalisation forte ou l'admissibilité des coupures ne sont plus garanties et apparaissent alors comme des propriétés intrinsèques des théories représentées sous forme de systèmes de réécriture. Nous démontrons que certains critères permettent d'assurer ces propriétés, notamment en définissant un langage de termes de preuve pour la superdéduction et en étudiant la permutabilité des inférences en calcul des séquents classique. Notre attention est focalisée sur les calculs des séquents classiques et la représentation des preuves dans de tels systèmes. D'autres formalismes connexes sont envisagés, notamment les réseaux de preuve et le focusing. Nous comparons cette dernière approche à la superdéduction, ce qui nous amène à proposer une refonte du paradigme de superdéduction basée sur un système de multifocusing pour la logique classique. Nous en montrons les effets bénéfiques en démontrant la complétude des systèmes déductifs obtenus
In this thesis we propose and study several deduction systems that mix deduction and computation. Deduction modulo proposes to translate a computational power through a rewriting system. We present the dual concept called superdeduction. It translates a deductive power into custom inference rules that enrich the deduction system. These computational and deductive powers modify the representation of proofs as well as their interaction through cut-elimination processes. Strong normalisation or cut-admissibility may be lost and therefore appear as intrinsic properties of theories represented as rewriting systems. We prove that certain criteria imply these properties by defining a proof-term language for superdeduction and by studying the permutability of inferences in classical sequent calculus. Our attention is focused on classical sequent calculi and on the representation of proofs in such systems. Other related paradigms are considered, namely proof-nets and focusing. We compare this latter approach with superdeduction. We consequently reforge the superdeduction paradigm on top of a multifocusing system for classical logic. We demonstrate the benefits of this approach by proving the completeness of the obtained deduction systems

APA, Harvard, Vancouver, ISO, and other styles

17

Houtmann, Clément. "Représentation et interaction des preuves en superdéduction modulo." Phd thesis, Université Henri Poincaré - Nancy I, 2010. http://tel.archives-ouvertes.fr/tel-00553219.

Full text

Abstract:

Cette thèse propose et étudie de nouveaux systèmes déductifs mêlant calculs et déductions. La déduction modulo est un premier formalisme qui traduit un pouvoir calculatoire grâce à un système de réécriture. Nous présentons un paradigme dual appelé superdéduction qui traduit un pouvoir déductif par de nouvelles inférences. Ces pouvoirs calculatoires et déductifs modifient la représentation des preuves et leur interaction par les processus d'élimination des coupures. La normalisation forte ou l'admissibilité des coupures ne sont plus garanties et apparaissent alors comme des propriétés intrinsèques des théories représentées sous forme de systèmes de réécriture. Nous démontrons que certains critères permeent d'assurer ces propriétés, notamment en définissant un langage de termes de preuve pour la superdéduction et en étudiant la permutabilité des inférences en calcul des séquents classique. Notre attention est focalisée sur les calculs des séquents classiques et la représentation des preuves dans de tels systèmes. D'autres formalismes connexes sont envisagés, notamment les réseaux de preuve et le focusing. Nous comparons cette dernière approe à la superdéduction, ce qui nous amène à proposer une refonte du paradigme de superdéduction basée sur un système de multifocusing pour la logique classique. Nous en montrons les effets bénéfiques en démontrant la complétude des systèmes déductifs obtenus.

APA, Harvard, Vancouver, ISO, and other styles

18

Lazrek, Azzeddine. "Étude et réalisation de méthodes de preuve par récurrence en logique équationnelle." Vandoeuvre-les-Nancy, INPL, 1988. http://www.theses.fr/1988NAN10380.

Full text

Abstract:

Développement d'un outil puissant pour la programmation logique et/ou fonctionnelle et pour la démonstration automatique. L’objectif principal est l'étude et la mise en œuvre d'une méthode de preuve de théorèmes inductifs dans l'algèbre initiale d'une variété équationnelle. La méthode étudiée est la synthèse de la méthode de preuve par consistance et de celle basée sur la réductibilité inductive. Le deuxième objectif est l'étude de la complétude relative, souhaitable dans la conception et la correction des spécifications algébriques structurées et requise par la méthode de preuve par consistance

APA, Harvard, Vancouver, ISO, and other styles

19

Saïbi, Amokrane. "Outils Génériques de Modélisation et de Démonstration pour la Formalisation des Mathématiques en Théorie des Types : application à la Théorie des Catégories." Paris 6, 1999. https://tel.archives-ouvertes.fr/tel-00523810.

Full text

APA, Harvard, Vancouver, ISO, and other styles

20

Duquesne, Eric. "Réseaux de preuve, types principaux et lambda-termes." Paris 7, 1992. http://www.theses.fr/1992PA077240.

Full text

Abstract:

Dans la théorie de la démonstration, la logique intuitionniste (LI) de brouwer et la logique linéaire (LL) de Girard définissent des preuves constructives (ou calculables) des formules mathématiques. Grâce à l'isomorphisme entre l'ensemble des preuves intuitionnistes et l'ensemble des lambda-termes types (curry-howard) et grâce à l'isomorphisme entre le lambda-calcul (non type) et l'ensemble des fonctions calculables par machine de Turing (Turing, Kleene), LI fait du lambda-calcul un modèle de langage de programmation par preuve. Le contenu du chapitre 4 contribue à faire jouer à ll un rôle analogue. Le fragment de LL considéré est le fragment multiplicatif et exponentiel avec les polarités de Danos et Regnier. L'ensemble des preuves est une traduction du lambda-calcul. Les preuves sont représentées par des structures de preuve sans concept de boites; la construction d'un espace cohérent modèle du lambda calcul (ch. 0) et de l'ensemble des réseaux de preuve fournit cette nouvelle définition en termes de graphes (ch. 1). Les structures de preuve (sans coupures) sont classifiées (ch. 3). En particulier les réseaux de preuve sans coupures sont les structures de preuve qui vérifient un critère de correction analogue à celui de Girard pour le fragment multiplicatif de LL. Ils correspondent aux lambda-termes normaux (ch. 4) et aux types principaux (ch. 5)

APA, Harvard, Vancouver, ISO, and other styles

21

Méhats, Laurent. "Théorie de la preuve des catégories monoïdales symétriques fermées : cohérence et équivalences de dérivations." Toulouse 3, 2005. http://www.theses.fr/2005TOU30238.

Full text

Abstract:

Cette thèse étudie la cohérence c. -à-d. L'égalité de morphismes canoniques dans les catégories monoïdales symétriques fermée (smcc) libres et non libres, via la théorie de la preuve de la logique linéaire multiplicative intuitionniste (imll) avec unité. L'étude de la cohérence dans les modèles non libres est réduite à l'étude d'équivalences de termes de la catégorie libre, plus fortes que l'équivalence induite par la structure de smcc libre. La catégorie libre est reformulée comme le système de séquents d'imll avec unité, de sorte que seules les équivalences de dérivations de ce système sont à considérer. Nous établissons que deux dérivations sans coupure sont équivalentes relativement à la structure de smcc libre si et seulement si elles sont inter-permutables, et que toute équivalence plus forte est axiomatisée par un ensemble de paires critiques de dérivations. Nous en déduisons l'incomplétude de Post du système d'égalités des smcc et des conditions suffisantes de pleine cohérence
This PhD thesis studies coherence, that is the equality of canonical morphisms in free and non free symmetric monoidal closed categories (smcc), using proof theory for intuitionistic multiplicative linear logic (imll) with unit. The study of coherence in non free models is reduced to the study of equivalences of terms of the free category, which are stronger than the equivalence induced by the free smcc structure. The free category is reformulated as the sequent calculus for imll with unit, so that only the equivalences of derivations in this system are to be considered. We establish that two cut-free derivations are equivalent w. R. T. The free smcc structure if and only if they are inter-permutable, and that any stronger equivalence is axiomatized by a set of critical pairs of derivations. From this, we deduce that the system of equalities for smcc is not Post-complete and we also deduce certain sufficient conditions for full coherence

APA, Harvard, Vancouver, ISO, and other styles

22

Vanzetto, Hernán. "Automatisation des preuves et synthèse des types pour la théorie des ensembles dans le contexte de TLA+." Thesis, Université de Lorraine, 2014. http://www.theses.fr/2014LORR0208/document.

Full text

Abstract:

Cette thèse présente des techniques efficaces pour déléguer des obligations de preuves TLA+ dans des démonstrateurs automatiques basées sur la logique du premier ordre non-sortée et multi-sortée. TLA+ est un langage formel pour la spécification et vérification des systèmes concurrents et distribués. Sa partie non-temporelle basée sur une variante de la théorie des ensembles Zermelo-Fraenkel permet de définir des structures de données. Le système de preuves TLAPS pour TLA+ est un environnement de preuve interactif dans lequel les utilisateurs peuvent vérifier de manière déductive des propriétés de sûreté sur des spécifications TLA+. TLAPS est un assistant de preuve qui repose sur les utilisateurs pour guider l’effort de preuve, il permet de générer des obligations de preuve puis les transmet aux vérificateurs d’arrière-plan pour atteindre un niveau satisfaisant d’automatisation. Nous avons développé un nouveau démonstrateur d’arrière-plan qui intègre correctement dans TLAPS des vérificateurs externes automatisés, en particulier, des systèmes ATP et solveurs SMT. Deux principales composantes constituent ainsi la base formelle pour la mise en oeuvre de ce nouveau vérificateur. Le premier est un cadre de traduction générique qui permet de raccorder à TLAPS tout démonstrateur automatisé supportant les formats standards TPTP/ FOF ou SMT-LIB/AUFLIA. Afin de coder les expressions d’ordre supérieur, tels que les ensembles par compréhension ou des fonctions totales avec des domaines, la traduction de la logique du premier ordre repose sur des techniques de réécriture couplées à une méthode par abstraction. Les théories sortées telles que l’arithmétique linéaire sont intégrés par injection dans la logique multi-sortée. La deuxième composante est un algorithme pour la synthèse des types dans les formules (non-typées) TLA+. L’algorithme, qui est basé sur la résolution des contraintes, met en oeuvre un système de type avec types élémentaires, similaires à ceux de la logique multi-sortée, et une extension avec des types dépendants et par raffinement. Les informations de type obtenues sont ensuite implicitement exploitées afin d’améliorer la traduction. Cette approche a pu être validé empiriquement permettant de démontrer que les vérificateurs ATP/SMT augmentent de manière significative le développement des preuves dans TLAPS
This thesis presents effective techniques for discharging TLA+ proof obligations to automated theorem provers based on unsorted and many-sorted first-order logic. TLA+ is a formal language for specifying and verifying concurrent and distributed systems. Its non-temporal fragment is based on a variant of Zermelo-Fraenkel set theory for specifying the data structures. The TLA+ Proof System TLAPS is an interactive proof environment in which users can deductively verify safety properties of TLA+ specifications. While TLAPS is a proof assistant that relies on users for guiding the proof effort, it generates proof obligations and passes them to backend verifiers to achieve a satisfactory level of automation. We developed a new back-end prover that soundly integrates into TLAPS external automated provers, specifically, ATP systems and SMT solvers. Two main components provide the formal basis for implementing this new backend. The first is a generic translation framework that allows to plug to TLAPS any automated prover supporting the standard input formats TPTP/FOF or SMT-LIB/AUFLIA. In order to encode higher-order expressions, such as sets by comprehension or total functions with domains, the translation to first-order logic relies on term-rewriting techniques coupled with an abstraction method. Sorted theories such as linear integer arithmetic are homomorphically embedded into many-sorted logic. The second component is a type synthesis algorithm for (untyped) TLA+ formulas. The algorithm, which is based on constraint solving, implements one type system for elementary types, similar to those of many-sorted logic, and an expansion with dependent and refinement types. The obtained type information is then implicitly exploited to improve the translation. Empirical evaluation validates our approach: the ATP/SMT backend significantly boosts the proof development in TLAPS

APA, Harvard, Vancouver, ISO, and other styles

23

El, haddad Yacine. "Integrating Automated Theorem Provers in Proof Assistants." Electronic Thesis or Diss., université Paris-Saclay, 2021. http://www.theses.fr/2021UPASG052.

Full text

Abstract:

Lambdapi est un assistant de preuve qui permet à l’utilisateur la construction d’une preuve d’un théorème donné dans un langage universel basé sur le lambda-pi-calcul. Le but de cette thèse est de rajouter de l’automatisation à Lambdapi pour faire gagner du temps à l’utilisateur. Cette thèse présente trois contributions liées à l’intégration des démonstrateurs automatiques dans les assistants de preuve. La première contribution consiste en l’implémentation d’une tactique qui fait appel au démonstrateurs automatiques depuis Lambdapi à travers une plateforme tiers appelé Why3. Généralement, les démonstrateurs automatiques ne génèrent pas un certificat de preuve complet, d’où la deuxième contribution présentée dans cette thèse: la reconstruction de preuves générées par les démonstrateurs automatiques du premier ordre dans Lambdapi implémenté dans un outil appelé Ekstrakto. Enfin, ces démonstrateurs peuvent parfois effectuer des modifications sur la formule qu'ils sont en train de prouver. Le dernier résultat de la thèse est consacré à la certification des étapes de Skolemisation faites par les démonstrateurs automatiques. Un algorithme est présenté, montré correct et impleménté dans l'outil Skonverto
Lambdapi is a proof assistant that allows users to construct a proof of a given theorem in a universal language based on the lambda-pi-calculus. The goal of this thesis is to add more automation to Lambdapi to gain more time and effort for the users. This thesis presents three contributions associated with the integration of automated provers in proof assistants. The first contribution consists of the implementation of a tactic that calls automated provers from Lambdapi by using an external platform called Why3. Usually, automated provers do not generate a complete certificate of a given formula, thus, the second contribution presented in this thesis is the reconstruction in Lambdapi of proofs generated by first-order automated provers implemented in a tool called Ekstrakto. Finally, automated provers often perform some transformations on the formula that they are trying to solve. Among these transformations, we can find Skolemization steps. The last contribution is devoted to the certification of Skolemization steps performed by the automated provers in order to have a complete reconstruction. This has been implemented in a tool called Skonverto

APA, Harvard, Vancouver, ISO, and other styles

24

Paulin-Mohring, Christine. "Définitions Inductives en Théorie des Types." Habilitation à diriger des recherches, Université Claude Bernard - Lyon I, 1996. http://tel.archives-ouvertes.fr/tel-00431817.

Full text

Abstract:

Ce document donne un panorama de la représentation des définitions inductives dans différents assistants de preuve en logique d'ordre supérieur, théorie des ensembles et théorie des types. Il présente, étudie et justifie les choix faits dans le système Coq.

APA, Harvard, Vancouver, ISO, and other styles

25

Mahboubi, Assia. "Contributions à la certification des calculs dans R : théorie, preuves, programmation." Phd thesis, Université de Nice Sophia-Antipolis, 2006. http://tel.archives-ouvertes.fr/tel-00117409.

Full text

Abstract:

Le logiciel Coq est un assistant à la preuve basé sur le Calcul des
Constructions Inductives.
Dans cette thèse nous proposons d'améliorer l'automatisation de ce
système en le dotant d'une procédure de décision réflexive et complète
pour la théorie du premier ordre de l'arithmétique réelle.
La théorie des types implémentée par le système Coq comprend un
langage fonctionnel typé dans lequel nous avons programmé un
algorithme de Décomposition Algébrique Cylindrique (CAD). Cet
algorithme calcule une partition de l'espace en cellules
semi-algébriques sur lesquelles tous les polynômes d'une famille donnée
ont un signe constant et permet ainsi de décider les formules de cette théorie.
Il s'agit ensuite de prouver la correction de l'algorithme et de la
procédure de décision associée avec l'assistant à la preuve Coq.
Ce travail comprend en particulier une librairie d'arithmétique polynomiale
certifiée et une partie significative de la preuve formelle de correction de
l'algorithme des sous-résultants. Ce dernier algorithme permet de calculer
efficacement le plus grand commun diviseur de polynômes à coefficients dans un
anneau, en particulier à plusieurs variables.
Nous proposons également une tactique réflexive de décision des égalités dans les
structures d'anneau et de semi-anneaux qui améliore les performances de l'outil
déjà disponible et augmente son spectre d'action en exploitant les possibilités de
calcul du système.
Dans une dernière partie, nous étudions le contenu calculatoire d'une preuve
constructive d'un lemme élémentaire d'analyse réelle, le principe d'induction
ouverte.

APA, Harvard, Vancouver, ISO, and other styles

26

Boite, Olivier. "Une aide à la réutilisation de preuves formelles : application aux preuves de propriétés sémantiques." Paris, CNAM, 2005. http://www.theses.fr/2005CNAM0499.

Full text

Abstract:

Les preuves formelles sont longues et délicates. Puisque l'automatisation n'est pas toujours possible, il est capital de pouvoir réutiliser les preuves existantes, afin d'accroître l'utilisation des méthodes formelles dans le monde industriel. Comme de nombreux problèmes se modélisent de manière inductive, et comme il est fréquent d'étendre le modèle pas-à-pas, nous proposons un ensemble de commandes permettant la modification de spécifications inductives, et permettant la réutilisation des preuves associées. Notre méthode de réutilisation génère des obligations de preuve lorsque les preuves nécessitent d'être complétées. Cet environnement de réutilisation est implémenté dans l'assistant à la preuve Coq. Un calcul de dépendances permet de prévoir les modifications à faire lors d'une réutilisation des preuves associées. Notre métode de réutilisation génère des obligations de preuve lorsque les preuves nécessitent d'être complétées. Cet environnement de réutilisation est implémenté dans l'assistant à la preuve Coq. Un calcul de dépendances permet de prévoir les modifications à faire lors d'une réutilisation. A chaque commande est associée une méthode de réutilisation automatique, prouvée correcte vis à vis du typage, certifiant ainsi l'utilisation de notre environnement de réutilisation
Formal proofs are long and difficult. As automation is not always possible, it is capital to be able to reuse existing proofs, in order to increase the use of the formal methods in the industrial world. As many problems are modelled in an inductive way, and as it is frequent to extend the model and allowing the reuse the associated proofs. Our reusing method generates proof obligations when the proof requires to be supplemented. This reusing environment is implemented in the Coq proof assistant. A computation of dependances allows to envisage the modifications to be made during the reuse process. Each command is associated with an automatic reuse method, proven correct with respect to typing, certifying the use of our reusing environment

APA, Harvard, Vancouver, ISO, and other styles

27

Puitg, François. "Preuves en modélisation géométrique par le calcul des constructions inductives." Université Louis Pasteur (Strasbourg) (1971-2008), 1999. http://www.theses.fr/1999STR13032.

Full text

Abstract:

Cette étude présente un nouveau développement de techniques formelles de spécification et de preuve en modélisation géométrique. Le modèle topologique des cartes combinatoires est axiomatisé dans le calcul des constructions inductives (CCI), une théorie des types bien adaptée à la mécanisation des mathématiques en logique d'ordre supérieur. Une hiérarchie de types abstraits spécifiant les cartes combinatoires est construite et validée par des preuves inductives de consistance et de complétude dans le système Coq, un assistant à la preuve implantant le CCI. Un prototype certifié est obtenu par l'extraction automatique d'algorithmes fonctionnels des preuves constructives de leur correction. Des difficultés classiques en spécification formelle et preuve de théorèmes - comme la cohabitation d'objets et de leur généralisation dans la même hiérarchie, la gestion élégante du sous-typage, la complétion de relations et d'objets partiels, la confrontation des approches constructive et observationnelle, et la symétrisation de relations - sont abordées, non seulement sur le plan des spécifications formelles et de la preuve, mais aussi du point de vue de l'extraction. Grâce notamment à la nouvelle notion de quasi-face, des questions délicates de modélisation géométrique - comme la notion de face, l'énoncé d'un critère de planarité, la preuve de la formule d'Euler et d'un théorème de Jordan topologique - sont ainsi résolues d'une façon originale et incontestable, offrant une grande pénétration des fondements topologiques de la modélisation géométrique et une profonde compréhension du modèle. Une méthodologie de spécification et de preuve applicable à d'autres domaines est enfin proposée.

APA, Harvard, Vancouver, ISO, and other styles

28

Cousineau, Denis. "Modèles et normalisation des preuves." Phd thesis, Ecole Polytechnique X, 2009. http://tel.archives-ouvertes.fr/tel-00433165.

Full text

Abstract:

La notion de théorie s'est séparée de la notion de logique à la ﬁn des années 1920, lorsque Hilbert et Ackermann ont distingué les règles de déduction, indépendantes de l'ob jet du discours, des axiomes qui lui sont spéciﬁques. S'est alors posée la question de caractériser les théories, déﬁnies donc comme des ensembles d'axiomes, que l'on peut utiliser pour formaliser une partie du raisonnement mathématique. Un premier critère est la cohérence de cette théorie : le fait qu'on ne puisse pas démontrer toutes les propositions de cette théorie. Cependant il est progressivement apparu que la cohérence n'était pas une propriété suﬃsante. Le fait que les démonstrations constructives vériﬁent les propriétés de la dijonction ou du témoin, ou la complétude de certaines méthodes de démonstration automatique ne découlent pas de la seule cohérence d'une théorie. Mais toutes trois sont par contre conséquentes d'une même propriété : la normalisation des démonstrations. En 1930, le théorème de complétude de Gödel montra que le critére de cohérence pouvait être vu sous diﬀérents angles. En plus de la déﬁnition précédente interne à la théorie de la démonstration, on peut également déﬁnir de manière algébrique la cohérence d'une théorie comme le fait qu'elle possède un modèle. L'équivalence entre ces deux déﬁnitions constitue un outil fondamental, qui a permis notamment la démonstration de la cohérence de nombreuses théories : la théorie des ensembles avec la négation de l'axiome du choix par Fraenkel et Mostovski, la théorie des ensembles avec l'axiome du choix et l'hypothèse du continue par Gödel, la théorie des ensembles avec la négation de l'hypothèse du continu par Cohen, . . . A l'inverse, la normalisation des démonstrations semblait ne pouvoir se déﬁnir que de manière interne à la théorie de la démonstration. Certains critères inspirés de la théorie des modèles étaient certes parfois utilisés pour démontrer la propriété de normalisation des démonstrations de certaines théories, mais la nécéssité de ces critéres n'avait pas été établie. Nous proposons dans cette thèse un critère algébrique à la fois nécessaire et suﬃsant pour la normalisation des démonstrations. Nous montrons ainsi que la propriété de normalisation des démonstrations peut également se déﬁnir comme un critère algébrique, à l'instar de la propriété de cohérence. Nous avons pour cela déﬁni une nouvelle notion d'algèbre de valeurs de vérités (TVA) appelée algèbres de vérité dépendant du langage (LDTVA). La notion de TVA permet d'exhiber l'algèbre de valeurs de vérité des candidats de réductibilité déﬁnis par Girard en 1970. L'existence d'un modèle à valeurs dans cette algèbre déﬁnit un critère algébrique suﬃsant pour la propriété de normalisation des démonstrations. Puis nous avons déﬁni un raﬃnement de la notion de candidats de réductibilité comme une de ces LDTVAs et avons montré que l'existence d'un modèle à valeurs dans cette algèbre déﬁnit un critère algébrique toujours suﬃsant mais également nécessaire pour la propriété de normalisation des démonstrations. Ce critère est déﬁni pour les cadres logiques de la déduction minimale et du λΠ-calcul modulo. Et nous exhibons ﬁnalement la puissance du λΠ-calcul modulo en montrant que tous les systèmes de types purs fonctionnels peuvent être simulés dans ce cadre logique.

APA, Harvard, Vancouver, ISO, and other styles

29

Deshayes, Fred. "Contribution à une théorie de la preuve devant la Cour européenne des droits de l'homme." Montpellier 1, 2002. http://www.theses.fr/2002MON10034.

Full text

Abstract:

La preuve est un instrument de la recherche de l'effectivité du contrôle effectué par la Cour européenne des droits de l'homme. Par touches successives, à force d'emprunts et d'originalité, cette juridiction a modelé son système probatoire afin qu'il réponde aux défis de la protection des droits de l'homme. Dans le domaine du droit à la preuve, son action a consisté à promouvoir la cause de l'individu au moyen d'un aménagement différencié des conditions d'exercice de cette faculté. Pour ce qui est de l'attribution de la charge de la preuve, elle a procédé avec plus de nuance ; si elle garantit l'équilibre du procès, elle décide au cas par cas de la cause qui l'emporte au bénéfice du doute en rendant son jugement. Ainsi, en dépit des imperfections que l'on peut constater, par l'usage des règles et des raisonnements qui forment son système probatoire, la Cour européenne des droits de l'homme a pu inscrire dans la réalité du droit des idéaux qui sont au fondement de la convention.

APA, Harvard, Vancouver, ISO, and other styles

30

Notin, Jean-Marc. "Recherche et construction de preuves en logique non-commutative." Nancy 1, 2004. http://www.theses.fr/2004NAN10183.

Full text

Abstract:

La logique NL étend la logique linéaire en y ajoutant des connecteurs non-commutatifs. Sa particularité vient des interactions entre les connecteurs commutatifs et non-commutatifs. Une première étude nous a conduit à analyser ces interactions dans le cadre des réseaux de preuve. Leur prise en compte lors de la recherche de preuves par composition (construction) nécessite l'introduction de structures spécifiques (labels, graphes de dépendances). Nous proposons ainsi plusieurs algorithmes de construction de réseaux de preuve pour le fragment multiplicatif de NL. Une autre approche étudiée est celle de la recherche de preuves par décomposition, mise en oeuvre en particulier dans le cadre des méthodes des connexions. En utilisant des labels associés aux sous-formules, et des contraintes exprimées sur ces labels, nous proposons une caractérisation par les connexions pour MNL. La méthode des connexions associée peut être vue comme un nouvel algorithme de construction de réseaux de preuve
Partially commutative logics allow to express properties mixing concurency and sequentiality. Thus, the logic NL extends linear logic with non-commutative connectives. The characteristic of NL comes from the interactions between commutative and non-commutative connectives. A first study led us to analyze these interactions within the framework of proof nets. Taking such interactions into account during top-down proof search (proof nets construction) requires the introduction of specific structures (labels, dependency sets). Thus, we propose several algorithms for building proof nets in the multiplicative fragment of NL (MNL). Another studied approach is bottom-up proof search, in particular within the framework of connection methods. By using labels associated with the subformulas, and constraints expressed on these labels, we propose a connection characterization for MNL. The associated connection method can be seen like a new algorithm for proof nets construction in MNL

APA, Harvard, Vancouver, ISO, and other styles

31

Vanzetto, Hernán. "Automatisation des preuves et synthèse des types pour la théorie des ensembles dans le contexte de TLA+." Electronic Thesis or Diss., Université de Lorraine, 2014. http://www.theses.fr/2014LORR0208.

Full text

Abstract:

Cette thèse présente des techniques efficaces pour déléguer des obligations de preuves TLA+ dans des démonstrateurs automatiques basées sur la logique du premier ordre non-sortée et multi-sortée. TLA+ est un langage formel pour la spécification et vérification des systèmes concurrents et distribués. Sa partie non-temporelle basée sur une variante de la théorie des ensembles Zermelo-Fraenkel permet de définir des structures de données. Le système de preuves TLAPS pour TLA+ est un environnement de preuve interactif dans lequel les utilisateurs peuvent vérifier de manière déductive des propriétés de sûreté sur des spécifications TLA+. TLAPS est un assistant de preuve qui repose sur les utilisateurs pour guider l’effort de preuve, il permet de générer des obligations de preuve puis les transmet aux vérificateurs d’arrière-plan pour atteindre un niveau satisfaisant d’automatisation. Nous avons développé un nouveau démonstrateur d’arrière-plan qui intègre correctement dans TLAPS des vérificateurs externes automatisés, en particulier, des systèmes ATP et solveurs SMT. Deux principales composantes constituent ainsi la base formelle pour la mise en oeuvre de ce nouveau vérificateur. Le premier est un cadre de traduction générique qui permet de raccorder à TLAPS tout démonstrateur automatisé supportant les formats standards TPTP/ FOF ou SMT-LIB/AUFLIA. Afin de coder les expressions d’ordre supérieur, tels que les ensembles par compréhension ou des fonctions totales avec des domaines, la traduction de la logique du premier ordre repose sur des techniques de réécriture couplées à une méthode par abstraction. Les théories sortées telles que l’arithmétique linéaire sont intégrés par injection dans la logique multi-sortée. La deuxième composante est un algorithme pour la synthèse des types dans les formules (non-typées) TLA+. L’algorithme, qui est basé sur la résolution des contraintes, met en oeuvre un système de type avec types élémentaires, similaires à ceux de la logique multi-sortée, et une extension avec des types dépendants et par raffinement. Les informations de type obtenues sont ensuite implicitement exploitées afin d’améliorer la traduction. Cette approche a pu être validé empiriquement permettant de démontrer que les vérificateurs ATP/SMT augmentent de manière significative le développement des preuves dans TLAPS
This thesis presents effective techniques for discharging TLA+ proof obligations to automated theorem provers based on unsorted and many-sorted first-order logic. TLA+ is a formal language for specifying and verifying concurrent and distributed systems. Its non-temporal fragment is based on a variant of Zermelo-Fraenkel set theory for specifying the data structures. The TLA+ Proof System TLAPS is an interactive proof environment in which users can deductively verify safety properties of TLA+ specifications. While TLAPS is a proof assistant that relies on users for guiding the proof effort, it generates proof obligations and passes them to backend verifiers to achieve a satisfactory level of automation. We developed a new back-end prover that soundly integrates into TLAPS external automated provers, specifically, ATP systems and SMT solvers. Two main components provide the formal basis for implementing this new backend. The first is a generic translation framework that allows to plug to TLAPS any automated prover supporting the standard input formats TPTP/FOF or SMT-LIB/AUFLIA. In order to encode higher-order expressions, such as sets by comprehension or total functions with domains, the translation to first-order logic relies on term-rewriting techniques coupled with an abstraction method. Sorted theories such as linear integer arithmetic are homomorphically embedded into many-sorted logic. The second component is a type synthesis algorithm for (untyped) TLA+ formulas. The algorithm, which is based on constraint solving, implements one type system for elementary types, similar to those of many-sorted logic, and an expansion with dependent and refinement types. The obtained type information is then implicitly exploited to improve the translation. Empirical evaluation validates our approach: the ATP/SMT backend significantly boosts the proof development in TLAPS

APA, Harvard, Vancouver, ISO, and other styles

32

Lengrand, Stéphane. "Normalisation et équivalence en théorie de la démonstration et théorie des types." Paris 7, 2006. http://www.theses.fr/2006PA077040.

Full text

Abstract:

Au coeur des liens entre Théorie de la Démonstration et Théorie des Types, la correspondance de Curry-Howard fournit des termes de preuves aux aspects calculatoires et équipés de théories équationnelles, i. E. Des notions de normalisation et d'équivalence. Cette thèse étend son cadre à des formalismes (comme le calcul des séquents) appropriés à des considérations d'ordre logique comme la recherche de preuve, à des systèmes expressifs dépassant la logique propositionnelle comme des théories des types, et aux raisonnements classiques plutôt qu'intuitionistes. La première partie est intitulée « Termes de Preuve pour la Logique Intuitioniste Implicationnelle », avec des contributions en déduction naturelle et calcul des séquents, normalisation et élimination des coupures, sémantiques en appel par nom et par valeur. En particulier elle introduit des calculs de termes de preuve pour le calcul des séquents depth-bounded G4 et la déduction naturelle multiplicative. Cette dernière donne lieu à un calcul de substitutions explicites avec affaiblissements et contractions, qui raffine la beta-reduction. La deuxième partie, intitulée « Théorie des Types en Calcul des Séquents », développe une théorie des Pure Type Sequent Calcul!, équivalents aux Systèmes de Types Purs mais mieux adaptés à la recherche de preuve. La troisième partie, intitulée « Vers la Logique Classique », étudie des approches à la Théorie des Types classique. Elle développe un calcul des séquents pour une version classique du Système Fomega. Une approche à la question de l'équivalence de preuves classiques consiste à calculer les représentants canoniques de preuves équivalentes dans le cadre du Calcul des Structures
At the heart of the connections between Proof Theory and Type Theory, the Curry-Howard correspondence provides proof-terms with computational features and equational theories, i. E. Notions of normalisation and equivalence. This dissertation extends its framework in the directions of proof-theoretic formalisms (such as sequent calculus) that are appealing for logical purposes like proof-search, powerful Systems beyond propositional logic such as type theories, and classical (rather than intuitionistic) reasoning. Part I is entitled Proof-terms for Intuitionistic Implicational Logic, with contributions in natural deduction, lambda-calculus, sequent calculus, normalisation and cut-elimination, with call-by-name and call-by-value semantics. In particular, it introduces proof-term calculi for multiplicative natural deduction and for the depth-bounded sequent calculus G4. The former gives rise to the calculus Ixr with explicit substitutions, weakenings and contractions that refines the lambda-calculus and beta-reduction. Part II, entitled Type Theory in Sequent Calculus develops a theory of Pure Type Sequent Calculi, which are equivalent (w. R. T. Provability and normalisation) to Pure Type Systems but better suited for proof-search, in connection with proof-assistant tactics and proof-term enumeration algorithms. Part III, entitled Towards Classical Logic, presents some approaches to classical type theory. It develops a sequent calculus for a classical version of System Fomega. Basing the notion of equivalence of classical proofs on parallel rewriting in the Calculus of Structures, we then compute canonical representatives of equivalent proofs

APA, Harvard, Vancouver, ISO, and other styles

33

Rouillard, Davy. "Application de techniques de preuve assistée pour la spécification, la vérification et le test." Bordeaux 1, 2002. http://www.theses.fr/2002BOR12573.

Full text

Abstract:

Les méthodes formelles ont pour objectif d'augmenter le niveau de confiance que l'on peut avoir en un système informatique, en proposant des techniques d'analyse dont les fondements sont mathématiques. Traditionnellement, ces méthodes sont classées en trois grandes familles : le model-checking, la preuve interactive et le test. Ce mémoire décrit le développement d'un environnement formel qui autorise à la fois une activité de vérification et dont l'objectif est permettre l'étude de systèmes complexes modélisés sous la forme d'automates. Cet environnement prend la forme d'un ensemble de théories Isabelle/HOL dont la racine est formée par la formalisation des systèmes de transitions et leur comportements. Plusieurs mécanismes de preuve sont présentés et il est mit en évidence l'importance du mécanisme de réécritures. Nous nous intéressons également à une nouvelle approche du test qui consiste à envisager la création d'un test comme la démonstration d'un énoncé.

APA, Harvard, Vancouver, ISO, and other styles

34

Spadotti, Régis. "Une théorie mécanisée des arbres réguliers en théorie des types dépendants." Thesis, Toulouse 3, 2016. http://www.theses.fr/2016TOU30178/document.

Full text

Abstract:

Nous proposons deux caractérisations des arbres réguliers. La première est sémantique et s'appuie sur les types co-inductifs. La seconde est syntaxique et repose sur une représentation des arbres réguliers par des termes cycliques. Nous prouvons que ces deux caractérisations sont isomorphes.Ensuite, nous étudions le problème de la définition de morphisme d'arbres préservant la propriété de régularité. Nous montrons en utilisant le formalisme des transducteurs d'arbres, l'existence d'un critère syntaxique garantissant la préservation de cette propriété. Enfin, nous considérons des applications de la théorie des arbres réguliers comme la définition de l'opérateur de composition parallèle d'une algèbre de processus ou encore, les problèmes de décidabilité sur les arbres réguliers via une mécanisation d'un vérificateur de modèles pour un mu-calcul coalgébrique. Tous les résultats ont été mécanisés et prouvés corrects dans l'assistant de preuve Coq
We propose two characterizations of regular trees. The first one is semantic and is based on coinductive types. The second one is syntactic and represents regular trees by means of cyclic terms. We prove that both of these characterizations are isomorphic. Then, we study the problem of defining tree morphisms preserving the regularity property. We show, by using the formalism of tree transducers, the existence of syntactic criterion ensuring that this property is preserved. Finally, we consider applications of the theory of regular trees such as the definition of the parallel composition operator of a process algebra or, the decidability problems on regular trees through a mechanization of a model-checker for a coalgebraic mu-calculus. All the results were mechanized and proved correct in the Coq proof assistant

APA, Harvard, Vancouver, ISO, and other styles

35

Filou, Vincent. "Une étude formelle de la théorie des calculs locaux à l'aide de l'assistant de preuve Coq." Thesis, Bordeaux 1, 2012. http://www.theses.fr/2012BOR14708/document.

Full text

Abstract:

L'objectif de cette thèse est de produire un environnement permettant de raisonner formellement sur la correction de systèmes de calculs locaux, ainsi que sur l'expressivité de ce modèle de calcul. Pour ce faire, nous utilisons l'assistant de preuve Coq. Notre première contribution est la formalisation en Coq de la sémantique des systèmes de réétiquetage localement engendrés, ou calculs locaux. Un système de calculs locaux est un système de réétiquetage de graphe dont la portée est limitée. Nous proposons donc tout d'abord une implantation succincte de la théorie des graphes en Coq, et utilisons cette dernière pour définir les systèmes de réétiquetage de graphes localement engendrés. Nous avons relevé, dans la définition usuelle des calculs locaux, certaines ambiguïtés. Nous proposons donc une nouvelle définition, et montrons formellement que celle-ci capture toutes les sous-classes d'algorithmes étudiées. Nous esquissons enfin une méthodologie de preuve des systèmes de calculs locaux en Coq.Notre seconde contribution consiste en l'étude formelle de l'expressivité des systèmes de calculs locaux. Nous formalisons un résultat de D. Angluin (repris par la suite par Y. Métivier et J. Chalopin): l'inexistence d'un algorithme d'élection universelle. Nous proposons ensuite deux lemmes originaux concernant les calculs locaux sur les arêtes (ou systèmes LC0), et utilisons ceux-ci pour produire des preuves formelles d'impossibilité pour plusieurs problèmes: calcul du degré de chaque sommet, calcul d'arbre recouvrant, etélection. Nous proposons informellement une nouvelles classes de graphe pour laquelle l'élection est irréalisable par des calculs locaux sur les arêtes.Nous étudions ensuite les transformations de systèmes de calculs locaux et de leur preuves. Nous adaptons le concept de Forward Simulation de N. Lynch aux systèmes de calculs locaux et utilisons ce dernier pour démontrer formellement l'inclusion de deux modes de détection de terminaison dans le cas des systèmes LC0. La preuve de cette inclusion estsimplifiée par l'utilisation de transformations "standards" de systèmes, pour lesquels des résultats génériques ont été démontrés. Finalement, nous réutilisons ces transformations standards pour étudier, en collaboration avec M. Tounsi, deux techniques de composition des systèmes de réétiquetage LC0. Une bibliothèque Coq d'environ 50000 lignes, contenant les preuves formelles des théorèmes présentés dans le mémoire de thèse à été produite en collaboration avec Pierre Castéran (dont environ 40%produit en propre par V. Filou) au cours de cette thèse
The goal of this work is to build a framework allowing the study, in aformal setting, of the correctness of local computations systems aswell as the expressivity of this model. A local computation system isa set of graph relabelling rules with limited scope, corresponding to a class of distributed algorithms.Our first contribution is the formalisation, in the Coq proofassistant, of a relationnal semantic for local computation systems.This work is based on an original formal graph theory for Coq.Ambiguities inherent to a "pen and paper" definition of local computations are corrected, and we prove that our definition captures all sub-classes of relabelling relations studied in the remainder. We propose a draft of a proof methodology for local computation systems in Coq. Our second contribution is the study of the expressivity of classes of local computations inside our framework. We provide,for instance, a formal proof of D. Angluin results on election and graph coverings. We propose original "meta-theorems" concerningthe LC0 class of local computation, and use these theorem to produce formal impossibility proofs.Finally we study possible transformations of local computation systemsand of their proofs. To this end, we adapt the notion of ForwardSimulation, originally formulated by N. Lynch, to localcomputations. We use this notion to define certified transformationsof LC0 systems. We show how those certified transformation can be useto study the expressivity of certain class of algorithm in ourframework. We define, as certified transformation, two notions ofcomposition for LC0 systems.A Coq library of ~ 50000 lines of code, containing the formal proofs of the theorems presented in the thesis has been produced in collaboration with Pierre Castéran

APA, Harvard, Vancouver, ISO, and other styles

36

Ruyer, Frédéric. "Preuves, types et sous-types." Phd thesis, Chambéry, 2006. http://tel.archives-ouvertes.fr/tel-00414653.

Full text

Abstract:

Cette thèse porte sur l'étude théorique et pratique d'un système de typage appliqué à la preuve de programmes de style fonctionnels. Le système de base est le système ST créé par C.Raffalli; il comporte, outre le polymorphisme, du sous-typage et de l'omission de contenu non-algorithmique. Nous étudions tout d'abord les modèles de la théorie définie par le système de types, en construisant une axiomatique basée sur les treillis permettant de modéliser le calcul et la logique. Nous étudions sur cette base le système de types, montrons la réduction du sujet, et la possibilité de définir en interne la normalisabilité et la réductibilité des programmes. Dans la suite de la thèse, plus appliquée, nous étudions des codages de types de données riches inspirés des langages fonctionnels - y incluant notamment un système de modules du premier ordre- dans le Lambda-Calcul, et montrons qu'ils s'intègrent harmonieusement dans le système; la méthodologie développée dans cette partie permet d'étendre le langage de types et le langage de programmation en conservant un critère de consistance assurant la sûreté du code typé.

APA, Harvard, Vancouver, ISO, and other styles

37

Nguyen, Quang Huy. "Calcul de réécriture et automatisation du raisonnement dans les assistants de preuve." Nancy 1, 2002. http://www.theses.fr/2002NAN10144.

Full text

Abstract:

Nous étudions dans cette thèse une coopération entre la réécriture du premier ordre et la théorie constructive des types pour automatiser les preuves assistées par l'ordinateur. Nous cherchons par ce travail à mettre en oeuvre la réécriture de manière automatique, sûre et efficace dans l'assistant de preuve Coq à l'aide d'un environnement de programmation externe (ELAN). Deux approches différentes sont étudiées. Dans l'approche mixte, ELAN est utilisé comme un moteur de réécriture externe pour la normalisation des termes dans une tactique réflexive de réécriture en Coq. La trace générée par ELAN de la normalisation est rejouée en Coq pour calculer la forme normale. Afin d'améliorer la performance de la tactique réflexive, nous montrons comment utiliser la réécriture paresseuse pour obtenir une meilleure trace de normalisation. La deuxième approche, appelée externe, est plus flexible car d'une part, elle permet d'obtenir également plusieurs extensions utiles de la réécriture telles que la réécriture conditionnelle ou bien la réécriture modulo l'associativité et la commutativité (AC), et d'autre part, elle peut être facilement adaptée pour d'autres assistants de preuve. Dans cette approche, la réécriture est effectuée entièrement en ELAN et les assistants de preuve ne servent qu'à la vérifier. Nous formalisons donc la notion de terme de preuve des calculs ELAN dans le calcul de réécriture avec substitutions explicites. Nous étudions les propriétés des termes de preuve et les traduisons en syntaxe de l'assistant de preuve pour vérifier les calculs correspondants. Par conséquent, les calculs non-déterministes en ELAN peuvent être certifiés indépendamment, et nous disposons de la réécriture dans l'assistant de preuve. Afin d'améliorer la performance de la vérification des calculs concernant la réécriture modulo AC, nous proposons également une méthode de preuve efficace pour les égalités modulo AC en se basant sur la syntaxicité des théories AC. Ces résultats ont été intégrés dans une nouvelle tactique de réécriture ELAN en Coq
In this thesis, we are interested in the cooperation of first-order rewriting and constructive type theory to improve the automation of computer-aided proofs. We aim to integrate (simple, conditional or AC) rewriting in the Coq proof assistant by an automatic, safe and efficient means using an external programming environment ELAN. Two different approaches are investigated. In the mixed approach, ELAN is used as an external rewriting engine for normalising terms in a reflexive rewriting tactic in Coq. The normalisation trace generated by ELAN is replayed in Coq to compute the corresponding normal form. In order to improve the performance of this reflexive tactic, we show how to use lazy rewriting for producing compact normalisation traces. The second approach called external is more flexible since it also covers several useful extensions of term rewriting such as conditional rewriting and AC rewriting, and it can be easily adapted to other proof assistants. In this approach, term rewriting is entirely performed in ELAN and proof assistants are only used for checking purpose. We formalise the notion of proof term for ELAN computations in the rewriting calculus with explicit substitutions. We investigate the equivalent properties of the proof terms and translate them into the syntax of proof assistant in order to check the corresponding computations. By this work, non-deterministic ELAN computations can be independently certified and we obtain term rewriting in proof assistant. In order to speed up proof-checking of the computations involving AC rewriting, we also propose an efficient method for proving equalities modulo AC based on the syntacticness of AC theories. These results have been integrated in a new ELAN-based rewriting tactic in Coq

APA, Harvard, Vancouver, ISO, and other styles

38

Ben, Rajeb Narjes. "Preuves par induction implicite : cas des théories associatives-commutatives et observationnelles." Nancy 1, 1997. http://www.theses.fr/1997NAN10174.

Full text

Abstract:

Les preuves automatiques par induction sont un moyen formel pour la validation de systèmes informatiques. Dans le cadre de l'induction par ensemble test, nous proposons deux méthodes de preuves automatiques s'appliquant à des spécifications conditionnelles : l'une opérant dans les théories associatives-commutatives (AC), l'autre dans les théories observationnelles. Dans la première méthode nous proposons un calcul des schémas d'induction, ainsi qu'un système d'inférence utilisant des techniques élaborées de réécriture modulo AC. Pour une classe de spécifications, la méthode détecte toute conjecture non valide en un temps fini. Des expérimentations intéressantes sur la correction de circuits digitaux, ont produit des preuves nécessitant moins d'interaction qu'avec d'autres prouveurs connus. Dans l'approche observationnelle, les objets d'un type de données sont considérés comme égaux s'ils ne peuvent être distingués par des expérimentations à résultats observables. Ces expérimentations sont représentées par des termes particuliers appelés contextes observables. Nous proposons une méthode de preuve automatique de propriétés observationnelles reposant sur le calcul d'un ensemble fini de contextes, appelés contextes tests, qui schématise l'ensemble de tous les contextes observables. Nous proposons également des méthodes de calcul de ces contextes tests ainsi qu'un nouveau système d'inférence. Pour une classe de spécifications, la méthode détecte toute conjecture non observationnellement valide en un temps fini
Automated induction proofs are a formal means for systems validation. In the framework of test set induction, we propose two automated proofs methods for conditional specifications: one deals with associative-commutative (AC) theories, the other with observational theories. In the first method, we give an algorithm for computing induction schemes, as well as a new inference system using elaborated AC rewriting techniques. For a class of specifications, the method detects non valid conjectures in a finite time. Interesting experiments on the correctness of digital circuits produced proofs requiring less interaction than other well-known provers. In the observational approach, data type objects are cnsidered as equal if they cannot be distinguished by experiments with observational results. These experiments are represented by particular terms called observable contexts. We propose an automated proof method of observational properties, relying on the computation of a finite set of well-chosen contexts called test contexts, that shematizes all the observable contexts. We also propose methods for computing such test contexts and a new inference system. For an interesting class of specifications, the method detects non observationally valid conjectures in a finite time

APA, Harvard, Vancouver, ISO, and other styles

39

De, Rancourt Noé. "Théorie de Ramsey sans principe des tiroirs et applications à la preuve de dichotomies d'espaces de Banach." Thesis, Sorbonne Paris Cité, 2018. http://www.theses.fr/2018USPCC208/document.

Full text

Abstract:

Dans les années 90, Gowers démontre un théorème de type Ramsey pour les bloc-suites dans les espaces de Banach, afin de prouver deux dichotomies d'espaces de Banach. Ce théorème, contrairement à la plupart des résultats de type Ramsey en dimension infinie, ne repose pas sur un principe des tiroirs, et en conséquence, sa formulation doit faire appel à des jeux. Dans une première partie de cette thèse, nous développons un formalisme abstrait pour la théorie de Ramsey en dimension infinie avec et sans principe des tiroirs, et nous démontrons dans celui-ci une version abstraite du théorème de Gowers, duquel on peut déduire à la fois le théorème de Mathias-Silver et celui de Gowers. On en donne à la fois une version exacte dans les espaces dénombrables, et une version approximative dans les espaces métriques séparables. On démontre également le principe de Ramsey adverse, un résultat généralisant à la fois le théorème de Gowers abstrait et la détermination borélienne des jeux dénombrables. On étudie aussi les limitations de ces résultats et leurs généralisations possibles sous des hypothèses supplémentaires de théorie des ensembles.Dans une seconde partie, nous appliquons les résultats précédents à la preuve de deux dichotomies d'espaces de Banach. Ces dichotomies ont une forme similaire à celles de Gowers, mais sont Hilbert-évitantes : elles assurent que le sous-espace obtenu n'est pas isomorphe à un espace de Hilbert. Ces dichotomies sont une nouvelle étape vers la résolution d'une question de Ferenczi et Rosendal, demandant si un espace de Banach séparable non-isomorphe à un espace de Hilbert possède nécessairement un grand nombre de sous-espaces, à isomorphisme près
In the 90's, Gowers proves a Ramsey-type theorem for block-sequences in Banach spaces, in order to show two Banach-space dichotomies. Unlike most infinite-dimensional Ramsey-type results, this theorem does not rely on a pigeonhole principle, and therefore it has to have a partially game-theoretical formulation. In a first part of this thesis, we develop an abstract formalism for Ramsey theory with and without pigeonhole principle, and we prove in it an abstract version of Gowers' theorem, from which both Mathias-Silver's theorem and Gowers' theorem can be deduced. We give both an exact version of this theorem in countable spaces, and an approximate version of it in separable metric spaces. We also prove the adversarial Ramsey principle, a result generalising both the abstract Gowers' theorem and Borel determinacy of countable games. We also study the limitations of these results and their possible generalisations under additional set-theoretical hypotheses. In a second part, we apply the latter results to the proof of two Banach-space dichotomies. These dichotomies are similar to Gowers' ones, but are Hilbert-avoiding, that is, they ensure that the subspace they give is not isomorphic to a Hilbert space. These dichotomies are a new step towards the solution of a question asked by Ferenczi and Rosendal, asking whether a separable Banach space non-isomorphic to a Hilbert space necessarily contains a large number of subspaces, up to isomorphism

APA, Harvard, Vancouver, ISO, and other styles

40

Lengrand, Stéphane. "Normalisation & Equivalence en Théorie de la Démonstration & Théorie des Types." Phd thesis, Université Paris-Diderot - Paris VII, 2006. http://tel.archives-ouvertes.fr/tel-00134646.

Full text

Abstract:

Au coeur des liens entre Théorie de la Démonstration et Théorie des Types, la correspondance de Curry-Howard fournit des termes de preuves aux aspects calculatoires et équipés de théories équationnelles, i.e. des notions de normalisation et d'équivalence. Cette thèse contribue à étendre son cadre à des formalismes (comme le calcul des séquents) appropriés à des considérations d'ordre logique comme la recherche de preuve, à des systèmes expressifs dépassant la logique propositionnelle comme des théories des types, et aux raisonnements classiques plutôt qu'intuitionistes.
La première partie est intitulée Termes de Preuve pour la Logique Intuitioniste Implicationnelle, avec des contributions en déduction naturelle et calcul des séquents, normalisation et élimination des coupures, sémantiques en appel par nom et par valeur. En particulier elle introduit des calculs de termes de preuve pour le calcul des séquents depth-bounded G4 et la déduction naturelle multiplicative. Cette dernière donne lieu à un calcul de substitutions explicites avec affaiblissements et contractions, qui raffine la beta-réduction.
La deuxième partie, intitulée Théorie des Types en Calcul des Séquents, développe une théorie des Pure Type Sequent Calculi, équivalents aux Systèmes de Types Purs mais mieux adaptés à la recherche de preuve.
La troisième partie, intitulée Vers la Logique Classique, étudie des approches à la Théorie des Types classique. Elle développe un calcul des séquents pour une version classique du Système Fomega. Une approche à la question de l'équivalence de preuves classiques consiste à calculer les représentants canoniques de preuves équivalentes dans le cadre du Calcul des Structures.

APA, Harvard, Vancouver, ISO, and other styles

41

Mayero, Micaela. "Formalisation et automatisation de preuves en analyses réelle et numérique." Paris 6, 2001. http://www.theses.fr/2001PA066460.

Full text

APA, Harvard, Vancouver, ISO, and other styles

42

Coscoy, Yann. "Explication textuelle de preuves pour le calcul des constructions inductives." Nice, 2000. http://www.theses.fr/2000NICE5428.

Full text

Abstract:

Ce travail concerne la présentation des preuves formalisées dans le calcul des constructions inductives. Le calcul des constructions est un [lambda]-calcul typé introduit par Th. Coquand et G. Huet. Il permet un codage fonctionnel des preuves d'ordre supérieur par l'isomorphisme de Curry-Howard. Nous étudions dans ce manuscrit une variante de ce formalisme étendue par Ch. Paulin et B. Werner. Nous décrivons une fonction réversible traduisant les termes de preuve du formalisme en des textes mathématiques en français. Dans le premier sens, du [lambda]-terme vers la langue naturelle, cette traduction est une présentation de la preuve. Elle comporte une phase de sélection des informations avec organisation du discours puis une phase de verbalisation. Dans l'autre sens, du texte vers le [lambda]-terme, il s'agit d'une validation. Le texte est analysé syntaxiquement puis évalué comme un script de système de preuve. La réversibilité de la fonction de présentation permet de garantir formellement que les démonstrations produites en français sont des preuves formelles. Elles peuvent de fait être validées par un processus automatique

APA, Harvard, Vancouver, ISO, and other styles

43

Garchery, Quentin. "Certification de la transformation de tâches de preuve." Electronic Thesis or Diss., université Paris-Saclay, 2022. http://www.theses.fr/2022UPASG006.

Full text

Abstract:

De nombreux prouveurs et outils de vérification font un usage instensif des transformations logiques afin de ramener un problème exprimé sous la forme d'une tâche de preuve à un certain nombre de tâches de preuve plus simples à valider. Les transformations font souvent partie de la base de confiance de l'outil de vérification. Cette thèse a pour objectif de renforcer la confiance accordée aux transformations logiques. Les transformations sont instrumentées pour produire des certificats puis ceux-ci sont vérifiés par un outil externe: c'est l'approche sceptique. De ce fait, notre méthode est incrémentale et robuste aux modifications apportées au code des transformations. Nous définissons deux formats de certificats; les transformations génèrent des certificats de surface et ces certificats sont traduits en des certificats de noyau qui sont destinés à la vérification finale. L'accent est mis sur la facilité de production des certificats de surface et nous avons fait en sorte qu'ils soient, autant que possible, indépendants des tâches de preuve, facilitant ainsi leur composition et rendant la certification plus modulaire. Les certificats de noyau, au contraire, incluent de nombreux détails tout en restant élémentaires, de sorte que leur vérification est réalisable par un outil simple, dont la confiance est facile à établir. Nous proposons une procédure de traduction d'un certificat de surface en un certificat de noyau qui n'a pas besoin d'être certifiée. Les transformations logiques sont considérées dans une logique d'ordre supérieur avec polymorphisme de type, ce formalisme pouvant être étendu avec des théories interprétées telles que l'égalité ou l'arithmétique entière. Nous appliquons notre méthode à Why3, et notamment à des transformations complexes qui pré-existent à notre travail. Nous implémentons également deux vérificateurs de certificats, le premier reposant sur une approche calculatoire efficace et l'autre s'appuyant sur un encodage superficiel des tâches de preuve dans le framework logique Lambdapi, donnant ainsi de fortes garanties de sa correction
In various provers and deductive verification tools, logical transformations are used extensively in order to reduce a proof task into a number of simpler tasks. Logical transformations are often part of the trusted base of such tools. In this thesis, we develop a framework to improve confidence in their results. We follow a skeptical} approach: transformations are instrumented to produce certificates that are checked by a third-party tool. Thus, we benefit from a modular approach that is also robust to changes in the source code of the transformations. We design two kinds of certificates. Transformations produce surface certificates} that are then translated to kernel certificates} which are destined for final verification. We made sure that surface certificates are easy to produce. Moreover, surface certificates are as independent of the transformation application as possible and this makes for a modular certification. On the contrary, kernel certificates include numerous details about the transformation application and are kept elementary. This helps to define simpler checkers and establish their correctness. We propose a translation procedure from surface certificates to kernel certificates which does not need to be trusted. Logical transformations are considered in a higher-order logic, with type polymorphism and built-in theories such as equality and integer arithmetic. We apply our framework to Why3 and use it to instrument pre-existing and complex transformations. Additionally, we implement two certificate checkers. The first one follows an efficient computational approach while the second is based on a shallow embedding of proof tasks inside the logical framework Lambdapi, thus exhibiting formal guaranties of its correctness

APA, Harvard, Vancouver, ISO, and other styles

44

Genet, Thomas. "Contraintes d'ordre et automates d'arbres pour les preuves de terminaison." Nancy 1, 1998. http://docnum.univ-lorraine.fr/public/SCD_T_1998_0245_GENET.pdf.

Full text

Abstract:

Les systèmes de réécriture sont des systèmes de calcul simples et lisibles dont l'expressivité est suffisante pour le codage des programmes ou la spécification de processus automatiques. En exprimant les programmes ou processus sous la forme de systèmes de réécriture, on dispose, en outre, d'outils de vérification puissants basés sur les méthodes de preuve de la réécriture. La terminaison assure l'achèvement des calculs en un temps fini et elle est une prémisse indispensable à d'autres méthodes de preuve telle la preuve par récurrence. Classiquement, la preuve de terminaison d'un système de réécriture utilise la recherche d'un ordre bien fondé assurant la décroissance de chaque étape de réécriture. La recherche manuelle d'un tel ordre n'est envisageable que sur des petits systèmes. C'est pourquoi l'automatisation des preuves de terminaison est un élément crucial pour l'exploitation des outils de preuve de la réécriture sur des programmes ou des processus de taille réelle. Dans cette thèse nous présentons deux approches pour l'automatisation des preuves de terminaison des systèmes de réécriture. Dans la première approche, la recherche de l'ordre de terminaison - une instance de l'ordre général sur les chemins (GPO) - est effectuée a l'aide d'un mécanisme de résolution de contraintes d'ordre (sur des graphes orientés) tendant à rendre la recherche efficace et automatique. La deuxième approche est modulaire ; le système est divisé en sous-systèmes et les preuves de terminaison sont réalisées indépendamment pour chaque sous-système. La terminaison du système complet est assurée, pour une certaine stratégie d'application des sous-systèmes, par un critère basé sur le calcul d'une approximation de l'ensemble des formes normales en utilisant des techniques d'automates d'arbres. D'autres applications de cette approximation sont également présentées, parmi lesquelles la complétude suffisante, le test d'atteignabilité, et la preuve de non-terminaison forte.

APA, Harvard, Vancouver, ISO, and other styles

45

Lepigre, Rodolphe. "Sémantique et implantation d'une extension de ML pour la preuve de programmes." Thesis, Université Grenoble Alpes (ComUE), 2017. http://www.theses.fr/2017GREAM034/document.

Full text

Abstract:

Au cours des dernières années, les assistants de preuves on fait des progrès considérables et ont atteint un grand niveau de maturité. Ils ont permit la certification de programmes complexes tels que des compilateurs et même des systèmes d'exploitation. Néanmoins, l'utilisation d'un assistant de preuve requiert des compétences techniques très particulières, qui sont très éloignées de celles requises pour programmer de manière usuelle. Pour combler cet écart, nous entendons concevoir un langage de programmation de style ML supportant la preuve de programmes. Il combine au sein d'un même outil la flexibilité de ML et le fin niveau de spécification offert par un assistant de preuve. Autrement dit, le système peut être utilisé pour programmer de manière fonctionnelle et fortement typée tout en autorisant l'obtention de nouvelles garanties au besoin.On étudie donc un langage en appel par valeurs dont le système de type étend une logique d'ordre supérieur. Il comprend un type égalité entre les programmes non typés, un type de fonction dépendant, la logique classique et du sous-typage. La combinaison de l'appel par valeurs,des fonctions dépendantes et de la logique classique est connu pour poser des problèmes de cohérence. Pour s'assurer de la correction du système (cohérence logique et sûreté à l'exécution), on propose un cadre théorique basé sur la réalisabilité classique de Krivine. La construction du modèle repose sur une propriété essentielle qui lie les différent niveaux d'interprétation des types d'une manière novatrice.On démontre aussi l'expressivité de notre système en se basant sur son implantation dans un prototype. Il peut être utilisé pour prouver des propriétés de programmes standards tels que la fonction « map »sur les listes ou le tri par insertion
In recent years, proof assistant have reached an impressive level of maturity. They have led to the certification of complex programs such as compilers and operating systems. Yet, using a proof assistant requires highly specialised skills and it remains very different from standard programming. To bridge this gap, we aim at designing an ML-style programming language with support for proofs of programs, combining in a single tool the flexibility of ML and the fine specification features of a proof assistant. In other words, the system should be suitable both for programming (in the strongly-typed, functional sense) and for gradually increasing the level of guarantees met by programs, on a by-need basis.We thus define and study a call-by-value language whose type system extends higher-order logic with an equality type over untyped programs, a dependent function type, classical logic and subtyping. The combination of call-by-value evaluation, dependent functions and classical logic is known to raise consistency issues. To ensure the correctness of the system (logical consistency and runtime safety), we design a theoretical framework based on Krivine's classical realisability. The construction of the model relies on an essential property linking the different levels of interpretation of types in a novel way.We finally demonstrate the expressive power of our system using our prototype implementation, by proving properties of standard programs like the map function on lists or the insertion sort

APA, Harvard, Vancouver, ISO, and other styles

46

Saleh, Mohamed Saad Sayed. "Essai d'une théorie générale de la preuve devant la juridiction internationale : étude sur la juridiction de la Cour internationale de justice." Paris 2, 1999. http://www.theses.fr/1999PA020087.

Full text

Abstract:

Cette etude propose un essai d'une theorie generale des problematiques de la preuve devant la juridiction internationale. Cette theorie sera degagee des pratiques juridiques internationales, notamment, les pratiques de la cour internationale de justice, qui sont, a notre avis, la base de cette theorie. Elle vise a faire evoluer ces pratiques et combler les lacunes en relation avec la nature de lajuridiction internationale. Les problemes qui surgissent a propos de la presentation et de l'evaluation de la preuve devant la juridiction internationale sont nombreux et complexes. Le droit international de la procedure manque de perennite et les regles qui le gouvernent sont tres sommaires et difficiles a interpreter. Le probleme apparait d'une maniere plus evidente lorsque des tribunaux internationaux se trouvent face a une difficulte supplementaire causee par la confrontation des regles de preuve retenues par les differents systemes juridiques. En effet, les techniques et les regles de preuve varient non seulement selon les systemes juridiques, mais aussi selon les finalites propres a chaque branche du droit. Les regles adoptees par le droit continental sont differentes de celles retenues par le droit anglo-americain. Cette difference pose de serieux problemes a la juridiction internationale, l'une des parties ne pourra ni evaluer les preuves presentees par l'autre, ni apprecier leur contenu. Les parties tentent de faire prevaloir leurs propres regles nationales en matiere de preuve et de les transposer devant la juridiction internationale. C'est ainsi qu'apparaissent des difficultes causees par les differences dans les diverses techniques retenues par les droits internes. Les juges emanant des differents systemes juridiques seront a leur tour confrontes aux memes difficultes ; cela apparaitra d'une maniere plus evidente lors de l'evaluation des preuves et de leur classification. Afin de faire face a ces difficultes, nous chercherons a etablir un systeme valable pour la presentation et l'evaluation des preuves, qui tient compte de la nature propre du droit international et de la juridiction internationale. Les regles dont nous allons etudier les modalites d'application sont propres a la procedure internationale, leur originalite est indeniable. Cette theorie ne doit pas etre consideree comme la transposition pure et simple des regles applicables devant les trib

APA, Harvard, Vancouver, ISO, and other styles

47

Cartier, Léa. "Le graphe comme outil pour enseigner la preuve et la modélisation." Phd thesis, Grenoble 1, 2008. http://www.theses.fr/2008GRE10148.

Full text

Abstract:

La raison initiale du sujet de cette thèse est l'introduction, pour la première fois en France, d'éléments de théorie des graphes dans un curriculum de l'enseignement secondaire, à savoir celui de la spécialité mathématiques de la Terminale économique et sociale (ES) en 2002. Après une brève étude historique de la genèse – relativement récente – du graphe en tant que concept mathématique et de la signification épistémologique de cette genèse, nous analysons les choix faits pour la transposition de ce concept, en particulier les énoncés proposés aux élèves, qui montrent le décalage entre les intentions affichées et la réalité. Cette partie du programme de terminale ES se particularise par sa mise en œuvre « axée sur le seule résolution de problèmes ». Or, nous montrons que les manuels scolaires sont dans ce chapitre composés d'exercices et non de problèmes. L'enseignement de théorie des graphes, s'il se limite à la résolution, locale, de ces exercices ou de « casse-tête » mathématiques, ne permet pas aux élèves de comprendre les concepts mathématiques sous-jacents ni surtout d'accéder au sens du raisonnement mathématique (en particulier autour de la modélisation et de la preuve) et à la richesse de la démarche scientifique, ce qu'aurait dû permettre ce domaine facilement abordable des mathématiques. Une étude théorique et expérimentale du problème de « parcours eulériens dans les graphes » a ensuite été menée, du primaire au supérieur, sous des formes différentes (situations-recherche en classe avec ou sans support matériel, étude de documents). Des éléments didactiques ont aussi été tirés de deux stages de formation d'enseignants en théorie des graphes pour la Terminale ES. Ces différentes études nous ont conduit à proposer un nouvel ensemble organisé de problèmes à destination des enseignants de Terminale ES, accompagnés de leur résolution et d'analyses didactiques qui attestent que des mathématiques plus consistantes peuvent être abordées et construites sur ce thème
In 2002, elements of graph theory entered the curriculum of Terminale ES (12th grade) in France. We first sketch a brief history of the genesis of the notion of graph (Chapter 1). We then study the way graphs entered the French high school curriculum, its transposition and realization, in particular through the study of the exercises that are proposed in the textbooks (Chapter 2). A specificity of this part of the curriculum lies on the fact that its implementation is to be based on problem-solving activities only. We demonstrate that textbooks actually never propose real problems, but only exercises. Furthermore, we discuss the dangers and drawbacks of restricting oneself to the resolution of exercises or “mathematical puzzles” only, in the sense that local resolutions do not necessary yield to the underlying mathematical concepts. In Chapter 3 we propose experimental studies on the eulerian trail problem, with learners ranging from primary school pupils to undergraduate students, and several kinds of implementations (classroom problem-solving activities, document study). We relate in details two classes with math teachers about graph theory in Terminale ES. Finally, we present in Chapter 4 a set of problems (with solutions) covering the curriculum of Terminale ES, intending to demonstrate that solid mathematics could be addressed on that occasion

APA, Harvard, Vancouver, ISO, and other styles

48

Cartier, Léa. "Le graphe comme outil pour enseigner la preuve et la modélisation." Phd thesis, Université Joseph Fourier (Grenoble), 2008. http://tel.archives-ouvertes.fr/tel-00416598.

Full text

Abstract:

La raison initiale du sujet de cette thèse est l'introduction, pour la première fois en France, d'éléments de théorie des graphes dans un curriculum de l'enseignement secondaire, à savoir celui de la spécialité mathématiques de la Terminale économique et sociale (ES) en 2002.
Après une brève étude historique de la genèse – relativement récente – du graphe en tant que concept mathématique et de la signification épistémologique de cette genèse, nous analysons les choix faits pour la transposition de ce concept, en particulier les énoncés proposés aux élèves, qui montrent le décalage entre les intentions affichées et la réalité. Cette partie du programme de terminale ES se particularise par sa mise en œuvre « axée sur le seule résolution de problèmes ».
Or, nous montrons que les manuels scolaires sont dans ce chapitre composés d'exercices et non de problèmes. L'enseignement de théorie des graphes, s'il se limite à la résolution, locale, de ces exercices ou de « casse-tête » mathématiques, ne permet pas aux élèves de comprendre les concepts mathématiques sous-jacents ni surtout d'accéder au sens du raisonnement mathématique (en particulier autour de la modélisation et de la preuve) et à la richesse de la démarche scientifique, ce qu'aurait dû permettre ce domaine facilement abordable des mathématiques.
Une étude théorique et expérimentale du problème de « parcours eulériens dans les graphes » a ensuite été menée, du primaire au supérieur, sous des formes différentes (situations-recherche en classe avec ou sans support matériel, étude de documents). Des éléments didactiques ont aussi été tirés de deux stages de formation d'enseignants en théorie des graphes pour la Terminale ES.
Ces différentes études nous ont conduit à proposer un nouvel ensemble organisé de problèmes à destination des enseignants de Terminale ES, accompagnés de leur résolution et d'analyses didactiques qui attestent que des mathématiques plus consistantes peuvent être abordées et construites sur ce thème.

APA, Harvard, Vancouver, ISO, and other styles

49

Ilik, Danko. "Preuves constructives de complétude et contrôle délimité." Phd thesis, Ecole Polytechnique X, 2010. http://tel.archives-ouvertes.fr/tel-00529021.

Full text

Abstract:

Motivés par la facilitation du raisonnement sur des méta-théories logiques à l'intérieur de l'assistant de preuve Coq, nous étudions les versions constructives de certains théorèmes de complétude. Nous commençons par l'analyse des preuves de Krivine et Berardi-Valentini qui énoncent que la logique classique est constructivement complète au regard des modèles booléens relaxés, ainsi que l'analyse de l'algorithme de cette preuve. En essayant d'élaborer une preuve de complétude plus canonique pour la logique classique, inspirés par la méthode de la normalisation-par-évaluation (NPE) de Berger et Schwichtenberg, nous concevons une preuve de complétude pour la logique classique en introduisant une notion de modèle dans le style des modèles de Kripke, dont le contenu calculatoire est l'élimination des coupures, ou la normalisation. Nous nous tournons ensuite vers la NPE pour une logique de prédicats intuitionniste (en considérant tous les connecteurs logiques), c'est-à-dire, vers sa complétude par rapport aux modèles de Kripke. Inspirés par le programme informatique de Danvy pour la normalisation des termes du $\lambda$-calcul avec sommes, lequel utilise des opérateurs de contrôle délimité, nous développons une notion d'un modèle, encore une fois semblable aux modèles de Kripke, qui est correct et complet pour la logique de prédicats intuitionniste, et qui est, par coïncidence, très similaire à la notion de modèle de Kripke introduit pour la logique classique. Finalement, en se fondant sur des observations de Herbelin, nous montrons que l'on peut avoir une logique intuitionniste étendue avec des opérateurs de contrôle délimité qui est equiconsistante avec la logique intuitionniste, qui préserve les propriétés de disjonction et d'existence, et qui est capable de dériver le schéma « Double Negation Shift » et le principe de Markov.

APA, Harvard, Vancouver, ISO, and other styles

50

Urbain, Xavier. "Approche incrémentale des preuves automatiques de terminaison." Paris 11, 2001. https://hal.archives-ouvertes.fr/tel-02061902.

Full text

Abstract:

La preuve de terminaison d'un système de récriture est souvent d'autant plus difficile que celui-ci est gros. Une stratégie de preuve divide and conquer ne peut hélas généralement pas s'appliquer directement, rendant l'automatisation des preuves pour les systèmes importants particulièrement ardue. Pour améliorer significativement la conduite de ces preuves nous nous fixons un double objectif : 1) Automatiser les preuves de terminaison et 2) Les rendre incrémentales afin de traiter efficacement des systèmes de plusieurs milliers de règles comme on en rencontre en pratique. Nous proposons une approche modulaire des systèmes de récriture tirant parti de leur structure hiérarchique en définissant la notion de modules de récriture, puis développons à partir de ceux-ci une méthode incrémentale de preuve de terminaison. Nous obtenons ainsi des critères de terminaison nouveaux et puissants, tant dans le cas standard que dans le cas de la récriture modulo associativité et commutativité pour laquelle nous donnons une extension des paires de dépendance. Notre politique consistant à affaiblir la notion de terminaison pour alléger les contraintes sur les constituants des hiérarchies et la généralité du concept de modules permettent d'exprimer des résultats antérieurs et de subsumer des méthodes aux prémisses plus restrictives quant à la nature des unions ou sur une stratégie particulière à appliquer. Nous présentons enfin une implantation de cette approche qui autorise une recherche automatique des preuves, la simplicité des ordres idoines ajoutant l'efficacité à l'automatisation. Des preuves de terminaison peuvent être trouvées de façon totalement automatique et incrémentale : le gain de temps passé lors de la résolution des contraintes est alors spectaculaire
Proving termination of a term rewriting system is often harder when the system is large. A divide and conquer strategy cannot be applied directly, thus making automation of proofs for systems with many rules a very difficult task. In order to provide a significant improvement in proving termination, we focus on two critical points : Automating termination proofs and Computing them incrementally, so as to deal with systems of thousands of rules (common in practice) efficiently. We propose a modular approach of term rewriting systems, making the best of their hierarchical structure. We define rewriting modules and then provide a new method allowing to prove termination incrementally. We obtain new and powerful termination criteria for standard rewriting but also for rewriting modulo associativity and commutativity. Our policy of restraining termination itself (thus relaxing constraints over hierarchies components) together with the generality of the module approach are sufficient to express previous results and methods the premisses of which either include restrictions over unions or make a particular reduction strategy compulsory. We describe our implementation of the modular approach. Proofs are fully automated and performed incrementally. Since convenient orderings are simpler, we observe a dramatic speed up in the finding of the proof

APA, Harvard, Vancouver, ISO, and other styles

Dissertations / Theses on the topic 'Preuve de théorème'

Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles