This HTML5 document contains 240 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
dbpedia-dehttp://de.dbpedia.org/resource/
dctermshttp://purl.org/dc/terms/
n31https://isabelle.in.tum.de/doc/
n18https://isabelle.in.tum.de/
dbohttp://dbpedia.org/ontology/
foafhttp://xmlns.com/foaf/0.1/
n32https://stackoverflow.com/tags/isabelle/
dbpedia-eshttp://es.dbpedia.org/resource/
n21https://global.dbpedia.org/id/
n20https://www.isa-afp.org/
umbel-rchttp://umbel.org/umbel/rc/
yagohttp://dbpedia.org/class/yago/
dbpedia-ruhttp://ru.dbpedia.org/resource/
schemahttp://schema.org/
dbthttp://dbpedia.org/resource/Template:
rdfshttp://www.w3.org/2000/01/rdf-schema#
freebasehttp://rdf.freebase.com/ns/
dbpedia-pthttp://pt.dbpedia.org/resource/
n27https://link.springer.com/chapter/10.1007/
n26http://dbpedia.org/resource/Isabelle/
n13http://commons.wikimedia.org/wiki/Special:FilePath/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n10https://arxiv.org/abs/cs/
owlhttp://www.w3.org/2002/07/owl#
n17https://
dbpedia-frhttp://fr.dbpedia.org/resource/
dbpedia-zhhttp://zh.dbpedia.org/resource/
wikipedia-enhttp://en.wikipedia.org/wiki/
dbphttp://dbpedia.org/property/
dbchttp://dbpedia.org/resource/Category:
provhttp://www.w3.org/ns/prov#
xsdhhttp://www.w3.org/2001/XMLSchema#
wikidatahttp://www.wikidata.org/entity/
goldhttp://purl.org/linguistics/gold/
dbrhttp://dbpedia.org/resource/
n29https://www.cl.cam.ac.uk/techreports/

Statements

