#1 Le 04/02/2013, à 23:29
- Hibou57
[Standard] 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 
Dernière modification par Hibou57 (Le 05/02/2013, à 03:37)
Hajimemashteeeee… \(^o^)/ Tachikoma desu (^_^;)
Le saviez‑vous : le j’m’en foutisme est la cause de la plupart des fléaux du monde contemporain.
Mangez des standards : un grand bol de Standard tous les matins, et vous débutez la journée en pleine forme !
bulleforum.net — Forum de discussions, La Bulle (papotage de la vie courante ou choses trop sérieuses)
Hors ligne
#2 Le 07/02/2013, à 01:03
- Hibou57
Re : [Standard] 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)
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.
Dernière modification par Hibou57 (Le 07/02/2013, à 01:07)
Hajimemashteeeee… \(^o^)/ Tachikoma desu (^_^;)
Le saviez‑vous : le j’m’en foutisme est la cause de la plupart des fléaux du monde contemporain.
Mangez des standards : un grand bol de Standard tous les matins, et vous débutez la journée en pleine forme !
bulleforum.net — Forum de discussions, La Bulle (papotage de la vie courante ou choses trop sérieuses)
Hors ligne