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. It can be seen as an IDE for formal methods. In recent years, a substantial number of theories and system extensions have been collected in the Isabelle Archive of Formal Proofs (Isabelle AFP) Isabelle was named by Lawrence Paulson after Gérard Huet's daughter. The Isabelle theorem prover is free software, released under the revised BSD license. Isabelle is generic: it provides a meta-logic (a weak type theory), which is used to encode object logics like first-order logic (FOL), higher-order logic (HOL) or Zermelo–Fraenkel set theory (ZFC). The most widely used object logic is Isabelle/HOL, although significant set theory developments were completed in Isabelle/ZF. Isabelle's main proof method is a higher-order version of resolution, based on higher-order unification. Though interactive, Isabelle features efficient automatic reasoning tools, such as a term rewriting engine and a tableaux prover, various decision procedures, and, through the Sledgehammer proof-automation interface, external satisfiability modulo theories (SMT) solvers (including CVC4) and resolution-based automated theorem provers (ATPs), including E and SPASS (the Metis proof method reconstructs resolution proofs generated by these ATPs). It also features two model finders (counterexample generators): Nitpick and Nunchaku. Isabelle features locales which are modules that structure large proofs. A locale fixes types, constants, and assumptions within a specified scope so that they do not have to be repeated for every lemma.

À 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.

Concepts associés (17)

Cours associés (6)

Séances de cours associées (75)

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!

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

CS-101: Advanced information, computation, communication I

Discrete mathematics is a discipline with applications to almost all areas of study. It provides a set of indispensable tools to computer science in particular. This course reviews (familiar) topics a

Isabelle (logiciel)

Unification

vignette|Unifier deux termes, c'est les rendre identiques en remplaçant les variables. En informatique et en logique, l'unification est un processus algorithmique qui, étant donnés deux termes, trouve une substitution qui appliquée aux deux termes les rend identiques. Par exemple, et peuvent être rendus identiques par la substitution et , qui donne quand on l'applique à chacun de ces termes le terme .

Metamath

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.

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.

Assistant à la preuve de la LISA : formalisation et vérification CS-550: Formal verification

Couvre l'organisation de la base de code de l'assistante d'épreuve LISA, le paquet noyau, la formalisation FOL et le paquet d'épreuves.

Coq: Vue d'ensemble

Présente Coq et se concentre sur la démonstration du théorème et du _comm étape par étape.