Academic literature on the topic 'Preuve de théorème'
Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles
Consult the lists of relevant articles, books, theses, conference reports, and other scholarly sources on the topic 'Preuve de théorème.'
Next to every source in the list of references, there is an 'Add to bibliography' button. Press on it, and we will generate automatically the bibliographic reference to the chosen work in the citation style you need: APA, MLA, Harvard, Chicago, Vancouver, etc.
You can also download the full text of the academic publication as pdf and read online its abstract whenever available in the metadata.
Journal articles on the topic "Preuve de théorème"
1
Krivine, Jean-Louis. "Une Preuve Formelle et Intuitionniste du Théorème de Complétude de la Logique Classique." Bulletin of Symbolic Logic 2, no. 4 (December 1996): 405–21. http://dx.doi.org/10.2307/421172.
Full textAbstract:
Introduction. Il est bien connu que la correspondance de Curry-Howard permet d'associer un programme, sous la forme d'un λ-terme, à toute preuve intuitionniste, formalisée dans le calcul des prédicats du second ordre (voir, par exemple [3]). Cette correspondance a été étendue, assez récemment, à la logique classique moyennant une extension convenable du λ-calcul (voir [1, 4, 5, 6]). Chaque théorème formalisé en logique du second ordre correspond donc à une spécification de programme.Il se pose alors le problème, en général tout à fait non trivial, de trouver la spécification associée à un théorème donné; autrement dit, de déterminer le comportement opérationnel commun aux λ-termes associés aux diverses démonstrations formelles du théorème considéré.Cette question est résolue ici pour le théorème de complétude de la logique classique.La première étape consiste à formaliser convenablement ce théorème en logique du second ordre. Ce travail est fait complètement dans la section 1. Il a comme sous-produit, peut-être inattendu, de montrer que ce théorème est prouvable en logique intuitionniste du second ordre (section 2). Ceci, toutefois, à condition d'introduire une légère variante de la notion de modèle, en admettant un modèle supplémentaire trivial, où toute formule est satisfaite.On notera, à ce sujet, que des preuves intuitionnistes du théorème de complétude de la logique intuitionniste, utilisant des variantes de la notion de modele de Kripke, ont été données par H. Friedman [7] et W. Veldman [8]. On remarquera également qu'un argument de G. Kreisel [2] montre que le théorème de complétude habituel de la logique intuitionniste n'a pas de preuve intuitionniste.
2
Chéritat, Arnaud. "Nouvelle preuve d'un théorème de Yoccoz." Comptes Rendus Mathematique 338, no. 4 (February 2004): 301–4. http://dx.doi.org/10.1016/j.crma.2003.12.020.
Full text
3
Bousch, Thierry. "Nouvelle preuve d’un théorème de Yuan et Hunt." Bulletin de la Société mathématique de France 136, no. 2 (2008): 227–42. http://dx.doi.org/10.24033/bsmf.2555.
Full text
4
LE SAEC, BERTRAND, JEAN-ERIC PIN, and PASCAL WEIL. "SEMIGROUPS WITH IDEMPOTENT STABILIZERS AND APPLICATIONS TO AUTOMATA THEORY." International Journal of Algebra and Computation 01, no. 03 (September 1991): 291–314. http://dx.doi.org/10.1142/s0218196791000195.
Full textAbstract:
Nous prouvons que tout semigroupe fini est quotient d'un semigroupe fini dans lequel les stabilisateurs droits satisfont les identités x = x2 et xy = xyx. Ce resultat a plusieurs consé-quences. Tout d'abord, nous l'utilisons, en même temps qu'un résultat de I. Simon sur les congruences de chemins, pour obtenir une preuve purement algébrique d'un théorème profond de McNaughton sur les mots infinis. Puis, nous donnons une preuve algébrique d'un théorème de Brown sur des conditions de finitude pour les semigroupes. We show that every finite semigroup is a quotient of a finite semigroup in which every right stabilizer satisfies the identities x = x2 and xy = xyx. This result has several consequences. We first use it together with a result of I. Simon on congruences on paths to obtain a purely algebraic proof of a deep theorem of McNaughton on infinite words. Next, we give an algebraic proof of a theorem of Brown on a finiteness condition for semigroups.
5
Le Calvez, Patrice. "Une nouvelle preuve du théorème de point fixe de Handel." Geometry & Topology 10, no. 4 (December 8, 2006): 2299–349. http://dx.doi.org/10.2140/gt.2006.10.2299.
Full text
6
Delorme, Patrick. "Théorème de Paley—Wiener pour les fonctions de Whittaker sur un groupe réductif p-adique." Journal of the Institute of Mathematics of Jussieu 11, no. 3 (January 6, 2012): 501–68. http://dx.doi.org/10.1017/s1474748011000193.
Full textAbstract:
RésuméSoit G un groupe réductif p-adique et U0 le radical unipotent d'un sous-groupe parabolique minimal de G. Nous introduisons une transformation de Fourier pour l'espace des fonctions de Whittaker lisses sur G et à support compact modulo U0. Nous en déterminons l'image. La preuve suit celle d'Heiermann pour les fonctions sur le groupe.Au cours de la preuve, une formule d'inversion est prouvée. Celle-ci permet de montrer qu'une représentation lisse irréductible de G, qui possède modèle de Whittaker dans les fonctions de Whittaker à support compact modulo U0, est cuspidale.Ce travail nous a donné l'opportunité de préparer un cadre pour l'analyse harmonique sur les espaces symétriques réductifs p-adiques: B-matrices et terme constant, propriétés des paquets d'ondes.
7
Cerf, J. "Homologie des simplexes plongés : une preuve nouvelle du théorème de Lalonde." Bulletin de la Société mathématique de France 118, no. 1 (1990): 1–25. http://dx.doi.org/10.24033/bsmf.2133.
Full text
8
Bardy-Panse, Nicole, Cyril Charignon, Stéphane Gaussent, and Guy Rousseau. "Une preuve plus immobilière du théorème de «saturation» de Kapovich–Leeb–Millson." L’Enseignement Mathématique 59, no. 1 (2013): 3–37. http://dx.doi.org/10.4171/lem/59-1-1.
Full text
9
Poizat, Bruno. "MM. Borel, Tits, Zil′ber et le Général Nonsense." Journal of Symbolic Logic 53, no. 1 (March 1988): 124–31. http://dx.doi.org/10.1017/s0022481200028978.
Full textAbstract:
Le rêve secret de tout logicien, c’est de prouver un résultat mathématique significatif avec des moyens de fortune; ce rêve se réalise parfois de manière quelque peu biaisée, le théorème obtenu n’étant qu’une version trop simplifiée, ou bien trop adaptée aux besoins de la logique, pour convaincre un mathématicien normal. C’est pour cela que j’annonce d’emblée la couleur, et que je précise les règles du jeu: la version du théorème de Borel-Tits que je vais montrer, concernant les groupes algébriques simples sur un corps de base algébriquement clos, sera considérée comme pratiquement évidente par un géomètre; mais c’est, à mon avis, la seule qui ait un intérêt pour un théoricien des modèles.Quand on entreprend ainsi de redémontrer une version simple d’un résultat par ailleurs bien connu, le seul intérêt est dans la méthode: ce que je veux, ici, c’est présenter une preuve qui n’utilise aucune information, ou presque, sur la structure algébrique de ces groupes; il est même souhaitable d’oublier qu’il s’agit de groupes linéaires! Elle repose sur des résultats généraux concernant les groupes de rang de Morley fini, dus à divers auteurs, dont le principal, Boris Iosifovič Zil′ber, a déjà fait une tentative similaire [Zil′ber 1984]; je poursuis ici cette tentative, mais en me limitant à des arguments encore moins spécifiques au contexte de la géométrie.Si je fais ainsi, ce n’est pas pour donner l’impression que l’unique ambition de la théorie des modèles est de montrer des résultats triviaux par des méthodes triviales.
10
Ara, Dimitri, and Georges Maltsiniotis. "Un théorème A de Quillen pour les ∞-catégories strictes I : la preuve simpliciale." Advances in Mathematics 328 (April 2018): 446–500. http://dx.doi.org/10.1016/j.aim.2018.01.018.
Full textDissertations / Theses on the topic "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 textAbstract:
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
2
Larchey-Wendling, Dominique. "Preuves, réfutations et contre-modèles dans des logiques intuitionnistes." Nancy 1, 2000. http://www.theses.fr/2000NAN10158.
Full textAbstract:
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'alorsLogics 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
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 textAbstract:
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
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 textAbstract:
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
5
Curien, Régis. "Outils pour la preuve." Nancy 1, 1995. http://docnum.univ-lorraine.fr/public/SCD_T_1995_0007_CURIEN.pdf.
Full textAbstract:
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.
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 textAbstract:
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 dronesBuilding 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
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 textAbstract:
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éécritureMethods 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
8
Selhab, Sohame. "Logiques et réécriture." Nancy 1, 1998. http://www.theses.fr/1998NAN10207.
Full textAbstract:
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.
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 textAbstract:
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.
10
Chouraqui, Jérôme. "Théorie juridique de la preuve électronique." Paris 12, 2002. http://www.theses.fr/2002PA122004.
Full textAbstract:
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.
Books on the topic "Preuve de théorème"
2
Meinel, Christoph. Mathematische Grundlagen der Informatik: Mathematisches Denken und Beweisen: eine Einführung. 4th ed. Wiesbaden: Teubner, 2009.
Find full text
3
1948-, Detlefsen Michael, ed. Proof, logic, and formalization. London: Routledge, 1992.
Find full text
4
Theoremus: A student's guide to math proofs. Victoria]: [Sleekersoft Pty Ltd.], 2015.
Find full text
5
1948-, Detlefsen Michael, ed. Proof and knowledge in mathematics. London: Routledge, 1992.
Find full text
10
Proof theory: Sequent calculi and related formalisms. Boca Raton: CRC Press, Taylor & Francis Group, 2015.
Find full textBook chapters on the topic "Preuve de théorème"
1
Bertoin, J. "Une preuve simple du théorème de Shimura Sur les points méandre du mouvement brownien plan." In Séminaire de Probabilités XXVII, 33–35. Berlin, Heidelberg: Springer Berlin Heidelberg, 1993. http://dx.doi.org/10.1007/bfb0087961.
Full text
2
KAMBAJA MUSAMPA, Emmanuel. "Stéréotypes sociaux et perturbation des niveaux de communication dans le contexte diglossique camerounais." In Plurilinguisme et tensions identitaires, 19–34. Editions des archives contemporaines, 2021. http://dx.doi.org/10.17184/eac.3776.
Full textAbstract:
Notre étude part de l’hypothèse selon laquelle les stéréotypes sociaux contenus dans le discours médiatique sur le conflit au Cameroun sont des indicateurs de la nature des relations entre les deux groupes linguistiques : anglophone et francophone. Nous nous sommes servi de la Théorie de l’École de Palo Alto et de la Théorie du conflit réel pour analyser les articles de presse en ligne portant sur le conflit inter Camerounais. A l’issue de nos analyses, il s’est avéré que fondamentalement, le conflit au Cameroun n’est pas une guerre de langues. Il est plutôt une perturbation des niveaux de communication. Les hétéro-stéréotypes et les auto-stéréotypes inscrits dans les articles de presse en ligne montrent que ce conflit est dû aux relations asymétriques compétitives qu’entretiennent les deux groupes linguistiques du Cameroun. La langue apparaît comme un élément de différence entre les deux groupes d’une part et un indicateur d’identité pour les anglophones d’autre part.
3
Favereau, Judith. "Expliquer la boîte noire : le rôle de la théorie dans l’approche du J-PAL." In Le hasard de la preuve, 145–66. ENS Éditions, 2021. http://dx.doi.org/10.4000/books.enseditions.39312.
Full text
4
Szczepankiewicz-Rudzka, Ewa. "Les mouvements de contestation du Printemps arabe à l’épreuve des théories de la révolution et démocratisation." In North Africa in the Process of Change: Political, Legal, Social and Economic Transformations, 23–38. Ksiegarnia Akademicka Publishing, 2015. http://dx.doi.org/10.12797/9788376386553.02.
Full textAbstract:
Les pays de l’Afrique du Nord et du Moyen-Orient vivent depuis 2011 une situation historique. Cette région qui nous était fréquemment présentée comme résistante aux processus de changement dit démocratique, par cette vague de contestations sociales, a fait une preuve qu’il n’existe aucune raison culturelle, politique ou sociale, pour qu’elle reste en dehors de ce mouvement d’émancipation. Ces « révolutions » baptisées « le Printemps arabe » ou « Arabe’89 » font référence aux mouvements sociales qui au cours du XIXe et XXe siècles ont touché un bon nombre des pays d’Europe. Ils incitent également à se demander si celles-ci s’inscrivent dans les cadres des théories de la révolution sociale et s’ils peuvent être examinés en s’appuyant sur les modèles jusqu’ ici existants. L’objectif de cet article sera entre autres de répondre à la question si c’était possible de prévoir les situations révolutionnaires dans les pays de MENA en s’appuyant sur les pronostics élabores par chercheures ainsi que différents instituts internationales. Deuxièmement nous chercherons les explications théorétiques des phénomènes récents dans les pays arabes. Pour cela nous nous pencherons sur les travaux de J. Goldstone, qui divise les révolutions en fonction de quatre générations. La dernière partie de ce texte tentera à examiner la théorie de la troisième vague de la démocratisation et son application dans le cas du Printemps arabe.
5
Lévy, Ghyslain. "La situation en psychanalyse." In La situation en psychanalyse, 223–33. In Press, 2012. http://dx.doi.org/10.3917/pres.barre.2012.01.0224.
Full textAbstract:
En chacun demeure la nostalgie voire la croyance en une mise en partage communautaire qui fasse communion autour d’Un seul, que celui-ci s’appelle théorie commune ou figure du Maître. Croyance et transfert se rejoignent dans la même attente d’un Autre dans lequel se rejoindrait l’unisson de nos différences. Comment peut-on penser à partir d’une telle attente qui fait souvent le fond de nos institutions, l’émergence d’une individuation singulière, condition de la construction subjective du rapport aux autres, et qui ne se résume pas à la stricte projection narcissique du semblable, du « prochain », mais qui prenne en compte la rencontre éthique de nos altérités ? N’est-ce pas cette non-conformité du sujet à lui-même qui est au travail dans la cure ? À partir de ce qui divise le sujet en lui-même, il s’agit ici d’interroger l’être commun que chaque Je a en partage avec les autres Je, sans pour autant devenir masse ou foule. Il s’agira de penser une institution qui, à partir de l’événement disruptif de Mai 68, a été conçue expérimentalement comme la possibilité d’échapper à cette nostalgie pour son rassemblement en Un-stitution : le Quatrième Groupe demeure jusqu’à aujourd’hui la seule institution analytique créée en articulation directe avec ce qui dans le social a fait événement. Il s’agirait de penser une telle singularité, et les résistances entropiques à cet événement.
Conference papers on the topic "Preuve de théorème"
1
Tardif, Marie-Pier. "La critique littéraire féminine dans la presse anarchiste : le cas des traductrices de l’Humanité nouvelle." In Théorie littéraire féminine à la Belle Époque. Fabula, 2023. http://dx.doi.org/10.58282/colloques.10975.
Full text