Metamath | EPFL Graph Search

Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?

Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur GraphSearch.

Découvrez-en plus sur les applications Graph.

Metamath est un langage formel et un logiciel associé (un assistant de preuve) pour rassembler, vérifier et étudier les preuves de théorèmes mathématiques. Plusieurs bases de théorèmes avec leurs preuves ont été développés avec Metamath. Elles rassemblent des résultats standards en logique, théorie des ensembles, théorie des nombres, algèbre, topologie, analyse, entre autres domaines. Début 2022, les théorèmes prouvées à l'aide de Metamath forment l'un des plus grands corps de mathématiques formalisées, et incluent notamment 74 des 100 théorèmes du défi "Formalizing 100 Theorems", ce qui en fait le quatrième après HOL Light et Isabelle et Coq, mais devant , Mizar, Proof Power, Lean, Nqthm, ACL2, et Nuprl. Il y a au moins 17 vérificateurs de preuves pour les bases de théorèmes au format Metamath. Ce projet est le premier de son genre qui permet la navigation interactive d'une base de théorèmes formalisés sous la forme d'un site web. Le langage Metamath est un metalanguage, adapté au développement d'une grande variété de systèmes formels. Le langage Metamath n'a pas de logique prédéfinie intégrée. Au lieu de cela, il peut être considéré simplement comme un moyen de prouver que les règles d'inférence (définies comme axiomes ou démontrées) peuvent être appliquées. La plus grande base de preuves concernent la logique classique et les théorèmes de la théorie des ensembles ZFC, mais il existe d'autres bases de données et d'autres peuvent être créés. La conception du langage Metamath se concentre sur la simplicité. Le langage, utilisé pour déclarer les définitions, axiomes, règles d'inférence et théorèmes ne se compose que d'une poignée de mots-clés, et toutes les preuves sont vérifiées à l'aide d'un algorithme simple basé sur les substitutions de variables (avec des contraintes possibles sur la liste des variables qui doivent rester distinctes après substitution). L'ensemble des symboles qui peuvent être utilisés pour construire des formules est déclaré en utilisant

c (déclaration de constante) et

v (déclaration de variable) déclarations.

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Publications associées (3)

Unités associées (1)

Concepts associés (10)

Cours associés (4)

Séances de cours associées (7)

LISA – A Modern Proof System

Viktor Kuncak, Simon Guilloud, Sankalp Gambhir

We present LISA, a proof system and proof assistant for constructing proofs in schematic first-order logic and axiomatic set theory. The logical kernel of the system is a proof checker for first-order logic with equality and schematic predicate and fun ...

2023

A Formally Verified NAT

George Candea, Solal Vincenzo Pirelli, Arseniy Zaostrovnykh, Luis David Figueiredo Mascarenhas Moreira Pedrosa

We present a Network Address Translator (NAT) written in C and proven to be semantically correct according to RFC 3022, as well as crash-free and memory-safe. There exists a lot of recent work on network verification, but it mostly assumes models of networ ...

Assoc Computing Machinery2017

Axiom: DTLS-Based Secure IoT Group Communication

Kirill Nikitin

This article presents Axiom, a DTLS-based approach to efficiently secure multicast group communication among IoT-constrained devices. Axiom provides an adaptation of the DTLS record layer, relies on key material commonly shared among the group members, and ...

Assoc Computing Machinery2017

CS-628: Interactive Theorem Proving CS

A hands-on introduction to interactive theorem proving, proofs as programs, dependent types, and to the Coq proof assistant. Come learn how to write bug-free code!

MATH-381: Mathematical logic

Branche des mathématiques en lien avec le fondement des mathématiques et l'informatique théorique. Le cours est centré sur la logique du 1er ordre et l'articulation entre syntaxe et sémantique.

CS-550: Formal verification

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to u

Isabelle (logiciel)

The Isabelle automated theorem prover is a higher-order logic (HOL) theorem prover, written in Standard ML and Scala. As an LCF-style theorem prover, it is based on a small logical core (kernel) to increase the trustworthiness of proofs without requiring yet supporting explicit proof objects. Isabelle is available inside a flexible system framework allowing for logically safe extensions, which comprise both theories as well as implementations for code-generation, documentation, and specific support for a variety of formal methods.

Logique

La logique — du grec , qui est un terme dérivé de signifiant à la fois « raison », « langage » et « raisonnement » — est, dans une première approche, l'étude de l'inférence, c'est-à-dire des règles formelles que doit respecter toute argumentation correcte. Le terme aurait été utilisé pour la première fois par Xénocrate. La logique antique se décompose d'abord en dialectique et rhétorique. Elle est depuis l'Antiquité l'une des grandes disciplines de la philosophie, avec l'éthique (philosophie morale) et la physique (science de la nature).

Système à la Hilbert

En logique, les systèmes à la Hilbert servent à définir les déductions formelles en suivant un modèle proposé par David Hilbert au début du : un grand nombre daxiomes logiques exprimant les principales propriétés de la logique que l'on combine au moyen de quelques règles, notamment la règle de modus ponens, pour dériver de nouveaux théorèmes. Les systèmes à la Hilbert héritent du système défini par Gottlob Frege et constituent les premiers systèmes déductifs, avant l'apparition de la déduction naturelle ou du calcul des séquents, appelés parfois par opposition systèmes à la Gentzen.

Les langues d'Isabelle : Isar, ML et Scala

Explore les langues d'Isar, de ML et de Scala, couvrant les systèmes de preuve, les règles de déduction naturelle, les définitions inductives et l'approche LCF.

Théorie de Galois: Récapitulation et Transitivité MATH-482: Number theory I.a - Algebraic number theory

Couvre la récapitulation de la théorie Galois et met l'accent sur la transitivité des groupes Galois.

Groupe symétrique: Notation de cycle MATH-310: Algebra

Explore le groupe symétrique, en mettant l'accent sur la notation du cycle et les propriétés du groupe.