Je suis des assistants de preuve auto-apprenants et j'ai décidé de commencer sur quelques preuves de base et de progresser. Étant donné que les preuves sont basées sur d'autres preuves et forment donc une hiérarchie, existe-t-il un référentiel de la hiérarchie des preuves?
Je sais que je peux choisir un assistant de preuve particulier et analyser sa bibliothèque pour extraire sa hiérarchie, mais si je veux trouver la prochaine preuve dans une chaîne à prouver, je ne peux pas quand elle n'est pas dans la bibliothèque.
Dans mon esprit, j'imagine un graphique, probablement un DAG , de toutes les preuves mathématiques connues qui peuvent être exprimées en utilisant des énoncés en anglais, pas des preuves en utilisant des images . Ce serait la carte principale (une carte dans le sens de commencer à un point et de voyager vers un autre point via des points intermédiaires), et pour un assistant de preuve particulier, on aurait un sous-graphique de la carte principale. Ensuite, si l'on voulait créer une preuve à l'aide d'un assistant de preuve trouvé sur le maître et non sur le sous-graphique, en comparant les deux graphiques, on pourrait avoir une idée du travail nécessaire pour créer la ou les preuves manquantes pour l'assistant de preuve.
Je suis conscient que les preuves mathématiques ne sont pas nécessairement facilement convertibles pour une utilisation avec un assistant de preuve, mais avoir une idée générale de ce qu'il faut faire est bien mieux que rien du tout.
De plus, en ayant la carte principale, je peux voir s'il y a plusieurs chemins d'un point à un autre et choisir un chemin qui convient mieux à l'assistant de preuve particulier.
ÉDITER
En cherchant, j'ai trouvé quelque chose de similaire pour les fonctions mathématiques . Je n'en ai pas trouvé de preuves au NIST
la source
Réponses:
Le système Mizar est un énorme référentiel de preuves mathématiques. Voir la page wikipedia et le site officiel .
De wikipedia / Mizar_system # Mizar_language :
Les preuves sont écrites sous forme d'articles, dont il existe plus d'un millier d'articles et plus de 50 000 théorèmes éprouvés. La page wikipedia mentionne quelques idées intéressantes du " manifeste QED ", et comment Mizar pourrait être sur la bonne voie pour y parvenir.
la source
ProofWiki contient une quantité décente de preuves provenant de divers domaines des mathématiques. Ce n'est en aucun cas complet, mais c'est un bon point de départ pour ce que vous voulez.
la source
Metamath dispose d'une large sélection de preuves, construites directement à partir de leur noyau dans une logique propositionnelle.
Cela dit, il manque cruellement en termes de théorie CS. N'hésitez pas à l'agrandir!
la source
Voir l' archive TPTP , Des milliers de problèmes pour les fournisseurs de théorèmes. C'est quelque peu standard dans le domaine. Il s'agit plus des "nœuds" du graphe théorème que vous demandez. Certains articles faisant référence à l'archive ont peut-être exploré les bords de ce graphique.
Notez que dans le domaine de l'ATM, de la démonstration automatisée de théorèmes et de la démonstration assistée de théorèmes, les preuves sont symboliques et il n'est pas vraiment possible ou plausible d'étudier les "preuves en langue anglaise" comme vous le visualisez.
Cependant, vous pourriez en apprendre davantage sur le paradoxe de Richard qui a commencé comme une formulation de langage et a ensuite été formalisé symboliquement. On dit qu'il est l'inspiration des «antimonies» (contradictions) trouvées dans la théorie des premiers ensembles qui, historiquement, a même ouvert la voie au théorème d'incomplétude de Gödel.
la source