The Isabelle theorem prover is an interactive theorem proving framework, a successor of the Higher Order Logic (HOL) theorem prover. It is an LCF-style theorem prover, so it is based on a small logical core guaranteeing logical correctness. Isabelle is generic: it provides a meta-logic, which is used to encode object logics like First-order logic (FOL), Higher-order logic (HOL) or ZFC. Isabelle's main proof method is a higher-order version of resolution, based on higher-order unification.

PropertyValue
dbpedia-owl:Software/license
dbpedia-owl:license
dbpprop:abstract
  • The Isabelle theorem prover is an interactive theorem proving framework, a successor of the Higher Order Logic (HOL) theorem prover. It is an LCF-style theorem prover, so it is based on a small logical core guaranteeing logical correctness. Isabelle is generic: it provides a meta-logic, which is used to encode object logics like First-order logic (FOL), Higher-order logic (HOL) or ZFC. Isabelle's main proof method is a higher-order version of resolution, based on higher-order unification. Though interactive, Isabelle also features efficient automatic reasoning tools, such as a term rewriting engine and a tableaux prover, as well as various decision procedures. Isabelle has been used to formalize numerous theorems from mathematics and computer science, like Gödel's completeness theorem, Gödel's theorem about the consistency of the axiom of choice, the prime number theorem, correctness of security protocols, and properties of programming language semantics. The Isabelle theorem prover is free software, released under the revised BSD license.
  • Isabelle ist ein generischer interaktiver Theorembeweiser, der von den Forschungsgruppen um Lawrence Paulson und Tobias Nipkow entwickelt wird. Ein wichtiger Anwendungsbereich von Isabelle ist die formale Verifizierung von Hard- und Software. Isabelle ist in der Programmiersprache Standard ML geschrieben und ist freie Software unter der BSD-Lizenz. Am australischen Forschungsinstitut NICTA wurde mithilfe von Isabelle erstmals die Korrektheit eines Kernels (Secure Embedded L4) formal bewiesen. Von den insgesamt 8700 Zeilen Code wurden 7500 bewiesen; der Rest ist Boot-Code, der nur initial ausgeführt wird.
  • El demostrador interactivo de teoremas Isabelle es una herramienta de ayuda a la demostración de teoremas escrita en el lenguaje de programación ML y desarrollada por Larry Paulson de la Universidad de Cambridge y Tobias Nipkow del Technische Universität München. El lenguaje en el cual se realizan las pruebas es HOL (acrónimo de Higher-Order Logic), que es un lenguaje fuertemente tipificado con estructuras de datos, funciones recursivas (incluyendo valores funcionales) y expresiones lógicas con cuantificadores. Entre las características más destacables de Isabelle se pueden mencionar: Sistema de deducción natural Inferencia de tipos para verificar que los términos manejados estén bien construidos Módulos llamados teorías Conjuntos y tipos de datos recursivos Inducción estructural Facilidades para realizar demostraciones interactivas Simplificación por reescritura de términos
  • Le logiciel Isabelle est un assistant de preuve, c'est-à-dire un démonstrateur interactif de théorèmes. C'est le successeur de HOL.
dbpprop:genre
  • Mathematics
dbpprop:hasPhotoCollection
dbpprop:latestReleaseVersion
  • Isabelle 2009
dbpprop:license
dbpprop:name
  • Isabelle
dbpprop:operatingSystem
  • Linux, Solaris, Mac OS X, Windows (Cygwin)
dbpprop:portalProperty
  • Free Software Portal Logo.svg
  • Free software
dbpprop:programmingLanguage
  • Standard ML
dbpprop:reference
dbpprop:website
dbpprop:wikiPageUsesTemplate
rdf:type
rdfs:comment
  • The Isabelle theorem prover is an interactive theorem proving framework, a successor of the Higher Order Logic (HOL) theorem prover. It is an LCF-style theorem prover, so it is based on a small logical core guaranteeing logical correctness. Isabelle is generic: it provides a meta-logic, which is used to encode object logics like First-order logic (FOL), Higher-order logic (HOL) or ZFC. Isabelle's main proof method is a higher-order version of resolution, based on higher-order unification.
  • Isabelle ist ein generischer interaktiver Theorembeweiser, der von den Forschungsgruppen um Lawrence Paulson und Tobias Nipkow entwickelt wird. Ein wichtiger Anwendungsbereich von Isabelle ist die formale Verifizierung von Hard- und Software. Isabelle ist in der Programmiersprache Standard ML geschrieben und ist freie Software unter der BSD-Lizenz. Am australischen Forschungsinstitut NICTA wurde mithilfe von Isabelle erstmals die Korrektheit eines Kernels (Secure Embedded L4) formal bewiesen.
  • El demostrador interactivo de teoremas Isabelle es una herramienta de ayuda a la demostración de teoremas escrita en el lenguaje de programación ML y desarrollada por Larry Paulson de la Universidad de Cambridge y Tobias Nipkow del Technische Universität München.
  • Le logiciel Isabelle est un assistant de preuve, c'est-à-dire un démonstrateur interactif de théorèmes. C'est le successeur de HOL.
rdfs:label
  • Isabelle (theorem prover)
  • Isabelle (Theorembeweiser)
  • Demostrador de teoremas Isabelle
  • Isabelle (logiciel)
owl:sameAs
skos:subject
foaf:homepage
foaf:name
  • Isabelle
foaf:page
is dbpprop:disambiguates of
is dbpprop:redirect of