| dbo:abstract
|
- Isabelle ist ein generischer interaktiver Theorembeweiser mit besonderemSchwerpunkt auf Higher-Order Logic (HOL). Ein wichtiger Anwendungsbereich von Isabelle ist die formale Verifizierung von Hard- und Software. Die Implementierungssprachen von Isabelle sind Standard ML und Scala. Das Basis-System unterliegt der BSD-Lizenz, während zusätzliche Komponenten unter Umständen andere Lizenzen für freie Software verwenden. Am australischen Forschungsinstitut NICTA wurde mithilfe von Isabelle erstmals die Korrektheit eines Kernels (Secure Embedded L4 (seL4)) formal bewiesen. Bei einer Programmlänge von insgesamt 8700 Zeilen Code wurde die Korrektheit von 7500 Zeilen gezeigt; der Rest ist Boot-Code, der nur initial ausgeführt wird. (de)
- 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. (en)
- 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 de la Universidad de Cambridge y del Technische Universität München. El lenguaje en que se realizan las pruebas es HOL (acrónimo de Higher-Order Logic), que es un lenguaje fuertemente tipado 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 (es)
- Le logiciel Isabelle est un assistant de preuve, c'est-à-dire un démonstrateur interactif de théorèmes. C'est le successeur de (en). C’est un logiciel libre publié sous licence BSD. Cette section est vide, insuffisamment détaillée ou incomplète. Votre aide est la bienvenue ! Comment faire ? (fr)
- Isabelle é um programa de computador utilizado para processar fórmulas matemáticas. Foi desenvolvido por um (da Universidade de Cambridge, no Reino Unido) e (da Universidade Técnica de Munique, na Alemanha). Trata-se de um ambiente de demonstrações que permite a representação e o uso de diversos sistemas como Pure, ZF, FOL, estruturado por uma metalógica intuicionista de . As podem ser especificadas em diferentes formatos, como por exemplo, dedução natural, , , , dentre outras, e possui três componentes principais: uma meta-implicação que possibilita o uso de regras da lógica-objeto específica e que é responsável pela aplicação dessas regras e no resultado das ; uma meta-quantificação universal sobre inúmeros quantificadores da linguagem-objeto; uma meta-igualdade que torna uma abreviação apenas uma maneira de reescrever regras. Pode ser visto como um provador de teoremas onde: lógica-objetos são λ-termos cuja os torna não ambíguos; regras da linguagem-objeto não são representadas como funções, mas como fórmulas da lógica de ordem superior; a combinação e aplicação dessas regras são executadas por um de inferência, a ; táticas são independentemente da lógica-objeto representada. (pt)
- Isabelle 是一个基于高阶逻辑（higher-order logic）的通用交互式定理证明器。它是一个 LCF（Logic for Computable Functions）风格的证明辅助工具，使用 Standard ML 语言实现。它拥有一个极小化的逻辑核心；这意味着使用它的证明和形式化验证具有较强的的可信度。 Isabelle 是通用的：它提供了一套（相当于一个较弱版本的类型论），可用于编码诸多对象逻辑，如一阶逻辑、高阶逻辑、或ZF集合论。最常被用到的对象逻辑是 Isabelle/HOL；而其对集合论的形式化工作则使用了 Isabelle/ZF。Isabelle 的主要证明手段利用了高阶版本的归结原理（resolution），基于高阶的合一（unification）。 尽管 Isabelle 主要采取交互式的证明方式，它同时亦提供了若干高效的自动化推理工具，例如项重写引擎、tableaux 证明器、以及各种判定过程。藉由 sledgehammer 界面，它还可以调用外部的 SMT 求解器（包括 CVC4）和其他归结式定理证明器（包括 E 和 SPASS）。 Isabelle 被用于形式化数学和计算机科学中的许多定理，诸如哥德尔完备性定理、哥德尔关于选择公理一致性的证明、素数定理、各种安全协议的正确性、程序语言语义的特性。这些定理形式化工作的维护通过形式化证明存档（Archive of Formal Proofs）进行；截至 2019 年它已包含逾 500 个条目，两百万行证明。 Isabelle 定理证明器是开源软件，其源码在 BSD license 下授权发布。 “Isabelle”由其作者 Lawrence Paulson 命名；这名字取自于法国计算机科学家 的女儿。 (zh)
- Isabelle — интерактивный инструмент для автоматического доказательства, использующий логику высшего порядка. Реализован в том же стиле, что и один из первых подобных инструментов — LCF и, точно так же как и LCF, был первоначально полностью написан на языке Standard ML. Система содержит компактное логическое ядро, которое можно принимать в качестве истинного без дополнительных доказательств (хотя это и не обязательно). Как универсальный инструмент, реализует металогику (слабую теорию типов), которая используется для реализации нескольких вариантов логики объектов Isabelle, таких как логика первого порядка (FOL), логика высшего порядка (HOL) или теория множеств Цермело-Френкеля (ZFC). Чаще всего используется вариант объектной логики является Isabelle/HOL, так же достаточно серьёзные разработки в области теории множеств проводились с использованием Isabelle/ZF. Основным методом реализации доказательства Isabelle является вариант резолюции высшего порядка, основанный на алгоритме унификации высшего порядка. Будучи интерактивной системой, Isabelle также включает в свой состав эффективные инструменты автоматического рассуждения, такие как механизм переписывания термов, решатель , внешние решатели выполнимости задач в различных теориях, подключаемые через специализированный интерфейс подключения внешних плагинов Sledgehammer, а также внешние инструменты автоматического доказывания теорем, такие как и . Isabelle была использована для формализации многочисленных теорем из математики и информатики, таких как теорема Гёделя о полноте, доказательство Гёделя о независимости , теоремы о распределении простых чисел. Также Isabelle использовалась для доказательства формальной корректности криптографических протоколов и свойств семантики языков программирования. Многие из формальных доказательств, полученных с применением Isabelle, доступны публично и хранятся в «Архиве формальных доказательств» (Archive of Formal Proofs), который содержит (по состоянию на 2019 год) не менее 500 статей, включающих в себя более 2 млн строк кода. Распространяется свободно под лицензией BSD.Автор — (англ. Lawrence Paulson), название дано в честь дочери Жерара Юэ. (ru)
|
| dbo:author
| |
| dbo:developer
| |
| dbo:genre
| |
| dbo:latestReleaseVersion
| |
| dbo:license
| |
| dbo:operatingSystem
| |
| dbo:programmingLanguage
| |
| dbo:thumbnail
| |
| dbo:wikiPageExternalLink
| |
| dbo:wikiPageID
| |
| dbo:wikiPageLength
|
- 13475 (xsd:nonNegativeInteger)
|
| dbo:wikiPageRevisionID
| |
| dbo:wikiPageWikiLink
| |
| dbp:author
| |
| dbp:caption
|
- Isabelle/jEdit running on macOS (en)
|
| dbp:developer
|
- University of Cambridge and Technical University of Munich et al. (en)
|
| dbp:genre
| |
| dbp:latestReleaseVersion
| |
| dbp:license
| |
| dbp:name
| |
| dbp:operatingSystem
| |
| dbp:programmingLanguage
|
- Standard ML and Scala (en)
|
| dbp:released
| |
| dbp:screenshot
| |
| dbp:website
| |
| dbp:wikiPageUsesTemplate
| |
| dcterms:subject
| |
| gold:hypernym
| |
| rdf:type
| |
| rdfs:comment
|
- Le logiciel Isabelle est un assistant de preuve, c'est-à-dire un démonstrateur interactif de théorèmes. C'est le successeur de (en). C’est un logiciel libre publié sous licence BSD. Cette section est vide, insuffisamment détaillée ou incomplète. Votre aide est la bienvenue ! Comment faire ? (fr)
- Isabelle ist ein generischer interaktiver Theorembeweiser mit besonderemSchwerpunkt auf Higher-Order Logic (HOL). Ein wichtiger Anwendungsbereich von Isabelle ist die formale Verifizierung von Hard- und Software. Die Implementierungssprachen von Isabelle sind Standard ML und Scala. Das Basis-System unterliegt der BSD-Lizenz, während zusätzliche Komponenten unter Umständen andere Lizenzen für freie Software verwenden. (de)
- 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 de la Universidad de Cambridge y del Technische Universität München. El lenguaje en que se realizan las pruebas es HOL (acrónimo de Higher-Order Logic), que es un lenguaje fuertemente tipado 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: (es)
- 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 was named by Lawrence Paulson after Gérard Huet's daughter. The Isabelle theorem prover is free software, released under the revised BSD license. (en)
- Isabelle é um programa de computador utilizado para processar fórmulas matemáticas. Foi desenvolvido por um (da Universidade de Cambridge, no Reino Unido) e (da Universidade Técnica de Munique, na Alemanha). Trata-se de um ambiente de demonstrações que permite a representação e o uso de diversos sistemas como Pure, ZF, FOL, estruturado por uma metalógica intuicionista de . (pt)
- Isabelle — интерактивный инструмент для автоматического доказательства, использующий логику высшего порядка. Реализован в том же стиле, что и один из первых подобных инструментов — LCF и, точно так же как и LCF, был первоначально полностью написан на языке Standard ML. Система содержит компактное логическое ядро, которое можно принимать в качестве истинного без дополнительных доказательств (хотя это и не обязательно). Как универсальный инструмент, реализует металогику (слабую теорию типов), которая используется для реализации нескольких вариантов логики объектов Isabelle, таких как логика первого порядка (FOL), логика высшего порядка (HOL) или теория множеств Цермело-Френкеля (ZFC). Чаще всего используется вариант объектной логики является Isabelle/HOL, так же достаточно серьёзные разработ (ru)
- Isabelle 是一个基于高阶逻辑（higher-order logic）的通用交互式定理证明器。它是一个 LCF（Logic for Computable Functions）风格的证明辅助工具，使用 Standard ML 语言实现。它拥有一个极小化的逻辑核心；这意味着使用它的证明和形式化验证具有较强的的可信度。 Isabelle 是通用的：它提供了一套（相当于一个较弱版本的类型论），可用于编码诸多对象逻辑，如一阶逻辑、高阶逻辑、或ZF集合论。最常被用到的对象逻辑是 Isabelle/HOL；而其对集合论的形式化工作则使用了 Isabelle/ZF。Isabelle 的主要证明手段利用了高阶版本的归结原理（resolution），基于高阶的合一（unification）。 尽管 Isabelle 主要采取交互式的证明方式，它同时亦提供了若干高效的自动化推理工具，例如项重写引擎、tableaux 证明器、以及各种判定过程。藉由 sledgehammer 界面，它还可以调用外部的 SMT 求解器（包括 CVC4）和其他归结式定理证明器（包括 E 和 SPASS）。 Isabelle 定理证明器是开源软件，其源码在 BSD license 下授权发布。 “Isabelle”由其作者 Lawrence Paulson 命名；这名字取自于法国计算机科学家 的女儿。 (zh)
|
| rdfs:label
|
- Isabelle (Theorembeweiser) (de)
- Isabelle (es)
- Isabelle (logiciel) (fr)
- Isabelle (proof assistant) (en)
- Isabelle (pt)
- Isabelle (ru)
- Isabelle (zh)
|
| owl:sameAs
| |
| prov:wasDerivedFrom
| |
| foaf:depiction
| |
| foaf:homepage
| |
| foaf:isPrimaryTopicOf
| |
| foaf:name
| |
| is dbo:knownFor
of | |
| is dbo:wikiPageDisambiguates
of | |
| is dbo:wikiPageRedirects
of | |
| is dbo:wikiPageWikiLink
of | |
| is foaf:primaryTopic
of | |