Subject Item
dbr:Cantor's_theorem
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:Proof_assistant
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:Metis_(theorem_prover)
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
dbo:wikiPageRedirects
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:Department_of_Computer_Science_and_Technology,_University_of_Cambridge
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:Van_Emde_Boas_tree
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:Archive_of_Formal_Proofs
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
dbo:wikiPageRedirects
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:Isabelle_(disambiguation)
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
dbo:wikiPageDisambiguates
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:Presburger_arithmetic
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:Coq
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:Nunchaku_(Isabelle)
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
dbo:wikiPageRedirects
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:Thomas_Callister_Hales
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:1986_in_science
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:Standard_ML
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:Mutilated_chessboard_problem
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:Type_theory
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:Agda_(programming_language)
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:Dictatorship_mechanism
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:Grigore_Roșu
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:HOL_(proof_assistant)
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:Isabelle_(proof_assistant)
rdf:type
owl:Thing umbel-rc:SoftwareObject wikidata:Q7397 wikidata:Q386724 yago:Software106566077 dbo:Software dbo:Work yago:Abstraction100002137 yago:Communication100033020 yago:WrittenCommunication106349220 yago:CodingSystem106353757 schema:CreativeWork yago:Writing106359877 yago:Code106355894
rdfs:label
Isabelle Isabelle (logiciel) Isabelle Isabelle Isabelle (proof assistant) Isabelle Isabelle (Theorembeweiser)
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 ? 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: 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 命名;这名字取自于法国计算机科学家 的女儿。 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. 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 . 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. Isabelle — интерактивный инструмент для автоматического доказательства, использующий логику высшего порядка. Реализован в том же стиле, что и один из первых подобных инструментов — LCF и, точно так же как и LCF, был первоначально полностью написан на языке Standard ML. Система содержит компактное логическое ядро, которое можно принимать в качестве истинного без дополнительных доказательств (хотя это и не обязательно). Как универсальный инструмент, реализует металогику (слабую теорию типов), которая используется для реализации нескольких вариантов логики объектов Isabelle, таких как логика первого порядка (FOL), логика высшего порядка (HOL) или теория множеств Цермело-Френкеля (ZFC). Чаще всего используется вариант объектной логики является Isabelle/HOL, так же достаточно серьёзные разработ
foaf:name
Isabelle
foaf:homepage
n18:
dbp:name
Isabelle
foaf:depiction
n13:Isabelle_jedit.png
dcterms:subject
dbc:Free_theorem_provers dbc:Software_using_the_BSD_license dbc:Proof_assistants
dbo:wikiPageID
161886
dbo:wikiPageRevisionID
1124441980
dbo:wikiPageWikiLink
dbr:Security_protocol dbr:CVC4 dbr:E_(theorem_prover) dbr:C_(programming_language) dbr:Method_of_analytic_tableaux dbr:Declarative_programming dbr:Coq dbr:SPASS dbr:Zermelo–Fraenkel_set_theory dbr:Mathematics dbr:First-order_resolution dbr:Mizar_system dbc:Software_using_the_BSD_license dbr:MacOS dbr:Free_software dbr:Lawrence_Paulson dbc:Free_theorem_provers dbr:Metamath dbr:Microkernel dbr:Twelf dbr:Square_root_of_2 dbr:Scala_(programming_language) dbr:Higher-order_logic dbr:University_of_Cambridge dbr:Subroutine dbr:Lightweight_Java dbr:Prime_number_theorem dbr:Computer_science dbr:ANSI_C dbr:Model_theory dbr:Procedural_programming dbr:OCaml dbr:Agda_(programming_language) dbr:Standard_ML dbr:Standard_ML_of_New_Jersey dbr:Tobias_Nipkow dbr:NICTA dbr:Type_soundness dbr:Resolution_(logic) dbr:BSD_license dbr:Counterexample dbr:Automated_theorem_prover dbr:Python_(programming_language) dbr:Formal_semantics_of_programming_languages dbr:Gérard_Huet dbr:Formal_verification dbr:C++ dbr:Tactic_(computer_science) dbr:Meta-logic dbc:Proof_assistants dbr:Axiom_of_choice dbr:Formal_methods dbr:Linux dbr:Haskell_(programming_language) dbr:Integrated_development_environment dbr:Lemma_(mathematics) dbr:Free_Pascal dbr:Technical_University_of_Munich dbr:Lawrence_C._Paulson dbr:Term_rewriting dbr:Satisfiability_modulo_theories dbr:Type_theory dbr:Unification_(computing) dbr:HOL_(proof_assistant) dbr:Proof_by_contradiction dbr:Prover9 dbr:L4_microkernel_family dbr:LCF_theorem_prover dbr:Lean_(proof_assistant) dbr:First-order_logic dbr:Windows dbr:Gödel's_completeness_theorem dbr:LEGO_(proof_assistant)
dbo:wikiPageExternalLink
n10:9301105 n17:isarmathlib.org n17:isabelle.in.tum.de n18: n20: n27:BFb0000502 n29:UCAM-CL-TR-189.pdf n31:tutorial.pdf n32:
owl:sameAs
dbpedia-fr:Isabelle_(logiciel) dbpedia-zh:Isabelle freebase:m.015gp5 n21:4GTTK dbpedia-es:Isabelle dbpedia-pt:Isabelle wikidata:Q460340 dbpedia-de:Isabelle_(Theorembeweiser) dbpedia-ru:Isabelle
dbp:wikiPageUsesTemplate
dbt:Green dbt:IPAc-en dbt:Issn dbt:Reflist dbt:= dbt:Refend dbt:Refbegin dbt:Color dbt:Further dbt:Mathbb dbt:Efn dbt:Blue dbt:Olive dbt:Short_description dbt:Portal dbt:Citation_needed dbt:Start_date_and_age dbt:Notelist dbt:Infobox_software
dbo:thumbnail
n13:Isabelle_jedit.png?width=300
dbp:author
dbr:Lawrence_Paulson
dbp:caption
Isabelle/jEdit running on macOS
dbp:developer
University of Cambridge and Technical University of Munich et al.
dbp:genre
dbr:Mathematics
dbp:latestReleaseVersion
Isabelle2021
dbp:license
dbr:BSD_license
dbp:operatingSystem
dbr:MacOS dbr:Linux dbr:Windows
dbp:programmingLanguage
Standard ML and Scala
dbp:released
1986
dbp:screenshot
Isabelle jedit.png
dbp:website
n18:
dbo:abstract
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 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 ? 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 命名;这名字取自于法国计算机科学家 的女儿。 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. 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 — интерактивный инструмент для автоматического доказательства, использующий логику высшего порядка. Реализован в том же стиле, что и один из первых подобных инструментов — 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), название дано в честь дочери Жерара Юэ. 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.
gold:hypernym
dbr:Prover
prov:wasDerivedFrom
wikipedia-en:Isabelle_(proof_assistant)?oldid=1124441980&ns=0
dbo:wikiPageLength
13475
dbo:latestReleaseVersion
Isabelle2021
dbo:author
dbr:Lawrence_Paulson
dbo:developer
dbr:Technical_University_of_Munich dbr:University_of_Cambridge
dbo:genre
dbr:Mathematics
dbo:license
dbr:BSD_license
dbo:operatingSystem
dbr:Linux dbr:MacOS dbr:Windows
dbo:programmingLanguage
dbr:Standard_ML dbr:Scala_(programming_language)
foaf:isPrimaryTopicOf
wikipedia-en:Isabelle_(proof_assistant)
Subject Item
dbr:JFreeChart
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:Kepler_conjecture
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:Lawrence_Paulson
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
dbo:knownFor
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:TLA+
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:Automated_reasoning
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:Integer
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:Metamath
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:Intelligible_semi-automated_reasoning
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
dbo:wikiPageRedirects
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:Sledgehammer_(Isabelle)
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
dbo:wikiPageRedirects
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:Locale_(Isabelle)
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
dbo:wikiPageRedirects
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:Finger_tree
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:Isabelle_(theorem_prover)
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
dbo:wikiPageRedirects
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:Isabelle_proof_assistant
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
dbo:wikiPageRedirects
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:Isabelle_theorem_prover
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
dbo:wikiPageRedirects
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:The_Archive_of_Formal_Proofs
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
dbo:wikiPageRedirects
dbr:Isabelle_(proof_assistant)
Subject Item
n26:HOL
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
dbo:wikiPageRedirects
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:Isabelle_AFP
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
dbo:wikiPageRedirects
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:Isabelle_software
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
dbo:wikiPageRedirects
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:Isar_(Isabelle)
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
dbo:wikiPageRedirects
dbr:Isabelle_(proof_assistant)
Subject Item
dbr:Nitpick_(Isabelle)
dbo:wikiPageWikiLink
dbr:Isabelle_(proof_assistant)
dbo:wikiPageRedirects
dbr:Isabelle_(proof_assistant)
Subject Item
wikipedia-en:Isabelle_(proof_assistant)
foaf:primaryTopic
dbr:Isabelle_(proof_assistant)