Standard pour la transmission de preuves et théories : Standards Informatiques & Numériques

Cette partie du forum n’est pas compatible avec les bloqueurs publicitaires

Félicitations à vous, de préférer les accès payants plutôt que la gratuité par la publicité, c’est honnorable et cohérent de votre part. Malheureusement, l’accès payant par micropaiement (qui serait d’environ 1 cent pour 20 pages consultées) n’est pour l’instant pas encore mis en place, et l’accès gratuit sans publicité, est réservé aux membres actif(ve)s du forum. En attendant, si vous souhaitez poursuivre votre visite chez nous, vous pouvez ajouter le site à votre liste blanche, ou encore mieux, désactiver le bloqueur partout. Pour ajouter le site à votre liste blanche, pour Firefox (similaire pour les autres navigateurs), rendez‑vous en bas à gauche de la fenêtre de votre navigateur, et cliquez sur le menu comme dans l’exemple de l’image ci‑dessous, puis rechargez la page, en appuyant sur F5.

Standard pour la transmission de preuves et théories

Auteur	Message

Hibou Administrateur Genre : Messages : 22281	Mar 26 Nov 2013 00:38 Standard pour la transmission de preuves et théories Si vous connaissez et/ou utilisez la conception de programmes dérivés de preuves en logique d’ordre supérieure, vous‑vous êtes peut‑être demandé pourquoi il existe plusieurs logiques d’ordre supérieur différentes (HOL4, Isabelle/HOL, HOL Zero, HOL Light, …), alors que la logique du premier ordre semble solidement standardisée (C’est FOL et c’est tout). Évidemment, si les fondations (ensemble d’axiomes fondamentaux) sont différents, à un plus haut niveau, les théorèmes dérivés tendent à faire se ressembler tous les systèmes à base de HOL, et ça ne pose pas trop de problèmes en pratique. Mais parfois il est utile de réutiliser des preuves éditées sur un système dans un autre (typiquement, des migrations de HOL4 vers Isabelle/HOL), … mais il n’existe pas de standard pour ça. Enfin, presque, et même si rien ne garantie que ce standard pendra toute la place qu’il faut pour être un standard en pratique, il existe au moins à l’état de projet, et il semble que au moins une personne importante et impliquée dans Isabelle/HOL, juge ce projet de standard crédible et pertinent, et c’est bon signe. Ce futur (ou pas futur, l’avenir le dira) standard, s’appelle OpenTheory, et il a un site. Page d’accueil : OpenTheory Project (gilith.com). FAQ du standard : Frequently Asked Questions About OpenTheory (gilith.com). Description d’une syntaxe pour l’écriture des théories : OpenTheory Article File Format (gilith.com). Il s’agit en fait de données destinées à une machine virtuelle, validant les théories. Ce n’est pas une syntaxe concrète adaptée à l’écriture de preuves structurées, ceci semblant resté du domaine des différents systèmes mentionnés plus haut entre parenthèses. bse7atkum Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon]



Hibou Administrateur Genre : Messages : 22281	Mar 26 Nov 2013 00:40 Re: Standard pour la transmission de preuves et théories Un peu H.S, mais dans le même domaine, pour les gens que ça intéresse. Le site de la quatrième conférence sur l’édition interactive de preuves informatiques, du 22 au 26 Juillet, à Renne, en france. L’organisation est apparemment gérée par l’INRIA (france aussi), mais c’est bien un événement international. ITP 2013, 4th Conference on Interactive Theorem Proving (inria.fr) Overview a écrit : ITP 2013 is the fourth conference on Interactive Theorem Proving and related issues, ranging from theoretical foundations to implementation aspects and applications in program verification, security, and formalization of mathematics. Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon]


Hibou Administrateur Genre : Messages : 22281	Dim 29 Juin 2014 23:58 Re: Standard pour la transmission de preuves et théories Une discussion technique sur le format OpenTheory, à l’occasion d’une réunion filmée, en 2011. Le locuteur est Joe Hurd, chercheur dans le domaine des preuves, et la réunion est organisée par Galois Inc, société spécialisée dans la sécurité et la fiabilité et la confidentialité () des logiciels. () Dans le sens où ils ne laissent pas fuiter d’information confidentielle. Je ne connais pas le terme approprié en français. (source de la vidéo) Pour les gens qui n’aiment pas consulter des vidéos (c’est en effet pas toujours commode), le PDF du diaporama qu’il projète sur l’écran, est disponible ici : The OpenTheory Standard Theory Library (gilith.com) [PDF]. Joe Hurd, Galois Inc Tech Talk. 2011. Moins technique, plus conceptuelle, est cet autre diaporama, du même auteur, et daté de 2009. Il est sans rapport directe avec la vidéo précédente. OpenTheory Package Management for Higher Order Logic Theories (gilith.com) [PDF]. Joe Hurd, Galois Inc Tech Seminar. 2009. Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon]


Hibou Administrateur Genre : Messages : 22281	Dim 27 Juil 2014 16:52 Re: Standard pour la transmission de preuves et théories Il existe une autre tentative d’élaboration de standard, mais qui me semble moins connu que OpenTheory, c’est une format nommé Ghilbert. Voir : Ghilbert (sites.google.com). Que ce standard n’ait pas de site dédié (il est sur un hébergeur tout‑venant, ce qui suggère que ce standard Ghilbert, bénéficie de peu d’investissement), m’inquiète quand‑même, mais c’est utile de mentionner son existence. Sa raison d’être est la même que celle d’OpenTheory : Présentation du standard Ghilbert a écrit : Ghilbert is an interchange format for formal proofs. As an interchange format, all that is needed to get started creating proofs is a verifier and a text editor. Yet, the promise of a simple, well-defined interchange format, rather than a complex highly-integrated system, is that there may eventually be an entire ecosystem consisting of various tools for automating the theorem proving process, searching and browsing proof repositories, integrations with other theorem-proving environments, and providing a rigorous basis for computer algebra systems and programming languages. Traduction a écrit : Ghilbert est un format d’échange pour les preuves formelles. Comme il est un format d’échange, il ne faut rien de plus pour débuter avec la création de preuves, qu’un validateur et un éditeur de texte. Le point de la promesse d’un format d’échange simple et bien défini, plutôt qu’un système hautement intégré et complexe, est qu’il pourrait exister un écosystème entier, constitué d’outils divers pour l’automatisation des processus de preuve de théorème, la consultation et la navigation dans les corpus, d’intégrations avec d’autres environnement de démonstration de théorème, et fournir un base rigoureuse pour les systèmes d’algèbre informatique et les langages de programmation. Il semble au point mort. J’en ai pris connaissance sur une page déjà ancienne (et qui pour preuve, contenait des liens obsolètes), ce qui suggère que Ghilbert n’est pas une initiative récente, et pourtant, on peut lire, ceci : Ghilbert Specification (sites.google.com) Spécification a écrit : obviously very rough draft, work in progress, at this point C’est donc toujours à l’état de brouillon brute depuis un temps suffisant pour qu’entre temps des choses du domaines (des sites et systèmes), aient eu le temps de disparaitre. C’est utile de connaitre son existence, mais je conseillerais d’en rester à OpenTheory, qui me semble un meilleur candidat pour un format standard pérenne.


Hibou Administrateur Genre : Messages : 22281	Lun 25 Mar 2019 18:53 Re: Standard pour la transmission de preuves et théories OpenTheory est un format d’archivage, pas d’édition, la modification est difficile. Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon]