Menu
Accueil
Forums
Liste des forums
En ce moment
Nouveaux messages
Nouveaux messages de profil
Connexion
S'inscrire
Quoi de neuf
Liste des forums
Menu
Connexion
S'inscrire
Forums
Loisirs et Entraides
Etudiant
Est ce une nouvelle découverte en mathématiques ?.
JavaScript est désactivé. Pour une meilleure expérience, veuillez activer JavaScript dans votre navigateur avant de continuer.
Vous utilisez un navigateur obsolète. Il se peut que ce site ou d'autres sites Web ne s'affichent pas correctement.
Vous devez le mettre à jour ou utiliser un
navigateur alternatif
.
Répondre à la discussion
Message
[QUOTE="Hibou57, post: 13967239, member: 82014"] Non, je ne peux pas. Je donnais des pistes, je n’ai pas dit que je pouvais être la personne qui convient. Sinon, si tu peux être patient, commencer à étudier soit Coq soit Isabelle (je conseillerais plutôt Coq, même si un choix entre les deux est difficile). Coq repose sur la logique constructiviste (pas de tiers‑exclus, etc), qui permet d’éviter les fausses pistes dans une démonstration. Sont éditeur de preuve est plus commode et maniable que celui de Isabelle, et il est également plus réputé que ce dernier (quelques preuves qui ont fait du bruit, ont été validé avec Coq). Isabelle repose sur HOL (Higher Order Logic), une logique courante, mais qui existe en plusieurs variantes. Pas mieux du côté de Coq cependant, qui utilise une logique propre, même si elle dérive de logiques connues. Isabelle a l’avantage sur Coq, de permettre d’écrire des preuves structurée, avec un bon rendu PDF, ce qui peut être intéressant pour transmettre des preuves à des tiers. Je ne peux rien faire de plus que donner des avis et des pistes, ne m’en demandes pas plus. [/QUOTE]
Insérer les messages sélectionnés…
Vérification
Répondre
Forums
Loisirs et Entraides
Etudiant
Est ce une nouvelle découverte en mathématiques ?.
Haut