Isabelle (proof assistant) (original) (raw)
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 ?
| Property | Value |
|---|---|
| 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 | dbr:Lawrence_Paulson |
| dbo:developer | dbr:University_of_Cambridge dbr:Technical_University_of_Munich |
| dbo:genre | dbr:Mathematics |
| dbo:latestReleaseVersion | Isabelle2021 |
| dbo:license | dbr:BSD_license |
| dbo:operatingSystem | dbr:Linux dbr:MacOS dbr:Windows |
| dbo:programmingLanguage | dbr:Scala_(programming_language) dbr:Standard_ML |
| dbo:thumbnail | wiki-commons:Special:FilePath/Isabelle_jedit.png?width=300 |
| dbo:wikiPageExternalLink | https://isabelle.in.tum.de/doc/tutorial.pdf https://isabelle.in.tum.de https://isarmathlib.org https://isabelle.in.tum.de/ https://arxiv.org/abs/cs/9301105 https://link.springer.com/chapter/10.1007/BFb0000502 https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-189.pdf https://stackoverflow.com/tags/isabelle/ https://www.isa-afp.org/ |
| dbo:wikiPageID | 161886 (xsd:integer) |
| dbo:wikiPageLength | 13475 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1124441980 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:BSD_license dbr:Prime_number_theorem dbr:Python_(programming_language) dbr:Scala_(programming_language) dbr:Mizar_system dbr:Model_theory dbr:Prover9 dbr:Declarative_programming dbr:Resolution_(logic) dbr:University_of_Cambridge dbr:E_(theorem_prover) dbr:Lightweight_Java dbr:LCF_theorem_prover dbc:Software_using_the_BSD_license dbr:Coq dbr:Mathematics dbr:SPASS dbr:Free_Pascal dbr:NICTA dbr:LEGO_(proof_assistant) dbr:Linux dbr:MacOS dbr:Standard_ML dbr:Standard_ML_of_New_Jersey dbr:Subroutine dbr:Computer_science dbr:Zermelo–Fraenkel_set_theory dbr:Microkernel dbr:C++ dbr:C_(programming_language) dbr:Type_theory dbr:Windows dbr:Gödel's_completeness_theorem dbr:Agda_(programming_language) dbr:First-order_logic dbr:Formal_semantics_of_programming_languages dbr:Formal_verification dbr:Formal_methods dbr:Lemma_(mathematics) dbr:Proof_by_contradiction dbr:First-order_resolution dbr:Procedural_programming dbr:Gérard_Huet dbr:HOL_(proof_assistant) dbr:Haskell_(programming_language) dbr:Technical_University_of_Munich dbr:Counterexample dbr:Term_rewriting dbr:Twelf dbr:ANSI_C dbc:Free_theorem_provers dbc:Proof_assistants dbr:L4_microkernel_family dbr:Lawrence_Paulson dbr:Lean_(proof_assistant) dbr:Higher-order_logic dbr:Automated_theorem_prover dbr:Axiom_of_choice dbr:Square_root_of_2 dbr:Free_software dbr:Meta-logic dbr:Integrated_development_environment dbr:Metamath dbr:Method_of_analytic_tableaux dbr:OCaml dbr:CVC4 dbr:Satisfiability_modulo_theories dbr:Tobias_Nipkow dbr:Lawrence_C._Paulson dbr:Security_protocol dbr:Unification_(computing) dbr:Type_soundness dbr:Tactic_(computer_science) |
| dbp:author | dbr:Lawrence_Paulson |
| dbp:caption | Isabelle/jEdit running on macOS (en) |
| dbp:developer | University of Cambridge and Technical University of Munich et al. (en) |
| dbp:genre | dbr:Mathematics |
| dbp:latestReleaseVersion | Isabelle2021 (en) |
| dbp:license | dbr:BSD_license |
| dbp:name | Isabelle (en) |
| dbp:operatingSystem | dbr:Linux dbr:MacOS dbr:Windows |
| dbp:programmingLanguage | Standard ML and Scala (en) |
| dbp:released | 1986 (xsd:integer) |
| dbp:screenshot | Isabelle jedit.png (en) |
| dbp:website | https://isabelle.in.tum.de/ |
| dbp:wikiPageUsesTemplate | dbt:= dbt:Citation_needed dbt:Color dbt:Efn dbt:Further dbt:IPAc-en dbt:Infobox_software dbt:Notelist dbt:Portal dbt:Refbegin dbt:Refend dbt:Reflist dbt:Short_description dbt:Start_date_and_age dbt:Green dbt:Mathbb dbt:Olive dbt:Issn dbt:Blue |
| dct:subject | dbc:Software_using_the_BSD_license dbc:Free_theorem_provers dbc:Proof_assistants |
| gold:hypernym | dbr:Prover |
| rdf:type | owl:Thing dbo:Software schema:CreativeWork dbo:Work wikidata:Q386724 wikidata:Q7397 yago:Abstraction100002137 yago:Code106355894 yago:CodingSystem106353757 yago:Communication100033020 yago:Writing106359877 yago:WrittenCommunication106349220 yago:Software106566077 umbel-rc:SoftwareObject |
| 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 | freebase:Isabelle (proof assistant) wikidata:Isabelle (proof assistant) dbpedia-de:Isabelle (proof assistant) dbpedia-es:Isabelle (proof assistant) dbpedia-fr:Isabelle (proof assistant) dbpedia-pt:Isabelle (proof assistant) dbpedia-ru:Isabelle (proof assistant) dbpedia-zh:Isabelle (proof assistant) https://global.dbpedia.org/id/4GTTK |
| prov:wasDerivedFrom | wikipedia-en:Isabelle_(proof_assistant)?oldid=1124441980&ns=0 |
| foaf:depiction | wiki-commons:Special:FilePath/Isabelle_jedit.png |
| foaf:homepage | https://isabelle.in.tum.de/ |
| foaf:isPrimaryTopicOf | wikipedia-en:Isabelle_(proof_assistant) |
| foaf:name | Isabelle (en) |
| is dbo:knownFor of | dbr:Lawrence_Paulson |
| is dbo:wikiPageDisambiguates of | dbr:Isabelle_(disambiguation) |
| is dbo:wikiPageRedirects of | dbr:Metis_(theorem_prover) dbr:Archive_of_Formal_Proofs dbr:Nunchaku_(Isabelle) dbr:Intelligible_semi-automated_reasoning dbr:Sledgehammer_(Isabelle) dbr:Locale_(Isabelle) dbr:Isabelle_(theorem_prover) dbr:Isabelle_proof_assistant dbr:Isabelle_theorem_prover dbr:The_Archive_of_Formal_Proofs dbr:Isabelle/HOL dbr:Isabelle_AFP dbr:Isabelle_software dbr:Isar_(Isabelle) dbr:Nitpick_(Isabelle) |
| is dbo:wikiPageWikiLink of | dbr:Cantor's_theorem dbr:Proof_assistant dbr:Metis_(theorem_prover) dbr:Department_of_Computer_Science_and_Technology,_University_of_Cambridge dbr:Van_Emde_Boas_tree dbr:Archive_of_Formal_Proofs dbr:Isabelle_(disambiguation) dbr:Presburger_arithmetic dbr:Coq dbr:Nunchaku_(Isabelle) dbr:Thomas_Callister_Hales dbr:1986_in_science dbr:Standard_ML dbr:Mutilated_chessboard_problem dbr:Type_theory dbr:Agda_(programming_language) dbr:Dictatorship_mechanism dbr:Grigore_Roșu dbr:HOL_(proof_assistant) dbr:JFreeChart dbr:Kepler_conjecture dbr:Lawrence_Paulson dbr:TLA+ dbr:Automated_reasoning dbr:Integer dbr:Metamath dbr:Intelligible_semi-automated_reasoning dbr:Sledgehammer_(Isabelle) dbr:Locale_(Isabelle) dbr:Finger_tree dbr:Isabelle_(theorem_prover) dbr:Isabelle_proof_assistant dbr:Isabelle_theorem_prover dbr:The_Archive_of_Formal_Proofs dbr:Isabelle/HOL dbr:Isabelle_AFP dbr:Isabelle_software dbr:Isar_(Isabelle) dbr:Nitpick_(Isabelle) |
| is foaf:primaryTopic of | wikipedia-en:Isabelle_(proof_assistant) |
